Graphic lambda calculus
- The tag graphic lambda calculus from the chorasimilarity blog
- The page “Emergent algebras / Computing with space / Graphical calculi“
The following list of papers (this list will be updated with new papers and with publication details):
- (arxiv) – On graphic lambda calculus and the dual of the graphic beta move
- (arxiv) – Graphic lambda calculus and knot diagrams
- (arxiv) – Local and global moves on locally planar trivalent graphs, lambda calculus and lambda-Scale
- (arxiv) – Lambda-Scale, a lambda calculus for spaces with dilations
- (arxiv) – Emergent algebras
What is graphic lambda calculus?
Graphic lambda calculus is a formalism working with a set of oriented, locally planar, trivalent graphs, with decorated nodes (and also wires, loops and a termination gate). The set is described in the Introduction to graphic lambda calculus.
There are moves acting on such graphs, which can be local or global moves.
Graphic lambda calculus contains differential calculus in metric spaces, untyped (or simply typed) lambda calculus and that part of knot theory which can be expressed by using knot diagrams.
The set GRAPH.
This is the set of graphs which are subjected to the moves. Any assembly of the following elementary graphs, called “gates” is a graph in .
- The gate, which corresponds to the lambda abstraction operation from lambda calculus, see lambda terms. It is this:
But wait! This gate looks like it has one input (the entry arrow) and two outputs (the left and right exit arrows respectively). This could not be a graph representing an operation, because an operation has two inputs and one output. For example, the lambda abstraction operation takes as inputs a variable name and a term and outputs the term .
Remember that the graphic lambda calculus does not have variable names. There is a certain algorithm which transforms a lambda term into a graph in , such that to any lambda abstraction which appears in the term corresponds a gate. The algorithm starts with the representation of the lambda abstraction operation as a node with two inputs and one output, namely as an elementary gate which looks like the gate, but the orientation of the left exit arrow is inverse than the one of the gate. At some point in the algorithm the orientation is reversed and we get gates as shown here. There is a reason for this, wait and see.
It is cool though that this gate looks like it takes a term as input and it outputs at the left exit arrow the variable name and at the right exit arrow the term . (It does not do this, properly, because there will be no variable names in the formalism, but it’s still cool.)
- The graph, which corresponds to the application operation from lambda calculus, see lambda terms. It is this:
This looks like the graph of an operation, there are no clever tricks involved. The sign I use is like a curly join sign.
- The graph, which will be used as a FAN-OUT gate, it is:
- The graph. For any element of an abelian group (think about as being or ) there is an “exploration gate”, or “dilation gate”, which looks like the graph of an operation:
(Therefore we have a family of operations, called “dilations”, indexed by the elements of an abelian group. This is a structure coming from emergent algebras.)
We use these elementary graphs for constructing the graphs in . Any assembly of these gates, in any number, which respects the orientation of arrows, is in .
Remark that we obtain trivalent graphs, with decorated nodes, each node having a cyclical order of his arrows (hence locally planar graphs).
There is a small thing to mention though: we may have arrows which input or output into nothing. Indeed, in particular the elementary graphs or gates are in and all the arrows of an elementary graph either input or output to nothing.
Technically, we may imagine that we complete a graph in , if necessary, with univalent nodes, called “leaves” (they may be be decorated with “INPUT” or “OUTPUT”, depending on the orientation of the arrow where they sit onto).
- For this reason we admit into arrows without nodes which are elementary graphs, called wires
and loops (without nodes from the elementary graphs, nor leaves)
- Finally, we introduce an univalent gate, the termination gate:
The termination gate has an input leaf and no output.
and now, any graph which is a reunion of lines, loops and assemblies of the elementary graphs (termination graph included) is in .
Still in beta version:
- The ext1 move, if you need extensionality.
If there is no oriented path from “2″ to “1″ outside the left hand side picture then one may replace this picture by an edge. Conversely, if there is no oriented path connecting “2″ with “1″ then one may replace the edge with the graph from the left hand side of the following picture:
- Crossings in lambda calculus (graphic beta rule as braiding)
- Emergent algebra crossings
- The zipper and examples
- Packing arrows (II) and the strand networks sector
- Sets, lists and order of moves in graphic lambda calculus
A sector of the graphic lambda calculus is:
- a set of graphs, defined by a local or global condition,
- a set of moves from the list of all moves available.
The name “graphic lambda calculus” comes from the fact that there it has untyped lambda calculus as a sector. In fact, there are
three four important sectors of graphic lambda calculus:
- untyped lambda calculus sector, which contains all graphs in which are obtained from untyped lambda calculus terms by the algorithm described here. The moves of this sector are: graphic beta move, fan-out moves, pruning moves. The article arxiv:1207.0332 describes this sector in detail.
- emergent algebra sector, which contain all graphs in described in the article arxiv:1103.6007, via the emergent algebra crossing macros, and the following moves: dual graphic beta move (which forms with the graphic move the extended beta move), fan-out moves, pruning moves, emergent algebra moves. See arXiv:1305.5786 section 5 for a precise description, as well as the post Emergent algebras as combinatory logic part IV (and check out the trackbacks).
- knot and tangle diagrams sector, defined by using crossings in lambda calculus macro and the Reidemeister moves as described in the post Generating set of Reidemeister moves for graphic lambda crossings, which are composite moves obtained from the graphic beta move and some local fan-out moves. The article arxiv:1211.1604 describes this sector in detail.
- Freedom sector of graphic lambda calculus
Simply typed version of graphic lambda calculus:
- Simply typed graphic lambda calculus
- Example: decorations of S,K,I combinators in simply typed graphic lambda calculus
Where I use it (work in progress) and other useful links:
In these two posts is used the tree formalism of the emergent algebras.
- Parallel transport in spaces with dilations, I
- What group is this? (Parallel transport in spaces with dilations, II)
In order to understand how this works, see the following posts, which aim to describe finite differential calculus as a graph rewriting system:
- Dictionary from emergent algebra to graphic lambda calculus (I)
- Dictionary from emergent algebra to graphic lambda calculus (II)
- Dictionary from emergent algebra to graphic lambda calculus (III)
The chemical concrete machine project:
- A chemical concrete machine for lambda calculus
- Local FAN-IN eliminates global FAN-OUT (I)
- Local FAN-IN eliminates GLOBAL FAN-OUT (II)
- Chemical concrete machine, short list of gates and moves
- Ancient Turing machine helps Chemical concrete machine
- Spiral patterns in the full zipper graph
- Extreme functional programming done with biological computers
- Chemical concrete machine, detailed (I)
- Chemical concrete machine, detailed (II)
- Chemical concret machine, detailed (III)
- Chemical concrete machine, detailed (IV)
- Chemical concrete machine, detailed (V)
- Chemical concrete machine, detailed (VI)
The neural networks project: