Graphic lambda calculus

chemlambda4

This is a tutorial for graphic lambda calculus. Up to now the best exposition is arXiv:1305.5786   but there are some facts not covered there.

See  also the related Chemical concrete machine  tutorial.

A decentralized computing model is described in the Distributed GLC tutorial.

 Sources:

 

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

What is graphic lambda calculus?

Graphic lambda calculus is a formalism working with a set GRAPH of oriented, locally planar, trivalent graphs, with decorated nodes (and also wires, loops and a termination gate node).   The set GRAPH 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 GRAPH.

  • The \lambda graph, which corresponds to the lambda abstraction operation from lambda calculus, see lambda terms. It is this:

lambdal

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 x a variable name and A a term and outputs the term \lambda x.A.

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 GRAPH, such that to any lambda abstraction which appears in the term corresponds a \lambda 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 \lambda  gate, but the orientation of the left exit arrow is inverse than the one of the \lambda gate. At some point in the algorithm the orientation is reversed and we get \lambda gates as shown here. There is a reason for this, wait and see.

It is cool though that this \lambda gate looks like it takes a term A as input and it outputs at the left exit arrow the variable name x and at the right exit arrow the term \lambda x.A. (It does not do this, properly, because there will be no variable names in the formalism, but it’s still cool.)

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

curlyl

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 \Upsilon graph, which will be used as a FAN-OUT gate, it is:

upsil

  • The \bar{\varepsilon} graph. For any element \varepsilon \in \Gamma of an abelian group \Gamma (think about \Gamma as being (\mathbb{Z}, +) or ((0,+\infty), \cdot) ) there is an “exploration gate”, or “dilation gate”, which looks like the graph of an operation:

epsil

(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 GRAPH. Any assembly of these gates, in any number, which respects the orientation of arrows, is in GRAPH.

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 GRAPH and all the arrows of an elementary graph either input or output to nothing.

Technically, we may imagine that we complete a graph in GRAPH, 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 GRAPH arrows without nodes which are elementary graphs, called wires

linel

and loops (without nodes from the elementary graphs, nor leaves)

loopl

  • Finally, we introduce an univalent gate, the termination gate:

topl

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

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

The moves.

beta_move_1

commr

assocr

fanoutr

lambdapr

epsipr

globalpr

r1amove

r1bmove

r2move

ext2r

Still in beta version:

Yet more:

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:ext1r

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

Macros.

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

Sectors.

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:

_______________

Simply typed version of 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.

In order to understand how this works, see the following  posts, which aim to describe finite differential calculus as a graph rewriting system:

The chemical concrete machine project:

The neural networks project:

12 thoughts on “Graphic lambda calculus”

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

computing with space | open notebook

computing with space | open notebook

cemerick

Against all odds.

The Quilt Project

writings on data, communication, and computation

Low Dimensional Topology

Recent Progress and Open Problems

Towards a 2nd Renaissance

The Internet of Things & Services: Renaissance Re-Born

kauffman2013

A fine WordPress.com site

Voxel-Engine

An expirimental non-gpu 3d voxel engine.

Theory, Evolution, and Games Group

The EGG studies theoretical computer science, evolution, and game theory.

semanto.me

freedom to grok

outfind.ca *

Out think, out search, out find * A blog by Olivier Charbonneau, Business Librarian at Concordia University (Montréal)

Sauropod Vertebra Picture of the Week

SV-POW! ... All sauropod vertebrae, except when we're talking about Open Access

isomorphismes

computing with space | open notebook

DIANABUJA'S BLOG: Africa, The Middle East, Agriculture, History and Culture

Ambling through the present and past with thoughts about the future

Retraction Watch

Tracking retractions as a window into the scientific process

Shtetl-Optimized

computing with space | open notebook

Theoretical Atlas

He had bought a large map representing the sea, / Without the least vestige of land: / And the crew were much pleased when they found it to be / A map they could all understand.

Gödel's Lost Letter and P=NP

a personal view of the theory of computation

Gowers's Weblog

Mathematics related discussions

Research and Lecture notes

by Fabrice Baudoin

The "Putnam Program"

Language & Brains, Machines & Minds

What's new

Updates on my research and expository papers, discussion of open problems, and other maths-related topics. By Terence Tao

Follow

Get every new post delivered to your Inbox.

Join 75 other followers

%d bloggers like this: