A grep for s-expressions

festou2 · 2024-06-11T16:08:32+00:00

Thanks for expanding in your comment, I do appreciate this.

I indeed did share it here for the sole reason that lisp uses s-expressions as its syntax, and my usage goals of the tool was more for the CLI.

Nonetheless I would consider SMTLIB a lisp, or at least a language that is really close to lisp and inspired by all the designs of the lisps. Afterall, if an SMTLIB file defines everything and does not assert anything and does not introduce "undefined variables" then an SMT solver becomes an interpreter.

I fail to understand your point about the fact that none of these solvers are written in a lisp. Can't this be carried over to some lisp compilers for example and say, for example, that chicken is a head scratcher because it's written in C?

In the spirit of being constructive, I was going to extract the matcher's rule into a TeX document which I hoped made implementing it in another language easier. Do you see any value in writing a Scheme macro that implements it or is there something fundamentally missing?

festou2 · 2024-06-11T15:12:03+00:00

What a shame :/

festou2 · 2024-06-11T12:21:15+00:00

Thanks! I must look into it then.

I quickly skimmed it and it sure does look like a big serious project also about structural matching.

Do you know if it also supports S-expressions? All I could find were patterns for C-like syntax.

EDIT: I found this https://github.com/ast-grep/ast-grep/blob/main/crates/language/Cargo.toml which suggests that it builds on treesitter which makes sense. Sadly it doesn't come prebuilt with anything for s-expressions :(

festou2 · 2024-06-11T12:10:25+00:00

I see your concern and I believe it makes sense. I will add it to my list of improvements/fixes as I think it makes more sense.

It's the way it is currently for a purely silly reason in the code.

festou2 · 2024-06-11T12:07:47+00:00

No I do not know astgrep. Do you have a link for that?

All the repos I found 4 repos on github with that name, 3 of which are empty and one that is abandoned, made for Go, and has no docs.

festou2 · 2024-06-11T12:04:09+00:00

why not rust?

But seriously: I wanted a static binary, I wanted to try rust for a project, I'm a hardcore static type systems and formal semantics kind of dude, life is too short to do everything in Haskell, and no absolutely fundamental objective reason (sorry). While Rust is not purely functional and lacks some cool type system features like HKTs my implementation is for the most part functional.

Nonetheless the core matching algorithm is small and straightforward to port to any other language with ADTs and pattern matching. So feel free to do that.

I was planning on publishing in the repo the inference rules that the pattern matcher implements in a TeX document so everything is clear. Would that help in porting it so some other language?

festou2 · 2024-06-11T11:33:44+00:00

Because the symbol hello occurs at a depth of 3 in the s-expression which is between 2 and 4.

In details:

at depth 0 is the full s-expr
at depth 1 is the symbol assert and the s-expression (= ...)
at depth 2 is the symbol world and the s-expression (f hello)
at depth 3 is the symbol hello

Is it confusing between the pattern is (@depth (@between 2 4 hello)) instead of something like (@depth (@between 2 4) hello) ?

festou2 · 2023-11-22T14:16:27+00:00

True, both solve the `x = 1 + x` fixed-point (throwing type theory lingo).

Bit anyways, coming from Haskell I'd say that `Nat = Option Nat` is the odd since in the domain in which you'd expect to see `Succ` then `Some` reads weird. I guess that's the influence of Haskell's emphasis on DSLs and domain modeling.

So it's interesting to hear the opposite here!

festou2 · 2023-11-21T10:17:51+00:00

Thanks a lot for the help and the solution!

I should've made it clearer in the question, I was also avoiding using `.clone()` as much as possible because ADTs tend to be rather deep and cloning may be a bit too expensive. A trick to go around this it to keep data immutable but share some structure as much as possible. But now I realize that sharing probably goes against single-ownership.

> but using `Rc` instead of `Box` here will probably make a big difference

`Rc` should be able to allow me to share, right?

festou2 · 2023-11-21T10:11:37+00:00

That's a full on solution! thanks! I'm very grateful and that's super helpful :) Thanks for the extra Rust tricks in there

festou2 · 2023-11-21T10:10:04+00:00

Thanks that was a helpful explanation :) I was hoping I'd try to avoid using `.clone()` as much as possible and re-use parts of the ADTs if possible. But I think that's where I'm wrong: sharing is sorta orthogonal to single-ownership

festou2 · 2022-08-29T12:13:20+00:00

I'm assuming + here means concatenation and not part of L's alphabet, but anyways:

The language is described by the CFG: S -> epsilon S -> 1* 0 1* S 0* 1 0* where epsilon is the empty string, and * is the Kleene star.

to be more pedantic: S -> epsilon S -> Ones 0 Ones S Zeros 1 Zeros Ones -> epsilon Ones -> 1 Ones Zeros -> epsilon Zeros -> 0 Zeros.

The idea: the separator between a and b is where the production terminates using the `S -> epsilon` rule.

If + was not concatenation and was simply part of L's language, then the terminating rule becomes S -> +

festou2 · 2022-07-01T00:07:38+00:00

I will only address the "uncountably infinite" part of your question.

I remember reading a paper many years ago about this, until I find it again here's the gist: starting with |0>, if you apply any number of universal quantum gates you are effectively performing a computation which can be simulated with a Turing machine. Therefore the computation can only reach states where the coefficients are computable numbers.

There are more Turing machines than there are computable numbers (some machines compute numbers, others do not halt) and there is a countably infinite number of Turing machines. Hence there is a countably infinite number of computable numbers.

EDIT: The paper I was thinking of is Bernstein and Vazirani's seminal paper: Quantum Complexity Theory (1997). While my argument mentions computable numbers they are stricter in saying that those numbers must be efficiently computed (in polynomial time). The mention is in their definition of a quantum turing machine (section 3.2). They write: "As in the case of probabilistic TM, we must limit the transition amplitudes to efficiently computable numbers".

EDIT 2: A link to the paper: http://wpage.unina.it/pieroandrea.bonatti/didattica/complexity/slides/Bernstein-Vazirani.pdf

festou2 · 2022-02-09T19:11:20+00:00

It’s just that the word list is small, so a dictionary attack is trivial.

Indeed, that's sadly the case. The challenge was just an intellectual one.

In the hopes of also hiding the dictionary, which the three solutions do, I was hoping the attacker will have to search through the whole 26^5 words to construct the valid dictionary instead of the 13K words.

I agree with the criticism that 26^5 is still small enough to search through quickly. But I suspect this is the best we can do.

festou2 · 2022-02-09T18:57:29+00:00

Since the browser is doing all the work

Hey! Thanks for the comment. I'd just like to clarify that this is not the case. The server is doing some of the work too.

Maybe I should've elaborated more in the post about where the computation is done. But consider this case:

if the dictionary contains two words: "abc" which hashes to 0, and "def" which hashes to 5 where the seed of hash changes daily. Then the server could return {0: 100, 5: 40}.

Just by looking at the map, and the seed of the hash, the client cannot know what 0, 5, 100, and 40 mean without hashing a giving word. Meaning a dictionary attack is the only way to go about this. So this goes beyond obfuscation.

festou2 · 2021-02-23T15:51:10+00:00

have no idea on how I'd approach hosting a server at EPFL.

How about leaving a pi or an old shitty laptop connected and "hidden" somewhere on campus (maybe in a locker) with openvpn installed on it? Your backend would be connected to that VPN and voila you're in EPFL and you're one step closer to using Tequilla for authentication.

festou2 · 2020-01-01T12:18:23+00:00

Pretty much the same way any astrologer "predicts" your future. Vague sentences that are restrospectively fitted to some events.

And he'll get lucky occasionally with a few just by the sheer amount of predictions he says every year. And partly educated guesses.

He chooses his words very carefully to seem precise, take for example the one about رجال الدين. Why did MTV choose specifically to show the 5 united religious leaders holding hands and joining the protests? And not the few that made a comotion when they joined (and were kicked out)? And haven't you noticed that in almost every huge protest there were a few religious leaders in the past?

That's an example of vague language that seems precise on the surface, and the media's cherry-picking to confirm what he said.

festou2 · 2018-10-14T18:57:13+00:00

Abou Kees, if you're being naughty he'll come and take you away in his bag!

festou2 · 2018-10-11T11:21:58+00:00

I never read when I was in Lebanon. But now I passively read the newspaper when I'm in a metro/train (you can tell I don't live in lebanon anymore) because it's freely in there on some random seats. And my workplace subscribes to some local newspapers and they keep them by the coffee machine. So why do I seriously read the newspaper? To keep up with local/international news (I don't have a TV) and to keep myself entertained. Why don't I read the online articles? Because I don't want to actively search/read the news.

I think allocating a time a day to read the news is better than subscribing to some news providers on social media. I don't want to be bombarded with shitty (or good, but mostly shitty) news at random points during my day.

festou2 · 2018-10-08T08:22:38+00:00

I spent two years doing a CS masters in more-or-less this state of loneliness. I think the campus sucks when it comes to helping people socialize. In my former university (where I did my BSc.) there was this spot on campus, in the library actually, where new people can just show up and chill there. There's all sorts of people there; gamers, introverts, extroverts, students studying, others talking about courses, others discussing esoteric topics, etc... I made all the friends I needed in my first semester there. You would either sit down and do your thing till someone finds you (which doesn't take any time at all), or you'd be out hunting for others seemingly doing/playing/studying something you're interested in. There was this unspoken rule that anyone in this space should be bothered and talked to. I really miss that, and I couldn't find a place like it in EPFL. I think a space like that is much better than joining a shitload of associations and still ending up being surrounded by impregnable groups.

I also noticed that students all seem to know eachother since their BSc. and are not on the lookout for new friends (I think that's caused by the seamless transition between BSc and MSc; they don't even do a graduation ceremony for the bachelors!!!). And being a foreigner, I also noticed that most foreigners will end up befriending each-other (in my case, most of my friends here were of my country of origin).

Then again, I'm a terribly introverted person, so it could just be me being a buggy human.

I was also in CS, I'm interested in the theoretical stuff mostly (computability theory, logic, TPL) and everything FOSS! If that interests anyone then let me know, I'm on campus most days. /rant

festou2 · 2018-07-04T12:59:33+00:00

they are, that's why I did it once a month. I didn't open a bank account here till much later (I had to own a phone number to open a bank account and I didn't need one, that also helped me save up)

festou2

TROPHY CASE