This post continues the previous: “Lambda scale in graphic lambda calculus and diagram crossings“.
Suppose, just suppose for the moment that there is an extension of the graphic beta move, suggested by the previous post. I shall call this move “extended beta move”, or “(ext )”, although a better name would be “scaled beta move”.
The extension to consider has the following form:
What a move! Who could have guessed such a move, involving four gates, without thinking about diagram crossings AND about lambda calculus?
Now, after expressing my enthusiasm, let’s see what this move can do.
First of all, per the previous post, the extended beta move implies the graphic beta move (by using (ext2) and LOCAL PRUNING). Recall that in terms of the crossing macro involving only lambda calculus gates, the graphic beta move looks like this:
which is the same as this:
The extended beta move implies also a new move, expressed via the emergent algebra crossings, namely this:
(See the last post: by the graphic beta move, which is implied by the extended one, the emergent algebra crossing from the RHS of the figure transforms into the graph from the RHS of the first figure, which now, by the extended beta move, transforms into the graphs from the LHS of the last figure.)
Let us give a name to this last move, call it “epsilon beta move”.
Now, fact: the usual graphic beta move together with the epsilon beta move are equivalent with the extended beta move.
Proof: we have to prove only one implication, because we have already proved the other. For this, let us express the graph from the RHS of the first figure with the help of the crossing macros. It looks like this:
Now we see that by applying first a epsilon beta move and then an usual graphic beta move, we recover the extended beta move.
Anyway, the extended beta move is left for further exploration.