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.


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.


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:


Let’s look now at the graphic beta move:


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


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


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

You are commenting using your account. Log Out /  Change )

Google photo

You are commenting using your Google 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 )

Connecting to %s