Zipper logic

As seen in GLC or chemlambda, combinatory logic is a matter of zipping, unzipping or self-multiplication of (half) zippers.

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.

A  n-zipper in GLC (in fact I am going to use chemlambda in order to eliminate the GLOBAL FAN-OUT move)  is a graph which has 2n nodes, looking like this:

zipper_n_1

Zippers are interesting because they behave like actual zippers. Indeed, we can unzip  a zipper by a graphic beta move:

zipper_n_2

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 k \leq n.

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”.

zipper_n_3

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 ):

zipper_3

_________________

zipper_4  The combinator S is made of:

  • one -3Z  half-zipper
  • one -2Z half-zipper
  • one -1Z half zipper
  • one fanout node

linked in a particular way:

zipper_5Conclusion: any combinator expressed through S,K,I is made of:

  • 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:

zipper_n_4

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.

_______________________________________

Advertisements

One thought on “Zipper logic”

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s