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 . 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.
The animal has therefore a body, which is a graph in with only one output, decorated in the figure with “OUT”. The allowed gates in the body are: the gate, the gate, the termination and the gates.
To the body is grafted a 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 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.
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
is transformed into the animal
The graphic beta move goes in both directions. For example the identity animal is transformed by the graphic beta move into the following animal
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 , where are untyped lambda calculus terms and is a variable. I call it a pattern because really it is one. Namely, start from the following data: a term , a variable (which appears in … ) and another term . They generate a new term which has all the occurences of the term in which were caused by the substitution , marked somehow.
If you think a bit in graphic lambda terms, that is almost an animal with the “IN” decorated by and the “OUT” decorated by .
Composition of animals corresponds to composition of patterns, namely , where is a term which is defined (with care) such that .
Clearly, the definition of patterns ant their composition is not at all rigorous, but it will be made so in a future post.