Graphic Lambda Calculus and Lambda Graphs

Recently I became aware of the research line started by Wadsworth ( Christopher P. Wadsworth, Semantics and Pragmatics of the Lambda Calculus , DPhil thesis, Oxford, 1971) and then Lamping (John Lamping, An algorithm for optimal lambda calculus reduction, POPL ’90 Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p. 16-30) on lambda graphs and sharing graphs (see for example this article by Stefano Guerrini). I see in Guerrini article, at page 5, a figure which is almost identical to the graphic beta move (and even more, when I shall really understand what a “mux” is, then maybe some of the moves from the middle of the page 5 will turn out to be related with the distributivity moves from the chemical concrete machine).

There are several differences between GLC and  Wadsworth-Lamping  kind of lambda graphs (research line denoted by “WL” further):

  •  the graphs used in GLC are all oriented, made by  trivalent or univalent nodes (the termination node) , while those from WL are a mix of oriented and non-oriented nodes,
  • GLC does not use any names, neither of variables, nor of terms, while in WL names are used everywhere. This looks like a minor difference but instead is very important and here is why. If we live by the “no names” rule then forget about evaluations, in particular forget about evaluation strategies and about using the result of an evaluation for deciding the next computational step. Moreover, forget about representing the state of a computation by a “value”, whatever value might mean. Does it start to look strange? It gets even weirder: forget about thinking in terms of flowcharts with nodes which represent operations (like application and lambda abstraction), which have inputs and outputs like wires which allow propagations of signals. After all forget about this signal idea. Can you? GLC can.
  • GLC has among the nodes a “fan-out” node which satisfies moves (graph rewrites) called CO-ASSOC and CO-COMM, as a replacement for the need to use names in WL, thus the only place in GLC which resembles to “sharing”  from WL is in the use of the GLOBAL FAN-OUT move (see however how this move is eliminated in the fully local version of GLC, called the chemical concrete machine),

Let’s now pass to bigger differences:

  • there is a sector of GLC which is made by graphs resembling the lambda graphs from WL, however, there is no effort made in GLC to work only with this sector, while a big deal of effort in the WL approach consists in finding ways to select those “valid” lambda graphs. In GLC there is no need to restrict only to well constructed lambda graphs.
  • this gives an advantage which GLC has over WL,  namely  that GLC has also other sectors, different from the one of lambda graphs, where the graphic beta move can be applied outside lambda calculus. One of this sectors is particularly interesting: is the sector containing knot and tangle diagrams, which allows GLC to interact with Kauffman Knot Logic   and Knot Automata.  Thus GLC is a formalism which can be used for lambda calculus but also for other types of nonstandard computing models, like Kauffman’s Knot Logic.

Finally, the most important difference comes from the motivation of GLC, which is the need to have a visual representation of certain finite differential computations in spaces with dilations and emergent algebras. This is possible in another sector of GLC, called the “emergent algebra sector” and it is completely out of reach of WL, see

This leads to a rigorous definition of what “computing with space” might be. It can also have very concrete applications, evoked here:

Otherwise, there are many things to learn by a geometer like me, from previous work. There are certainly many geometric things to be learned by CS experts as well, because there is more and more clear that computation needs some notion of space, besides the boringly trivial one dimensional one.

Advertisements

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