Generating a graphviz dot file equivalent to the mol file of pred(3)
in chemlambda v2: pred_3.mol (original name was erroneous)
The lambda calculus expression for pred(3)
(predecessor(3) == 2
) is PRED := λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)
(ref wikipedia)
Writing the above expression as nodes in a graph leads to the below graph. The corresponding dot file was written manually and available further below in this gist. An annotated version of pred_3.mol
to help compare it to pred_3.dot
is available further below in this gist.
To generate the dot file automatically from lambda terms, check http://www.teamshadi.net/chemlambda-js/ (a fork from this jsfiddle ). Its current output for pred(3)
matches with the manually specified graph below.
Version 4 (2019-04-11): shifted indeces back by 1 (e.g. L1 to L0) to match with the auto-generated graph from here
Compare the above graph to the chemlambda d3.js graph for pred_3.mol
here
To experiment with graphviz, use
http://www.webgraphviz.com/ or
https://dreampuf.github.io/GraphvizOnline
http://viz-js.com/
Notes:
- This work was prompted from chamlambda issue #6
- Older versions of graphs:
Thank you for the effort! Here is what I got after 2 hours of trying to understand pred_2.mol. The short message is that it is indeed PRED 3 but after 3 graphical beta rewrites. This is because pred_2.mol is part of experiments which led to chemlambda quines, see for example this description [1].
Further I shall use the rewrites from chemlambda as described in [2].
Let's start with some lambda terms
D = \g.\h.(h(gf))
PRED = \n.\f.\x.( (( (n D ) (\u.x) ) (\v.v)) )
3 = \y.\z.(y(y(yz)))
T = PRED 3
The term T is the lambda term which interests us. Let's see the mol file which is obtained from turning it into a "molecule".
Further I add the line number like this (1), at the beginning of the line, which identifies in your notation with the node number. At the end of the line I add info about whose node it is, like (\u.x). In order to obtain a valid mol file you have first to delete all line numbers and spaces before the node types, as well as all spaces and info after the last port variable.
(1) L 3 2 1 (\u. from \u.x from PRED)
(2) T 2 (u from \u.x does not occur elsewhere in PRED)
(3) L 6 6 5 (\v.v from PRED)
(4) L 4 3 7 (\x. from PRED)
(5) L 7 8 9 (\f. from PRED)
(6) A 10 8 11 (the application of g to f in D)
(7) A 12 11 13 (the application of h to gf in D)
(8) L 13 12 14 (\h. from D)
(9) L 14 10 a43 (\g. from D)
(10) A 19 5 4 (the application of (nD)(\u.x) to (\v.v) from PRED)
(11) A a03 22 a02 (the application yz from 3)
(12) FO a13 a11 a03 (2nd and 3rd occurrence of y in 3)
(13) A a11 a02 a12 (the application of y to (yz) in 3)
(14) FO 21 a41 a13 (1st occurrence of y and input to node (12) in 3)
(15) A a41 a12 a42 (1st application of y to y(yz) in 3)
(16) A 24 a43 17 (the application n to D in PRED)
(17) A 17 1 19 (the application (nD) to (\u.x) in PRED)
(18) L 18 21 16 (\y. from 3)
(19) L a42 22 18 (\z. from 3)
(20) L 9 24 23 (\n. from PRED)
(21) A 23 16 25 (the application of PRED to 3)
not figured in the mol (because my script add the FRIN and FROUT nodes if they are needed)
(22) FROUT 25 (the output, the term T)
The mol file has 21 lines, or 22 with the FROUT line, wich means that the molecule has 21 or 22 nodes with the FROUT node. The pred_2.mol has 15 lines, meaning it describes a molecule with 15 nodes, FROUT (or perhaps FRIN) excluded.
Why is it then claimed to be the chemlambda version of PRED 3? Because I already did some reductions. These are 3 (partial) beta reductions. The same is true for https://github.com/chorasimilarity/chemlambda-gui/blob/gh-pages/dynamic/mol/bigpred.mol which is the correspondent of PRED 28.
We start to reduce (graphically) this "molecule". There is a first beta rewrite which erases the nodes (20) and (21)
L 9 24 23, A 23 16 25 --> Arrow 16 24, Arrow 9 25
Then there are two COMB rewrites which eliminate the two Arrow nodes and renumber the edges: 24 --> 16 , 25 --> 9.
This can be seen as the lambda calculus beta rewrite
PRED 3 --> PRED[n=3]
and still the modified mol file represents exactly the term PRED[n=3]
(1) L 3 2 1 (\u. from \u.x from PRED[n=3])
(2) T 2 (u from \u.x does not occur elsewhere in PRED[n=3])
(3) L 6 6 5 (\v.v from PRED[n=3])
(4) L 4 3 7 (\x. from PRED[n=3])
(5) L 7 8 9 (\f. from PRED[n=3])
(6) A 10 8 11 (the application of g to f in D)
(7) A 12 11 13 (the application of h to gf in D)
(8) L 13 12 14 (\h. from D)
(9) L 14 10 a43 (\g. from D)
(10) A 19 5 4 (the application of (3 D)(\u.x) to (\v.v) from PRED[n=3])
(11) A a03 22 a02 (the application yz from 3)
(12) FO a13 a11 a03 (2nd and 3rd occurrence of y in 3)
(13) A a11 a02 a12 (the application of y to (yz) in 3)
(14) FO 21 a41 a13 (1st occurrence of y and input to node (12) in 3)
(15) A a41 a12 a42 (1st application of y to y(yz) in 3)
(16) A 16 a43 17 (the application 3 to D in PRED[n=3])
(17) A 17 1 19 (the application (3 D) to (\u.x) in PRED[n=3])
(18) L 18 21 16 (\y. from 3)
(19) L a42 22 18 (\z. from 3)
not figured
{22} FROUT 9 (the output, the term PRED[n=3])
We can perform two (graphical) beta rewrites and we obtain the mol file which is misleadingly named http://imar.ro/~mbuliga/pred_2.mol . In lambda calculus this corresponds almost to two beta rewrites in the sub-term (3 D) (\u.x). In lambda calculus this should lead to the subterm (3[y=D])[z=\u.x]. But in chemlambda, even if we do two beta rewrites, we end just before to replace the occurrences of y with copies of D.
Let's see this:
L 18 21 16, A 16 a43 17 --> Arrow a43 21, Arrow 18 17
The nodes (18) and (16) are eliminated and two COMB rewrites renumber the edges: 21 --> a43 , 17 --> 18. We get the mol file
(1) L 3 2 1 (\u. from \u.x )
(2) T 2 (u from \u.x does not occur elsewhere )
(3) L 6 6 5 (\v.v from ...)
(4) L 4 3 7 (\x. from ...)
(5) L 7 8 9 (\f. from ...)
(6) A 10 8 11 (the application of g to f in D)
(7) A 12 11 13 (the application of h to gf in D)
(8) L 13 12 14 (\h. from D)
(9) L 14 10 a43 (\g. from D)
(10) A 19 5 4 (the application of (3 D)(\u.x) to (\v.v) )
(11) A a03 22 a02 (the application (y=D)z from 3)
(12) FO a13 a11 a03 (2nd and 3rd occurrence of (y=D) in 3)
(13) A a11 a02 a12 (the application of (y=D) to ((y=D)z) in 3)
(14) FO a43 a41 a13 (1st occurrence of (y=D) and input to node (12) in 3)
(15) A a41 a12 a42 (1st application of (y=D) to (y=D)((y=D)z) in 3)
(17) A 18 1 19 (the application (3 D) to (\u.x) )
(19) L a42 22 18 (\z. from 3)
not figured
{22} FROUT 9 (the output)
This mol file contains the node (9) L 14 10 a43 whose output a43 is the input of the node (14) FO a43 a41 a12. This configuration cannot be the output of the algorithm of transformation of a lambda term to mol.
Then we have the graphical beta rewrite which would correspond in lambda terms to the substitution [z=\u.x]
L a42 22 18, A 18 1 19 --> Arrow 1 22, Arrow a42 19
The nodes (19) and (17) are eliminated and two COMB rewrites renumber the edges: 22 --> 1 , 19 --> a42. We get the mol file which is the content of pred_2.mol:
(1) L 3 2 1 (\u. from \u.x )
(2) T 2 (u from \u.x does not occur elsewhere )
(3) L 6 6 5 (\v.v from ...)
(4) L 4 3 7 (\x. from ...)
(5) L 7 8 9 (\f. from ...)
(6) A 10 8 11 (the application of g to f in D)
(7) A 12 11 13 (the application of h to gf in D)
(8) L 13 12 14 (\h. from D)
(9) L 14 10 a43 (\g. from D)
(10) A a42 5 4 (the application of (3 D)(\u.x) to (\v.v) )
(11) A a03 1 a02 (the application (y=D)(\u.x) from 3)
(12) FO a13 a11 a03 (2nd and 3rd occurrence of (y=D) in 3)
(13) A a11 a02 a12 (the application of (y=D) to ((y=D)(\u.x)) in 3)
(14) FO a43 a41 a13 (1st occurrence of (y=D) and input to node (12) in 3)
(15) A a41 a12 a42 (1st application of (y=D) to (y=D)((y=D)(\u.x)) in 3)
not figured
{22} FROUT 9 (the output)
This is not the mol file obtained from an algorithm of conversion of a lambda term to mol, because of the same observation as before.
In conclusion this is the mol file not of lambda term, but of a lambda term with some shared parts. There is a whole literature on shared graphs. In my opinion the true image is at the graph leven, not at the lambda calculus level which is only semantic pain, or tarpit.
Finally what about molecules which are not obtained from lambda terms? Chemlambda does not reject them.
[1] https://chorasimilarity.wordpress.com/2019/03/02/lambda-calculus-inspires-experiments-with-chemlambda/
[2] http://chorasimilarity.github.io/chemlambda-gui/dynamic/moves.html