Tag Archives: Lambda World Cadiz 2018

Diagrammatic execution models (Lambda World Cadiz 2018) compared with chemlambda

Via this MonkeyPatchBlog post I learned about a keynote presented at the Lambda World Cadiz 2018, on Diagrammatic execution models, quote:

Koko Muroya and Steven Cheung, working under the direction of Dan Ghica, gave a fantastic overview of their work on diagrammatic execution model.   […]

There is a nice demo of their work hosted on github, which was used during the presentation. […]

Applied category theory is booming right now, and this work led me to wonder if they were considering describing their work in a categoretic way (yes, it seems). Some of the demos they showed were reminiscent of chemlambda: a graph evolving given rewriting rules (which incidently provided the illustration for the ACT 2019 announcement).”

So I wanted to see how does the lambda term reduce in chemlambda (with the random reduction).

Here is the GoI Visualiser in action: the term is ((λf. λx. f (f x)) ((λy. y) (λz. z))) (λw. w)

reduced with call-by-need looks like this:

goi

Comparison with chemlambda. The mol file goi.mol for this lambda term is:

A 1 2 out

A 3 4  1

L 5 f 3

FO f 7 9

A 7 8 6

A 9 x 8

L 6 x 5

A 10 11 4

L y y 10

L z z 11

L w w 2

I prepared an archive with all needed, taken from the chemlambda repository. You may just download it and then you shall see in the mol folder the goi.mol file. To produce (a) reduction you write in terminal

bash quiner_shuffle.sh

then you write

goi.mol

then you see that a file goi.html appeared. You write

firefox goi.html &

and you see this:

goi-chem

 

or something equivalent. So that’s how the reduction of this term looks in chemlambda. 🙂 Well, the animated gif shows that again and again…

UPDATE: Thank you for the interest and nice words. If you don’t like my way of writing code, which is to be expected because geometer here, then there is this Haskell implementation.

My opinion is still that the most interesting ideas of chemlambda are:

As concerns the first point, this justifies the accent on the dumbest, random, local reduction algorithm, and the experiments outside graphs which represent lambda terms (from all those chemlambda quines to mixtures of busy beavers and lambda terms).

As for the second point, there is really a lot of mathematics, perhaps logic too, to be explored here.