search

HerrmannM / eole

Éole, a Lévy-optimal lambda calculus evaluator without oracle
GNU General Public License v3.0
110 stars 4 forks source link

Similar projects #1

Open mbuliga opened 5 years ago

mbuliga commented 5 years ago

Hi, I read your [0] and I want to point you some similar projects: Formality, chemlambda and kali.

[0] https://www.reddit.com/r/haskell/comments/dih8xu/optimal_reduction_without_oracle_prototype/

[1] https://github.com/moonad/Formality (labels fans)

[2] https://github.com/chorasimilarity/chemlambda-gui/blob/gh-pages/dynamic/README.md (does not label fans)

[3] https://mbuliga.github.io/kali24.html (does not label fans, working version)

If you look for counterexamples then you may find some in one of the pages linked here

[4] http://imar.ro/~mbuliga/pages.html

I'd be glad to talk more.

HerrmannM commented 5 years ago

Thank you for the links! Your page is really interesting. I did not have a the time to read https://arxiv.org/abs/1811.04960 yet, but it I will!

What do you mean by "label" in the case of formality ?

mbuliga commented 5 years ago

What do you mean by "label" in the case of formality ?

See about the CON node and rewrites here:

https://docs.formality-lang.org/en/latest/theory/Formality-Net.html#rewrite-rules

See also https://github.com/MaiaVictor/optlam

HerrmannM commented 5 years ago

I see, they are not the same kind of label as in Éole. In Formality, they represent the "kind" of the node (like "application"), so they do not label fans. In Éole labels are used to pair fans.

Is kali24 related somehow to EAL? I saw your paper on EM-algebra, but I don't have the background to understand...

Is \x.((\y.yy)(xx)) the counter example you were talking about ?

mbuliga commented 5 years ago

In Formality, they represent the "kind" of the node (like "application"), so they do not label fans.

This is false. Where do you read this? Surely not from the given links.

In Éole labels are used to pair fans.

Just like in optlam which later became formality. Labeling of fans it is not sufficient.

Is kali24 related somehow to EAL? I saw your paper on EM-algebra, but I don't have the background to understand...

If you say that you use two kinds of fanouts then in chemlambda there are one fanin "FI" and two fanouts "FO" and "FOE" with different rewrites. Again all info provided.

kali24 is a different approach, because I made chemlambda not for lambda calculus, but for a formal calculus called "emergent algebra" which appears in metric geometry (em-convex in the last version, is a commutative variant of it). However chemlambda does not cover all that calculus, but kali24 does. In kali24 all the nodes are labeled with elements of the anharmonic group. Still this not works all the time, but for me the constraint is to accept only random rewrite algorithms and the only acceptable translation of lambda terms to graphs should be local too (therefore any global device, like the De Bruijn indices, or croissants and brackets, is not acceptable). What I try does work correctly for graphs coming from lambda terms most of the time, but not always, which I think is the most one can ask for under the given constraints.

Is \x.((\y.yy)(xx)) the counter example you were talking about ?

No, the duplication of it, or of \x.(\f.ff)(\y.xy)

A harder example is the reduction of (\a.aa)(\x.((\b.bb)(\y.yx))), what gives under your algorithm?

--

You are receiving this because you authored the thread.

Reply to this email directly or view it on GitHub:

https://github.com/HerrmannM/eole/issues/1#issuecomment-544880742

HerrmannM commented 5 years ago

My bad, I read too quickly!

CON has 3 ports and an integer label. It is used to represent lambdas, applications, boxes (implicitly) and duplications. Since FM-Core is based on EAL, there is no book-keeping machinery to keep track of Bruijn indices, just CON is enough for beta-reduction. And then That’s why FMC’s box system is necessary: to prevent concurrent duplication processes to interfere with each other by ensuring that, whenever you duplicate a term with dup x = val; ..., all the duplication CON nodes of val will have a labels higher than the one used by that dup.

So that integer label corresponds to the "number of boxes" (https://docs.formality-lang.org/en/latest/theory/Formality-Net.html#compiling-fm-core-to-fm-net). So yes, labels are used to paired fan in both Formality and Éole! But they are still different as Éoles' labels are generated lazily at runtime.

Labeling of fans it is not sufficient. For the full untyped lambda calculus, yes... Maybe the stem fan solves that? (but it seems that no, see below!)

(\a.aa)(\x.((\b.bb)(\y.yx))), what gives under your algorithm? That's interesting, I think this is a counter example! The steps 9-12 give me (d->d d) (d->d d), but then step 13 is different, and everything fall down after... See the pdf It is actually easy to see what is going one: the lambdas force the stem fan to differentiate, leading us back to the way Asperti & Guerrini presented why static labelling does not work... and I don't think we can fix that!

Thank you for helping me settling the case of the untyped lambda calculus! I'm still surprise by the amount of terms that were "accepted" by Éole (like a factorial coded with a yY combinator). Next step will be to see if it corresponds to a useful fragment...

mbuliga commented 5 years ago

(\a.aa)(\x.((\b.bb)(\y.yx))), what gives under your algorithm?

That's interesting, I think this is a counter example! The steps 9-12 give me (d->d d) (d->d d), but then step 13 is different, and everything fall down after...

See the pdf

It is actually easy to see what is going one: the lambdas force the stem fan to differentiate, leading us back to the way Asperti & Guerrini presented why static labelling does not work... and I don't think we can fix that!

I saw this example in https://arxiv.org/pdf/1701.04691.pdf by @codetot https://github.com/codedot

Thank you for helping me settling the case of the untyped lambda calculus! I'm still surprise by the amount of terms that were "accepted" by Éole (like a factorial coded with a yY combinator). Next step will be to see if it corresponds to a useful fragment...

Good luck, I'm interested, but skeptical, as I am about the applications of my systems to lambda calculus. Again, I think the killer app is in chemistry.

--

You are receiving this because you authored the thread.

Reply to this email directly or view it on GitHub:

https://github.com/HerrmannM/eole/issues/1#issuecomment-544966756

mbuliga commented 4 years ago

Hi, these are slides for a talk I gave recently, which explain why this subject is interesting for me.

https://mbuliga.github.io/emergent-10-years/presentation.html

Best regards, Marius

----- Original Message ----- From: HerrmannM notifications@github.com To: HerrmannM/eole eole@noreply.github.com Cc: mbuliga Marius.Buliga@imar.ro, Author author@noreply.github.com Sent: Tue, 22 Oct 2019 16:39:24 +0300 (EEST) Subject: Re: [HerrmannM/eole] Similar projects (#1)

My bad, I read too quickly!

CON has 3 ports and an integer label. It is used to represent lambdas, applications, boxes (implicitly) and duplications. Since FM-Core is based on EAL, there is no book-keeping machinery to keep track of Bruijn indices, just CON is enough for beta-reduction.

And then

That’s why FMC’s box system is necessary: to prevent concurrent duplication processes to interfere with each other by ensuring that, whenever you duplicate a term with dup x = val; ..., all the duplication CON nodes of val will have a labels higher than the one used by that dup.

So that integer label corresponds to the "number of boxes" (https://docs.formality-lang.org/en/latest/theory/Formality-Net.html#compiling-fm-core-to-fm-net).

So yes, labels are used to paired fan in both Formality and Éole! But they are still different as Éoles' labels are generated lazily at runtime.

Labeling of fans it is not sufficient.

For the full untyped lambda calculus, yes... Maybe the stem fan solves that? (but it seems that no, see below!)

(\a.aa)(\x.((\b.bb)(\y.yx))), what gives under your algorithm?

That's interesting, I think this is a counter example! The steps 9-12 give me (d->d d) (d->d d), but then step 13 is different, and everything fall down after...

See the pdf

It is actually easy to see what is going one: the lambdas force the stem fan to differentiate, leading us back to the way Asperti & Guerrini presented why static labelling does not work... and I don't think we can fix that!

Thank you for helping me settling the case of the untyped lambda calculus! I'm still surprise by the amount of terms that were "accepted" by Éole (like a factorial coded with a yY combinator). Next step will be to see if it corresponds to a useful fragment...

--

You are receiving this because you authored the thread.

Reply to this email directly or view it on GitHub:

https://github.com/HerrmannM/eole/issues/1#issuecomment-544966756

mbuliga commented 4 years ago

Hi, I made a landing page for all chemlambda projects here https://chemlambda.github.io/index.html

HerrmannM commented 4 years ago

Hi,

Your slides and this pages are quite interesting! If I may suggest: I think that a small introduction of the subject of computation by chemistry would be great on the landing page (e.g. the same first line as in your slides "Chemlambda for the people").

From what I understood, Éole (which uses some labelling) is not usable in your framework. I"ll keep the repo on, I may one day come back to it and try to figure out what is that thing actually computing...