Animals in lambda calculus

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 GRAPH, 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 A in untyped lambda calculus, with a variable x which is marked (now the green disks correspond to the places where the variable appears in the term). When the animal eats another term B, it means that the variable x is replaced by B in A.  Otherwise said, an animal is an expression like A[x:= ].

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

One thought on “Animals in lambda calculus”

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