Tag Archives: untyped lambda calculus

Fixed points in graphic lambda calculus

Background: the page Graphic lambda calculus.

Let A be a graph in GRAPH with one input and one output. For any  graph B with one output, we denote by A(B) the graph obtained  by grafting the output of B to the input of A.

Problem:  Given A, find B such that A(B) \leftrightarrow B, where \leftrightarrow means any finite sequence of moves in graphic lambda calculus.

The solution is in principle the same as in usual lambda calculus, can you recognize it? Here is it. We start from the following:

fixpoint_1

That’s almost done. It suffices to do this:

fixpoint_3

to get a good graph B:

fixpoint_2

Combinators and zippers

The goal of this post is to show how to use graphic lambda calculus for understanding the SKI combinators. For the graphs associated to the SKI combinators see this post.

__________

UPDATE: See also the post “Combinators and stickers“.

__________

Zippers have been introduced here.  In particular, the first three zippers are depicted in the following figure.

zipper_2

The combinator I has the expression I = \lambda x . x and it satisfies the relation I A \rightarrow A, where \rightarrow means any combination of beta reduction and alpha renaming (in this case is just one beta reduction: I A = \left( \lambda x . x \right) A \rightarrow A).

In the next figure it is shown that the combinator I  (figured in green) is just a half of the zipper_1, with an arrow added (figured in blue).

zipper_3

When you open the zipper you get A, as it should.

The combinator K = \lambda xy.x satisfies K A B = (KA)B \rightarrow A. In the next figure the combinator K (in green) appears as half of the zipper_2, with one arrow and one termination gate added (in blue).

zipper_4

When you open the zipper you obtain a pair made by A   and B which gets the termination gate on top of it. GLOBAL PRUNING sends B to the trash bin.

Finally, the combinator S = \lambda xyz. ((xz)(yz)) satisfies SABC = ((SA)B)C \rightarrow (AC)(BC). The combinator S (in green) appears to be made by half of the zipper_3, with some arrows added and also with a “diamond” added (all in blue). Look well at the “diamond”, it is very much alike the emergent sum gate from this post.

zipper_5

The three main sectors of graphic lambda calculus

For a web tutorial on graphic lambda calculus go here.  There will be detailed explanations concerning the three main sectors of the graphic lambda calculus, for the moment here is a brief description of them.

Sectors.

A sector of the graphic lambda calculus is:

  • a set of graphs, defined by a local or global condition,
  • a set of moves from the list of all moves available.

The name “graphic lambda calculus” comes from the fact that there it has untyped lambda calculus as a sector. In fact, there are three important sectors of graphic lambda calculus:

Animals in lambda calculus II. The monoid structure and patterns

This is a continuation of “Animals in lambda calculus“. You may need to consult the web tutorial on graphic lambda calculus.

Animals are particular graphs in GRAPH. They were introduced in the mentioned post. I wrote there that animals have the meaning of a kind of transformations over terms in lambda calculus. I shall come back to this at the end of this post and a future post will develop this subject.

The anatomy of an animal is described in the next figure.

animal_4

The animal has therefore a body, which is a graph in GRAPH with only one output, decorated in the figure with “OUT”.  The allowed gates in the body are: the \lambda gate, the \curlywedge gate, the termination and the \Upsilon gates.

To the body is grafted a \Upsilon tree, with the root decorated in the figure with “IN”. The said tree is called “the spine” of the animal and the grafting points are called “insertions” and are figured by green small disks in the figure.

An animal may have a trivial spine (no \Upsilon gate, only a wire). The most trivial animal is the wire itself, with the body containing just a wire and with no insertion points. Let’s call this animal “the identity”.

Animals may compose one with another, simply by grafting the “OUT” of one animal to the “IN” of the other. The body, the spine and the insertions of the composed animal are described in the next figure.

animal_5

The moral is that the spine and the insertions  of the composed animal are inherited from the first animal in the composition, excepting the case when the first animal has trivial spine (not depicted in the figure).

The pleasant thing is that the set of animals is a monoid with composition and with the identity animal as neutral element. That is: the composition of animals is associative and the identity is the neutral element.

In the first post about animals it is explained that the graphic beta move transforms an animal into an animal.  Indeed, the animal

animal_1

is transformed into the animal

animal_3_p

The graphic beta move goes in both directions.  For example the identity animal is transformed by the graphic beta move into the following animal

animal_3_pp

With this monoid structure in mind, we may ask if there is any category structure behind, such that the animals are (decorations of) arrows. Otherwise said, is there any interesting category which admits a functor from it to the monoid of animals, seen as a category with one object and animals as arrows?

An interesting category is the one of “patterns”, the subject will be developed in a future post. But here I shall explain, in a not totally rigorous way,  what a pattern is.

The category of patterns has the untyped lambda terms as objects (with some care about the use of alpha equivalence) and patterns as arrows. A category may be defined only in terms of its arrows, therefore let me say what a pattern should be.

A bit loosely speaking, a pattern is a pair (A[u:=B], B), where A,B are untyped lambda calculus terms and u is a variable. I call it a pattern because really it is one. Namely, start from the following data: a term A, a variable u (which appears in A … ) and another term B. They generate a new term A[u:=B] which has all the occurences of the term B in A[u:=B] which were caused by the substitution u:=B, marked somehow.

If you think a bit in graphic lambda terms, that is almost an animal with the “IN” decorated by B and the “OUT” decorated by A[u:=B].

Composition of animals corresponds to composition of patterns, namely (C[v:= A[u:=B]], A[u:=B]) (A[u:=B], B) = (D[u:=B], B), where D is a term which is defined (with care) such that D[u:=B] = C[v:= A[u:=B]].

Clearly, the definition of patterns ant their composition is not at all rigorous, but it will be made so in a future post.

A question and a comment about untyped lambda calculus

Question: Is there any formulation in terms of category theory of pure untyped lambda calculus, only with alpha-equivalence and beta-reduction, but not with eta-reduction? Please provide links to the relevant sources, which have to contain proofs.

My impression (which could be wrong) is that the answer is NO. It becomes YES with eta-reduction, am I right?

Comment: This is again about pure untyped lambda calculus, only with alpha-equivalence and beta-reduction. compared with my graphic lambda calculus.  So, in pure untyped lambda calculus there are only two moves: beta-reduction and (a collection of moves under the) alpha-equivalence. At first view, the graphic lambda calculus has much more moves. Let us neglect the emergent algebra moves, which are exterior to lambda calculus. Still, in graphic lambda calculus there are the  fan-out moves    and the pruning moves. Compare these moves with the long prose one has to write in order to really explain how alpha-equivalence works and how terms are written, with all rules and moves included so that a non-human computer might apply them.

UPDATE: The question, formulated as: “is lambda-beta representable?” is an open problem by Barendregt and others. See for the precise language the paper GRaph models of lambda-calculus at work, by C. Berline, Math Struct. for Comput. Sci. 16:1-37, 2006,  link to ps.

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:

animal_1

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:

animal_2

Apply then the graphic beta move and get:

animal_3

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