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.

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com 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 )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s