Tag Archives: zipper

Zipper logic (III). Universality

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.

zipper_not_8

2. The S, K, I combinators in zipper logic are defined int he next figure.

zipper_not_6

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 A be a  combinator, then the zipper combinator which corresponds to IA reduces to the zipper combinator of A:

zipper_not_7

Let A, B be two combinators. Then the zipper combinator corresponding to the combinator (KA)B reduces as in the following figure.

zipper_not_10

The combinator (SK)K reduces to the combinator I, as in the next figure.

zipper_not_11

Now, let A, B, C be three combinators. We see then how the combinator ((SA)B)C reduces to (AC)(BC), when expressed as zipper combinators.

zipper_not_12

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.

________________________________

Zipper logic (II). Details

Continuing from Zipper logic, let’s make the following notation for half zippers:

zipper_not_1

As you see, each half zipper has a leading strand, i.e. the 1->1″ for the (-n)Z  and 1″->1′ for the (+n)Z.

The half zippers are just towers of nodes, therefore if we put a tower over another then we get a bigger tower, provided is made by the same nodes. We transform this into two moves.

zipper_not_2

We make, from two half zippers with opposed signs, a zipper and a half zipper (that is the CLICK move), then we ZIP the zipper (this corresponds to the graphic beta move).  This is explained in the next figure, for a particular case n<m

zipper_not_3

The CLICK move and the (full) zippers are not necessary, but they help to visualize in a more clear way what is happening. Moreover, you shall see that there are other zipper constructs, and the introduction of both full zippers and the CLICK move helps to structure future explanations.

______________________

In the zipper logic formalism, there are also used the fanout node, the termination node and the fanin node (so we are seeing the zippers as if we are in chemlambda).

The fanout and fanin nodes satisfy the FAN-IN move.  The fanout satisfies CO-ASSOC and CO-COMM.

______________________

I mentioned in the previous post that half zippers are distributors. Indeed, they satisfy the following DIST moves when connected at the leading strand with a fanout:

zipper_not_4

______________________

The LOC PRUNING  moves for half zippers are:

zipper_not_5

______________________

In the next post we shall see that zipper logic is universal.

______________________

As given here, some of the moves are not local,  because there is no restriction on the length of the half zippers where the moves apply.  But this is not a serious problem because, as we shall see, it’s enough to use half zippers and moves with bounded length (at least 3).

______________________

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.

_______________________________________