Packing and unpacking arrows in graphic lambda calculus

In this post, which continues Currying by using zippers and an allusion to the Cartesian Theater, I want to explain how we may pack and unpack two arrows into one, in the realm of graphic lambda calculus.  An algebrization of graphic lambda calculus may be deduced from this, but one step of it, namely enumerating arbitrarily the nodes of a graph in GRAPH, suffers from the same cartesian disease which was exposed in the previously mentioned post. But nevermind, it is at least funny to show that the usual ways of CS thinking may be used to transform this apparently more general frame of graphic lambda calculus into a 1D string submitted to local algebraic manipulations.

We start from the following sequence of three graphic beta moves.

reg_1

With words, this figure means: we pack the 1, 2, entries into a list, we pass it trough one arrow then we unpack the list into the outputs 3, 4. This packing-unpacking trick may be used of course for more than a pair of arrows, in obvious ways, therefore it is not a restriction of generality to  write only about two arrows.

We may apply the trick to a  pair of graphs in GRAPH, call them A and B, which are connected by a pair of arrows, like in the following figure.

reg_2

With the added packing and unpacking triples of gates, the graphs A, B are interacting only by the intermediary of one arrow.

In particular, we may use this trick for the elementary gates of abstraction and application,  transforming them into graphs with one input and one output, like this:

reg_3

Let’s look now at the graphic beta move:

beta_move_1

If we use the elementary gates transformed into graphs with one input and one output, the move becomes this almost algebraic, 1D rule:

reg_4

Finally, the packing-unpacking trick described in the first figure becomes this:

reg_5

Advertisements

8 thoughts on “Packing and unpacking arrows 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