Birth and death of zipper combinators (I)

Because zipper logic is a graph rewriting system which does not use variable names, just like GLC and chemlabda,  it needs ways to multiply, distribute or kill  things.

See  Chemlambda, universality and self-multiplication  for multiplication, distribution or propagation phenomena.

In this post we shall see how zipper combinators die or are born, depending on the sense of reading the moves. This can happen in several ways, one of them explained in this post.

This can also be seen as the statement: we can do garbage collection in chemlambda, GLC or zipper logic.

____________________________________

 

Zipper combinators.   The set of zipper combinators is the smallest set of zipper graphs with the properties:

  •  it contains the S, K, I zipper graphs defined in  the next figure

zipper_not_6

  • for any natural number n >0 and for any n+1 zipper combinators, the zipper graph obtained by connecting the out arrows of the  zipper combinators to the in arrows of the (+n) half-zipper is a zipper combinator.

appli

  • any zipper graph which is obtained by applying a zipper logic move to a zipper combinator is a zipper combinator.

 

 

I want to prove that for any zipper combinator A, there is a number n and  a succession of n  LOCAL PRUNING,  CLICK and ZIP moves such that:

zipd_0

Proof.     Becauseof the LOC PRUNING move satisfied by  $latex  (+)$ half-zippers, it follows that by a finite number of these moves we can achieve the effect described in the next figure, for any zipper combinator A (of course, the number of these moves depends on A):

zipd_2

It is left to prove that the free arrow ending with a termination node can “eat”, one by one, all the I, K, S zipper combinators.

For the I combinator, it happens like this:

zipd_1

The case of the combinator K is described next:

zipd_3

The combinator S is absorbed by the following succession of moves:

zipd_4

 

The proof is done.

_____________________________________

We can read all backwards, by saying that an arrow connected to a termination node can give birth to  any zipper combinator, with the out arrow connected to a termination node.

_____________________________________

 

 

 

Advertisements

One thought on “Birth and death of zipper combinators (I)”

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