Continues from Zipper logic (II). Details . In this post we shall see that zipper logic is Turing universal.
The plan is the following. I shall define combinators in the zipper logic framework, as being made of two ingredients:
- instead of a tree of application nodes we have a combination of + half zippers (i.e. there is a clear way to transform a binary tree of application nodes into a collection of + zippers)
- each combinator is then seen as being made of a combination of + half zippers (replacing the tree of application nodes) and the combinators S, K, I, seen also as particular combinations of + and – zippers.
1. Converting trees of application nodes into combinations of + zippers is straightforward. Imagine such a tree with the root upwards and leaves downwards. Each application node has then an exit arrow and two input arrows, one at left, the other one at right.
Cut into two each right input arrow which is not a leaf or the root arrow. We obtain a collection of + half zippers. Replace each tower of application nodes from this collection with the corresponding + half zipper.
Then glue back along the arrows which have been cut in two.
An example is given in the following figure.
2. The S, K, I combinators in zipper logic are defined int he next figure.
3. Combinators in zipper logic are by definition trees of application nodes translated into + half zippers, as explained at point 1, with leaves the S, K, I combinators defined at point 2.
4. Computation in zipper logic means the application of the moves (graph rewrites) defined in the previous post Zipper logic (II). Details .
In particular the computation with a combinator in zipper logic means the reduction according to the graph rewrites of zipper logic of the respective combinator, as defined at point 3.
5. Zipper logic is Turing universal. In order to prove this we have to check the usual reductions of the S, K, I combinators.
Let be a combinator, then the zipper combinator which corresponds to reduces to the zipper combinator of :
Let be two combinators. Then the zipper combinator corresponding to the combinator reduces as in the following figure.
The combinator reduces to the combinator , as in the next figure.
Now, let be three combinators. We see then how the combinator reduces to , when expressed as zipper combinators.
We see here a move called “FAN-OUT”. This move is a composite of DIST and FAN-IN, like in chemlambda. It is left to prove that indeed, any zipper combinator is a multiplicator (i.e. the move FAN-OUT makes sense when applied to a zipper combinator). The proof is the same as the one needed in a step of the proof that chemlambda is Turing universal. This is left to the reader, or for another time, if necessary.
Question: why is CLICK needed? after all I used it all the time with ZIP.
Will see this next time, when I shall prove that tangle diagrams are Turing universal, via zipper logic.