The graphic lambda calculus formalism described in the paper Local and global moves on locally planar trivalent graphs, lambda calculus and lambda-Scale concerns moves performed on oriented trivalent graphs, which are locally planar in the sense that each node comes with a cyclic order of the three edges connected with it.
I have shown that a sector of this formalism (i.e. some of the moves applied to a certain set of trivalent graphs) is equivalent with untyped lambda calculus. There are two interesting facts about this, namely:
(a) the set of trivalent graphs is defined by global conditions (“global condition ” as opposed to “local condition”; a local condition is one which involves up to a number of edges and nodes, with fixed ),
(b) apart some unimportant global pruning moves, all the other moves are local. In particular, the most important rule of lambda calculus, the beta reduction, is equivalent with the graphic beta move depicted here
which is a local move!
In this post I want to make some supplementary remarks about this graphic beta move.
1. It is not written in the paper, but this move resembles a lot with the unzip operation from the knotted trivalent graphs formalism, see for example the paper The algebra of knotted trivalent graphs and Turaev’s shadow world by D.P. Thurston, section 3. There are two differences: the unzip operation works on unoriented trivalent graphs and moreover by this move we can only unzip pairs of connected nodes (so the move goes only in one direction).
2. As explained in my paper, the graphic beta move may be used outside of the lambda calculus sector, i.e. it may be used for any oriented trivalent graph from my formalism. The previous remark suggests that there is a connection between knot diagrams formalism and the graphic lambda calculus, because the knotted trivalent graphs formalism contains the knot diagrams one. In the last section of my paper I proposed some relations between knot diagrams and graphic lambda calculus, also in the post Four symbols, where I connect with decorated knot diagrams relevant for emergent algebras.
3. There is though one easy way to see yet another connection between these formalisms: the graphic beta move is a braiding operation!
Indeed, it is important to notice that the moves of the graphic lambda formalism are independent of the particular embeddings of trivalent graphs into the plane. This may not be obvious from the figures which explain the moves, but it is so after further inspection.
Let us look again at the graphic beta move, as depicted in the first figure. In fact, this is a move which transforms a pair of edges (from the right of the picture) into the graph from the left of the picture. The fact that the edges cross in the figure is irrelevant. What matters is that, for the sake of performing the move, one edge is temporarily decorated with 1-3 and the other with 4-2.
Here are two more equivalent depictions of the same rule, coming from different choices of 1-3, 4-2 decorations. We may see the graphic beta move as
but also as
Let me then make some notations of the figures from the left hand sides of the previous diagrams. Here they are: for the first figure we introduce the “crossing notation”
and for the second figure the “opposite crossing notation”:
With these notations the graphic beta move may be see as this braiding operation
or as this other braiding operation
These are “notations” which encode the performing of the graphic beta move in a particular embedding (of the graph) in the plane. As such, they look dependent of the particular embedding, but the crossings satisfy the Reidemeister moves for knot diagrams (see the last section in the paper), therefore the notation system appears to be independent of the change of embedding of the graphs in the 3-dim space!