* UPDATE:* Just go and read/use this, this and this.

____________________

This post is part of the Tutorial: Graphic lambda calculus. It describes the set .

____________________

** What is graphic lambda calculus?**

Graphic lambda calculus is a formalism working with oriented, locally planar, trivalent graphs, with decorated nodes. It has a number of moves (transformations) acting on such graphs, which can be local or global moves.

It contains differential calculus in metric spaces, untyped 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 .

, which corresponds to the lambda abstraction operation from lambda calculus, see lambda terms. It is this:**The gate**

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.)

, which corresponds to the application operation from lambda calculus, see lambda terms. It is this:**The graph**

This looks like the graph of an operation, there are no clever tricks involved. The sign I use is like a curly join sign.

, 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:**The graph.**

(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 .

——————————————

I’m interested in logic and computation.

And I use some proof assistants like as Coq, Agda, Idris etc.

But I’m unsatisfied them because it is too difficult to operate their expressions.

Barendregt had introduced “illative combinatory logic”, which is logical system consists of lambda calculus, some logical constants and deduction rules .

and Luke Palmer had introduced IΞ which is a variety of illative combinatory logic.

http://lukepalmer.wordpress.com/tag/ixi/

I think GRAPH moves in your graphic lambda calculus correspond to inference rules in illative combinatory logic.

Can we replace ε-gate by Ξ-gate in illative combinatory logic?

If it can, what kind of moves is there?

Thanks for pointing to this! I shall look and think about.

Re: YMorita, after a bit of reading, it looks like it might be possible to construct an illative version of graphic lambda calculus with eta reduction, but not that the epsilon gate is the illation gate. Instead, if you look at http://arxiv.org/abs/1205.0139 , which is graphic lambda calculus with eta reduction, written in the ordinary way, as a rewrite system , 2nd part of page 4 and beginning of page 5, the introduction of an illation gate would allow to talk about domains of dilations (corresponding to axiom 0 of dilation structures), in particular would allow to interpret the gate (the one which is graphically represented with two concentric circles in this post ) as being an ordinary dilation gate together with information about the domain of the gate. It is an interesting thing to try (at least for me) and I thank you for this.

Another thing which I would like to try is to interpret Xanadu tumblers as dilation gates, mainly because graphically they ressemble very much with the description of dilations as maps, as here http://arxiv.org/abs/1107.2817 .

Thank you for replying.

Originally, the Illation term is to avoid a paradox in predicate logic or set theory.

But It seems it has relation with the epsilon gate.

By reading your paper, I can vaguely understand what are dilations.

(metric) spaces have inclusion relation, scaling operator, so, they have some algebra.

I hardly understand about Xanadu tumblers.

Xanadu handles address space and its contents (space?).

By the way, the FAN-OUT gate and the beta-star move are my favorites.

In ordinary lambda expression, the FAN-OUT gate isn’t expressed explicitly.

I think the FAN-OUT gate has relation to linear lambda calculus.

Indeed, the FAN-OUT moves CO-COMM, CO-ASSOC and some pruning moves look like diagrams related to co-commutative co-monoids. Examples of such algebraic objects are to be found in relation to linear spaces.

The FAN-OUT gate is not expressed explicitly in ordinary lambda calculus because variable names are used instead. In graphic lambda calculus variable names are eliminated, but for this are needed trees of FAN-OUT gates.

Re Xanadu tumblers, to me they look like graphs of dilations (or relations which approximate such graphs). Graph here is in the sense of the graph of a function.

The algebras related to dilation spaces are the emergent algebras, i.e. families of idempotent right quasigroups parametrized by scale. Funny examples appear in sub-riemannian geometry.

I still hope, but I am not yet satisfied by the graphic lambda calculus, to obtain a notion of computation exclusively with dilation gates and FAN-OUT gates, maybe with the beta star move, which would be the “computing with space” which I am chasing. For the moment I don’t know what is the precise status of the beta star move, mainly because it is (a bit like the FAN-IN move from the chemical machine) a bit too powerful, because it allows to switch arbitrary pairs of arrows.