This post continues the Dictionary from emergent algebra to graphic lambda calculus (I). Let us see if we can prove the approximate associativity property (for the approximate sum) in graphic lambda calculus. I am going to use the dictionary and see if I can make the translation.
With the dilation structures/tree formalism, the approximate associativity, with it’s proof, is this:
Let’s translate the trees, by using the dictionary.
At first sight, the graphs and are clearly in the emergent algebra sector of the graphic lambda calculus. For the graph , which corresponds to the tree from the middle of the first figure, it’s not clear if it belongs to the same sector.
The next figure shows that it does, because we can pass from to by a succession of moves acceptable in the sector.
Problems appear when we try to relate and . The reason of these problems, we shall see, is the fact that we renounced at having variables, by employing the “fan-out” gate . But this gate is a fan-out only in a very weak sense, in fact is more like a co-commutative co-monoid operation.
Let’s see, we prepare in order to be more alike .
There is a part of the final graph which is encircled by a green dashed line, pay attention to it.
We prepare now a bit:
The graph from the right has also an encircled part in green. Look close to this graph, in parallel with the last graph from the preparation of . We remark that these two graphs are the same outside of the respective encircled regions. If we could transform one encircled region into the other then we would have a proof that .
In conclusion, the mystery move
would solve the problem of proving the approximate associativity in the emergent algebra sector of the graphic lambda calculus. Remark that if would really be a fan-out gate, i.e. if we could apply to it GLOBAL FAN-OUT moves, then the mystery move would be true.
But I don’t want to use global moves in the emergent algebra sector, because in the tree formalism all moves are local. Moreover, even with global fan-out, in order to be able to apply it, it would be necessary that at the labels “x” and “u” to be grafted graphs which have no connection in common, therefore, strictly speaking, we succeed to prove an approximate associativity weaker than the approximate associativity from emergent algebras/tree formalism. (The same phenomenon, but for another identity of emergent algebras, is explained in this post.) The reason is in the apparently innocuous but hard to manage fact that we renounce of having variables in graphic lambda calculus.
Next time, about the meaning of the mystery move.