This post continues from Diagrammatic execution models (Lambda World Cadiz 2018) compared with chemlambda . For the context, I quote from this MonkeyPatchBlog post
“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”
The demo is the “GoI Visualiser”. In this post I continue to play with this visualiser and with chemlambda as well.
You can play too by using the link to the GoI Visualiser demo and an archive available here, which contains all is needed for running chemlambda and for producind anything from this post.
There is a readme.txt inside which you may enjoy, with instructions to use and some background.
OK, let’s play.
The Goi Visualiser comes with the untyped lambda term
A = ((λf. λx. f (f x)) ((λy. y) (λz. z))) (λw. w)
and in the preceding post I reduced this term in chemlambda. Now I take this term and remark that there are inside 3 identity terms: (λy. y) , (λz. z) and (λw. w). That is why I take the term
B = (λu.(((λf.λx.f(fx))(uu))u))(λw.w)
which has the property that by one BETA reduction it becomes A.
I filmed the reduction of B with the call-by-need, in the GoI Visualiser:
and, out of curiosity, remarked that call-by-name does not work actually it does but I misunderstood what I see!
What about chemlambda? The “molecule” (i.e. chemlambda graph) for the lambda term B can be either goi-5.mol, i.e.
A out2 in2 out3
L out in1 out2
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
FO in1 2 13
FO 13 10 11
L w w in2
or the goi-6.mol, i.e.
A out2 in2 out3
L out in1 out2
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
FO in1 13 2
FO 13 10 11
L w w in2
These two molecules differ in only one place:
FO in1 2 13 (goi-5.mol) vs. FO in1 13 2 (goi-6.mol)
Everything is in the archive! Go check for yourself, please 🙂
This difference is due to the fact that the algorithm for building a chemlambda molecule from a lambda term leaves freedom for the way to duplicate variables. Here in the case of the term B, this freedom is in relation with the variable “u”. Indeed
B = (λu. … (uu))u) …
and to produce 3 u’s from one we need two FO (fanout) nodes, but we may arrange them in two ways.
The algorithm is the one to be expected, here the one from section 3, M. Buliga, Graphic lambda calculus, Complex Systems 22, 4 (2013), 311-360, arXiv:1305.5786. In chemlambda we transform terms from lambda calculus by this algorithm, but mind that in Graphic Lambda Calculus (GLC) there is only one fanout node, the FO. In chemlambda there are two fanout nodes, the FO and the FOE. What is interesting is that there are no other nodes but the fanin FI, two fanouts FO, FOE, application A, lambda L, arrow Arrow, free input FRIN, free output FROUT, termination T. There are no brackets, boxes, tags!
You want to see again the rewrites of chemlambda? arXiv:1811.04960
So the algorithm of conversion is the one from GLC, with only FO nodes in the initial molecule for the term. There are two possible ways to convert the term B, these are goi-5.mol and goi-6.mol.
The goi-6.mol behaves very cool all the time (i.e. under the random reduction algorithm of chemlambda)
The goi-5.mol behaves very well in about 87.5% cases (i.e. in 7/8 cases), from experiments. In most of the cases the reduction ends with an identity, as it should, but in 1/8 cases we end with this siamese brothers identity:
which is in mol notation:
FI 1 2 out
L z z 1
L v v 2
i.e. a fanin FI is left alone and it does not know that his left and right inputs are the same.
Why is that?
From all examples where I reduced molecules from lambda terms, I encountered this phenomenon only once, see the story of The factorial and the little lisper . In that case, I was able to produce a working example, and as well some funny ones, like this version of the factorial of 5:
(taken from the Chemlambda for the people html/js slides)
This happens because there is a mix between execution and duplication which sometimes goes astray. For example if I take the molecule goi-2.mol
FO out out1 out2
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
which is exactly like the molecule goi.mol for the lambda term A (seen in the previous post), only with
FO out out1 out2
added, then the execution (reduction) of the two copies of A while they duplicate, it goes great:
That is because the nodes FO, FOE and FI satisfy the shuffle trick, which guarantees the duplication of FO trees from lambda terms molecules (in particular).
I suspect that there is a choice of the FO fanout trees in the conversion of a lambda term into a molecule which does the job.
Don’t know how to prove it 🙂