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:

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

_________________

  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:

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

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.

_______________________________________

Un-currying with Actors

This is an illustration of a sequential computation with actors and graphic lambda calculus, based on the ideas from  Actors for the Ackermann machine .  It describes the inverse of the currying process described in  Currying by using zippers and an allusion to the cartesian theater.

Without further ado, let’s watch the play.

The preparation consists in introducing the cast and the initial actors diagram.

The play starts. The actor introduces to and dies, or maybe goes playing elsewhere.

We see the states of the actors and , the other main character is waiting for his line, while the figuration wait in the back of the stage, in artful positions.

The rest of the process consists in unzipping a graphic lambda calculus zipper. Zippers are very useful, because the unzipping process is sequential, i.e. it can happen in only one way. Therefore, by using zippers we can force a naturally distributed parallel computation to happen in a sequential way!

At the end of the computation, the two actors and , which represent the two parts of the zipper, cancel one another. Eventually the graph is now connected with the output to the address and with the inputs to the (addresses of the) figuration actors .

The graph corresponds to the graph from  the post   Currying by using zippers and an allusion to the cartesian theater  and the computation just described is a reversed computation of the one described in the mentioned previous post.

__________________________

As a side remark, graphic lambda calculus suggests that currying and un-currying should be eliminated at the preparation stage of a distributed computation. However, I took this example of computation with actors and GLC as a simple illustration and also for stressing that zippers can impose, if needed, an order of reduction moves in GLC.

__________________________

Teaser: B-type neural networks in graphic lambda calculus (II)

The connections in a B-type neural network can be trained.  The following  quote and figure are taken from the article  Turing’s Neural Networks of 1948, by Jack Copeland and Diane Proudfoot:

Turing introduced a type of neural network that he called a ‘B-type unorganised machine’, consisting of artificial neurons, depicted below as circles, and connection-modifiers, depicted as boxes. A B-type machine may contain any number of neurons connected together in any pattern, but subject always to the restriction that each neuron-to-neuron connection passes through a connection-modifier.

A connection-modifier has two training fibres (coloured green and red in the diagram). Applying a pulse to the green training fibre sets the box to pass its input–either 0 or 1–straight out again. This is pass mode. In pass mode, the box’s output is identical to its input. The effect of a pulse on the red fibre is to place the modifier in interrupt mode. In this mode, the output of the box is always 1, no matter what its input. While it is in interrupt mode, the modifier destroys all information attempting to pass along the connection to which it is attached. Once set, a connection-modifier will maintain its function unless it receives a pulse on the other training fibre. The presence of these modifiers enables a B-type unorganised machine to be trained, by means of what Turing called ‘appropriate interference, mimicking education’.

Let’s try to construct such a connection in graphic lambda calculus.  I shall use the notations from the previous post  Teaser: B-type neural networks in graphic lambda calculus (I).

3. Connections.   In lambda calculus, Church booleans are the following terms: and (remark that is the combinator ).  By using the algorithm for transforming lambda calculus terms into graphs in , we obtain the following graphs:

They act on other graphs () like this:

The graphs are almost identical: they are both made by a 2-zipper with an additional termination gate and a wire. See the  post   Combinators and zippers  for more explanations about , or .

I am going to exploit this structure in the construction of a connection. We are going to need the following ingredients: a 2-zipper, an INPUT BOX (otherwise called “switch”, see further) and an OUTPUT BOX,

which is almost identical with a switch (it is identical as a graph, but we are going to connect it with other graphs at each labelled edge):

I start with the following description of objects and moves from the freedom sector of graphic lambda calculus (the magenta triangles were used also in the previous post).  I call the object from the middle of the picture a switch.

As you can see, a switch can be transformed into one of the two graphs (up and down parts of the figure).  We can exploit the switch in relation with the and graphs. Indeed, look at the next figure, which describes graphs almost identical with the and graph (as represented by using zippers), with an added switch:

Now we are ready for describing a connection like the one from the B-type neural networks (only that better, because it’s done in graphic lambda calculus, thus much more expressive than boolean expressions). Instead of training the connection by a boolean TRUE of FALSE input (coming by one of the green or red wires in the first figure of the post), we replace the connection by an OUTPUT BOX (should I call it “synapse”? I don’t know yet) which is controlled by a switch. The graph of a connection is the following:

The connection between an axon and a dendrite is realized by having the axon at “1” and the dendrite at “3”. We may add a termination gate at “2”, but this is irrelevant somehow. At the top of the figure we have a switch, which can take any of the two positions corresponding, literary, to or . This will transform the OUTPUT BOX into one of the two possible graphs which can be obtained from a switch.

You may ask why did I not put directly a switch instead of an OUTPUT BOX. Because, in this way, the switch itself may be replaced by the OUTPUT BOX of another connection. The second reason is that by separating the graph of the connection into a switch, a 2-zipper and an OUTPUT BOX, I proved that what is making the switch to function is the TRUE-FALSE like input, in a rigorous way. Finally, I recall that in graphic lambda calculus the green dashed ovals are only visual aids, without intrinsic significance. By separating the OUTPUT BOX from the INPUT BOX (i.e. the switch) with a zipper, the graph has now an unambiguous structure.

Currying by using zippers and an allusion to the Cartesian Theater

Here is a recipe for understanding currying with the help of zippers.  (Done in graphic lambda calculus.)

We have a graph which has one output and several inputs. We want to curry it. For this we have to artificially give names to the inputs, i.e. to number them (notice that such a thing is not needed in graphic lambda).

The next step is to use a -zipper in order to clip the inputs, by using graphic beta moves, until we get this:

This graph is, in fact, the following one (we replace the -zipper, which is just a notation, or a macro, with its expression).

The graph inside the green dotted rectangle is the currying of , let’s call him .  This graph has only one output and no inputs.  (The procedure of currying can be made itself into a graph which is applied to  the output of , but we stop at this level for this post.) The graph inside the red dotted rectangle is almost a list. We shall transform it into a list by using again a zipper and one graphic beta move.

Now we’re done!

As you see, the currying creates the list, or the list creates the currying, or both form a pair, like the homunculus and the scenic space , an allusion to my post on the Cartesian Theater.