Home > Uncategorized > Extensionality in graphic lambda calculus

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

1. January 2, 2013 at 6:00 pm | #1
Sauropod Vertebra Picture of the Week #AcademicSpring

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

Science to Grok

computing with space

isomorphismes

computing with space

Retraction Watch

Tracking retractions as a window into the scientific process

Shtetl-Optimized

computing with space

Not Even Wrong

computing with space

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

Calculus VII

being boring

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