So, why not taking this seriously, by asking if there is a way to express combinatory logic as a logic of zippers.
Besides the fun, there are advantages of using this for computing with space, just let me first explain the logic of zippers in all detail.
The starting point is the fact that the S, K, I combinators and the reductions they are involved into can be expressed by the intermediary of zippers.
I am going back to the post Combinators and zippers.
Zippers are interesting because they behave like actual zippers. Indeed, we can unzip a zipper by a graphic beta move:
Therefore, we can define a k-ZIP move, as a concatenation of k beta moves, which can be applied to a n-zipper, provided that .
As a real zipper, we see that the n-zipper can be split into 2 half zippers, which are denoted as “-n Z” and “+n Z”.
Prepared like this, let’s think about combinators. In the SKI system a general combinator is expressed as a tree made by application nodes, which has as leaves the combinators S, K, and I.
Now, we can see a tree made by application nodes as a combination of + half zippers.
Also, the leaves, i.e. the S,K, I combinators are themselves made of half zippers and termination nodes or fanout nodes.
This is easy to see for the I and K combinator (images taken from the post Combinators and zippers ):
- one -3Z half-zipper
- one -2Z half-zipper
- one -1Z half zipper
- one fanout node
linked in a particular way:
- a tree of + half zippers
- with leaves made by -1Z, -2Z, -3Z half zippers,
- connected perhaps to fanout nodes and termination nodes.
The reduction of a combinator is then expressed by:
- application of k-ZIP moves
- LOC PRUNING moves (in relation to termination nodes and also in relation to CO-ASSOC moves, see further)
- and DIST moves.
Let me explain. The application of k-ZIP moves is clear. The k-ZIP moves shorten the + half zippers which form the application tree.
We sit now in chemlambda, in order to avoid the GLOBAL FAN-OUT. Then, what about the moves related to a half zipper which is connected to the in arrow of a fanout node?
These are DIST moves. Indeed, remark that all half zippers are DISTRIBUTORS. Because they are made by concatenations of lambda or application nodes.
Moreover, the fanout node is a distributor itself! Indeed, we may see the CO-ASSOC move as a DIST move, via the application of some FAN-IN and LOC PRUNING moves:
All in all this defines the Zipper Logic, which is then Turing universal. In the next post I shall give all details, but it’s straightforward.