Extensionality in graphic lambda calculus

This is part of the tutorial “Introduction to graphic lambda calculus“.

I want to discuss here the introduction of extensionality in the graphic lambda calculus. In some sense, extensionality is already present in the emergent algebra moves. Have you noticed the move “ext2″?

However, the eta-reduction from untyped lambda calculus needs a new move. I called it the ext1 move in arXiv:1207.0332 [cs.LO] paragraph 2.7. It is a global move, because in order to use it one has to check a global condition (without bound on the number of nodes and edges involved in the condition). In the mentioned paper I stated that the move applies only to graphs  which represent lambda calculus terms, but now I see no reason why it has to be confined to this sector, therefore here I shall formulate the ext1 move in more generality.

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

This move acts like eta-reduction when translated back from graphs to lambda calculus terms. “Ext” comes from “extensionality”.

Let us see why we need to formulate the move like this. Suppose that we eliminate the global condition  “there is no oriented path from “2″ to “1″ outside the left hand side  of the previous picture”. In particular let us suppose that there is an edge from “2″ to “1″ which completes the graphs from the LHS of the previous picture. For this graph, which appears at left in the next figure, we may use the graphic beta move like this (numbers in red indicate how we use the graphic beta move):

If we could apply the ext 1 move to this graph, then the result would be the following:

Not only the result of this move is one loop, but it is the “wrong” loop, in the sense that this loop is obtained by closing the edge which vanishes in thin air when the graphic beta move is applied. There is no contradiction though, unless we wish to decorate the edges (i.e. to evaluate the result of the computation). It is just strange.

There is one question left: why the move called “ext2″, which is one of the emergent algebra moves, is also an extensionality move? A superficial answer is that the move ext2 says that the dilation of coefficient “1″ is the identity function.

About these ads