Sets, lists and order of moves in graphic lambda calculus

Suppose that we want to group together three arrows in graphic lambda calculus. We have this:

sets_1

We want to group them together such that later, by performing graphic beta moves, the first arrow available to be 11′, then 22′, then 33′. Moreover, we want to group the arrows such that we don’t have to make choices concerning the order of the graphic beta moves, i.e. such that there is only one way to unpack the arrows. The solution is to “pack” the arrows into a variant of a list. Lists have been defined here, in relation to currying.

sets_2

Basically we take a zipper and we close it.  Further we see how to unpack this list.

sets_3

The dashed red curve encircles the only place where we can use a graphic beta move. The first move frees the 11′ arrow and then there is only one place where we can do a graphic beta move, which frees the 22′ arrow and finally a last move frees the 33′ arrow and produces a loop which can be eliminated.

The uniqueness of the order of moves is true, in fact, if we accept as valid beta moves only those from left to right (i.e. those which eliminate gates). Otherwise we can go back and forth with a beta move as long as we want.

There is another way to pack the three arrows, under the form of another graph, which could aptly be called a “set”. This time we need a graph with the property that we can extract any arrow we want from it, by one graphic beta move. Here is the solution:

sets_5

Indeed, in the next figure we see that we have three places, one for each arrow, which can be independently used for extraction of the arrow of choice.

set_4

In between these extremes, there are other possibilities.  In the next figure is a graph which packs the three arrows such that: there are three places where a graphic beta move can be performed, as in the case of the set graph, but once a beta move is performed, the symmetry is broken. The performed beta move does not free any arrow, but now we have the choice between the other two possible beta moves. Any such choice frees only one arrow, and the last possible beta move frees the remaining two arrows simultaneously.

Here is the figure:

sets_6

The graph from the left hand side is not a list, nor a set, although it is as symmetric as a set graph.  There are 3 \cdot 2 = 6 possible ways to unpack the graph. So this graph encodes all lists of two arrows out of the three arrows.

Advertisements

2 thoughts on “Sets, lists and order of moves in graphic lambda calculus”

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