Here is, in more detail, how the graphic beta rule acts in the lambda calculus sector of the graphic lambda calculus.

Let us meet an animal:

It is a graph in , i.e. a trivalent or univalent locally planar graph, with the decorated nodes corresponding to the operations of lambda abstraction, application, FAN-OUT (but, attention, not really a fan-out gate, unless the GLOBAL FAN-OUT move is used), and termination node (corresponding to univalent nodes).

Moreover, it has a “mouth”, named in the figure “IN”, which is continued by a tree of FAN-OUT gates (this tree may be trivial, i.e. just an arrow). The green discs represent the insertion points of the FAN-OUT tree into the rest of the graph.

After the animal eats, it spills by the OUT arrow. There are no other OUT arrows.

Animals have the following nice property: an animal which eats a graph in the lambda calculus sector (i.e. an untyped lambda calculus term) spills out a graph in the lambda calculus sector (a term).

You may think about an animal as being a term in untyped lambda calculus, with a variable which is marked (now the green disks correspond to the places where the variable appears in the term). When the animal eats another term , it means that the variable is replaced by in . Otherwise said, an animal is an expression like .

Animals are not graphs in the lambda calculus sector.

Let us now apply the graphic beta move: we are going to cross the IN and OUT arrows. It goes like this: first identify the places where the graphic beta move will be applied. This is explained in the next figure:

Apply then the graphic beta move and get:

This is another animal, with trivial FAN-OUT tree after the IN arrow.

So graphic beta move, as seen acting on the lambda calculus sector, looks like a transformation of animals. Untyped lambda calculus is so complex because animals are complex objects, defined by GLOBAL rules, not because the beta move has any intrinsic complexity inside (here I use the word “complex” in the vague, usual, sense, not in any technical sense).

### Like this:

Like Loading...

*Related*

## One thought on “Animals in lambda calculus”