Because I am going to explore in future posts the emergent algebra sector, I think it is good to know where we stand with using graphic lambda calculus for describing proofs in emergent algebra as computations. In the big map of research paths, this correspond to the black path linking “Energent algebra sector” with “Emergent algebras”.
A dictionary seems a good way to start this discussion.
Let’s see, there are three formalisms there:
- in the first paper on spaces with dilations, Dilatation structures I. Fundamentals arXiv:math/0608536 section 4, is introduced a formalism using binary decorated trees in order to ease the manipulations of dilation structures,
- emergent algebras are an abstraction of dilation structures, in the sense that they don’t need a metric space to live on. The first paper on the subject is Emergent algebras arXiv:0907.1520 (see also Braided spaces with dilations and sub-riemannian symmetric spaces arXiv:1005.5031 for explanations of the connection between dilation structures and emergent algebras, as well as for braided symmetric spaces, sub-riemannian symmetric spaces, conical groups, items you can see on the big map mentioned before). Emergent algebras is a mixture of an algebraic theory with an important part of epsilon-delta analysis. One of the goals of graphic lambda calculus is to replace this epsilon-delta part by a computational part.
- graphic lambda calculus, extensively described here, has an emergent algebra sector (see arXiv:1305.5786 , equally check out the series Emergent algebras as combinatory logic part I, part II, part III, part IV, ). This is not an algebraic theory, but a formalism which contains lambda calculus.
The first figure describes a dictionary of objects which appear in these three formalisms. In the first column you find objects as they appear in dilation structures – emergent algebra formalism. In the second column you find the corresponding object in the binary trees formalism. In the third column there are the respective objects as they appear in the emergent algebra sector of the graphic lambda calculus.
Some comments: the first two rows are about an object called
- “dilation (of coefficient , with , a commutative group)” in dilation structures, which is a operation in emergent algebras, indexed by , (the second row is about dilations of coefficient ),
- it is an elementary binary tree with the node decorated by white (for ) or black (for )
- it is one of the elementary gates in graphic lambda calculus.
The third row is about the “approximate sum” in dilation structures, which is a composite operation in emergent algebras, which is a certain graph in graphic lambda calculus.
The fourth row is about the “approximate difference” and the fifth about the “approximate inverse”.
What is different between these rows?
- In the first row we have an algebra structure based on identities between composites of operations defined on a set.
- In the second row we have trees with leaves decorated by labels from an alphabet (of formal variables) or terms constructed recursively from those .
- In the third row we have graphs with no variable names. (Recall that in graphic lambda calculus there are no variable names. Everything written in red can be safely erased, it is put there only for the convenience of the reader.)
Let’s see now the dictionary of identities/moves.
The most important comment is that identities in emergent algebras become moves in the other two formalisms. A succession of moves is in fact a proof for an identity.
The names of the identities or moves have been commented in many places, you see there names like “Reidemeister move” which show relations to knot diagrams, etc. See this post for the names of the moves and relations to knot diagrams, as well as section 6 from arXiv:1305.5786 .
Let’s read the first column: it says that from an algebraic viewpoint an emergent algebra is a one parameter family (indexed by ) of idempotent right quasigroups. From the geometric point of view of dilation structures, it is a formalisation of properties expected from an object called “dilation”, namely that it preserves the base-point ( “” in the figure), that a composition of dilations of coefficients , with the same base-point, is again a dilation, of coefficient , etc.
In the second column we see two moves, R1 and R2, which can be applied anywhere in a decorated binary tree, as indicated.
In the third column we see that these moves are among the moves from graphic lambda calculus, namely that R1 is in fact related to the oriented Reidemeister move R1a, so it has the same name.
The fact that the idempotent right quasigroup indexed by the neutral element of , denoted by , is trivial, has no correspondent for binary trees, but it appears as the move (ext 2) in graphic lambda calculus. Through the intermediary of this move appears the univalent termination gate.
These are the common moves. To these moves add, for the part of the emergent algebra sector, the R1b move, the local fan-out moves and some pruning moves. There is also the global fan-out move which is needed, but we are going to replace it by a local move which has the funny name of “linearity of fan-out”, but that’s for later.
The local fan-out moves and the pruning moves are needed for the emergent algebra sector but not for the binary trees or emergent algebras. They are the price we have to pay for eliminating variable names. See the algorithm for producing graphs from lambda calculus terms, for what concerns their use for solving the same problem for untyped lambda calculus. (However, the emergent algebra sector is to be compared not with the lambda calculus sector, but with the combinatory logic sector, more about this in a further post.)
We don’t need all pruning moves, but only one which, together with the local fan-out moves, form a family which could be aptly called:
(notice I consider a reversible local pruning)
Grouping moves like this makes a nice symmetry with the fact that is a commutative group, as remarked here.
As concerns the R1b move, which is the one from the next figure, I shall use it only if really needed (for the moment I don’t). It is needed for the knot diagrams made by emergent algebra gates sector, but it is not yet clear to me if we need it for the emergent algebra sector.
However, there is a correspondent of this move for emergent algebras. Indeed, recall that a right quasigroup is a a quasigroup if the equation has a solution, which is unique. If our emergent algebra is in fact a (family of) quasigroup(s) , as happens for the cases of conical groups or for symmetric spaces in the sense of Loos (explained in arXiv:1005.5031 ), then in particular it follows that the equation has only the solution (for ). This last statement has the R1b move as a correspondent in the realm of the emergent algebra sector.
Until now we have only local moves in the emergent algebra sector. We shall see that we need a global move (the global fan-out) in order to prove that the dictionary works, i.e. for proving the fundamental identities of emergent algebras within the graphic lambda calculus formalism. The goal will be to replace the global fan-out move by a new local move (i.e. one which is not a consequence of the existing moves of graphic lambda calculus). This new move will turn out to be a familiar sight, because it is related to the way we see linearity in emergent algebras.