No extensionality, no semantics

Extensionality, seen as eta reduction, or eta conversion, is a move which can be described in GLC, but it is global, not local.

See this post for the description of the move. The move is called “ext1”. I borrow from that post the description of the move.

Move ext1.  If there is no oriented path from “2″ to “1″ outside the left hand side picture then one may replace this picture by an arrow. Conversely, if there is no oriented path connecting “2″ with “1″ then one may replace the arrow with the graph from the left hand side of the following picture:


Why is this move global? Because of the condition “there is no oriented path from “2″ to “1″ outside the left hand side picture”.  This condition involves an unbounded number of nodes and arrows, therefore it is global.

Further I shall make the usual comments:

  • the move ext1, by itself,  can be applied to any GLC graph, not only to those graphs which represent lambda terms. In this respect the move ext1 is treated like the graphic beta move, which, in GLC, can be applied to any graph (for example to graphs which are used to encode knot diagrams, or other examples of graphs which are outside the lambda calculus sector of GLC, but nevertheless are interesting),
  • if we restrict the move ext1 to lambda graphs then we have another problem: the condition “is a lambda graph” is global.

That is why the move ext1 is not considered to be part of GLC, nor will be used in distributed GLC.

You may remark that   GLOBAL FAN-OUT is a global move, which is part of GLC.  The answer to the implicit question is that chemlambda, which is a purely local graph rewriting system, solves this. Even if chemlambda and GLC are different formalisms, when it comes to universality, then they behave the same on lambda graphs, with the bonus on the chemlambda side of being able to prove that we can replace the use of the GLOBAL FAN-OUT with a succession of moves from chemlambda.

This can’t be done for the move ext1.

And this is actually good, because it opens a very intriguing research path: how far can we go by using only locality?

That means in particular: how far can we go without semantics?


  • extensionality brings functions
  • functions bring types
  • types bring the type police
  • the type police brings semantics.

It looks that life (basic works of real lifeforms) goes very well:

  • without semantics
  • with self-duplication instead of GLOBAL FAN-OUT (or even instead recursion).

In this respects distributed GLC is even more life-like than it looks at first sight.

2 thoughts on “No extensionality, no semantics”

Leave a Reply

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

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

Google photo

You are commenting using your Google 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 )

Connecting to %s