This is part of the tutorial “Introduction to graphic lambda calculus“.
Here is described the algorithm for converting untyped lambda calculus terms into graphs in . (Source used: Graphic lambda calculus, arXiv:1305.5786 section 3.)
A. Terms in lambda calculus. We have an infinite list of variable names . A term in untyped lambda calculus is obtained after the application of a finite number of times of any of the following:
- variables are terms,
- if are terms then $AB$ is a term,
- if is a variable and is a term then is a term.
There are two operations:
- the application, which sends a pair of terms to the term ,
- lambda abstraction, sending a pair , made by a variable and a term, to the term .
I shall therefore represent terms as syntactic trees. For the application operation I shall use the gate and for the lambda abstraction I shall use a gate decorated by a inscribed into a square.
Notice that the gate for the lambda abstraction is not the gate from graphic lambda calculus.
Any term is represented as a binary tree, with nodes for the application and lambda abstraction operations and with leaves decorated by variable names.
I shall take as examples the following five lambda terms: , , (the SKI combinators), and other two famous terms, and .
B. Elimination of bound variables, part I. Any leaf of the tree is connected to the root by an unique path. Start from the leftmost leaf, perform the algorithm explained further, then go to the next leaf at the right and repeat until all leaves are exhausted. We initialize also an empty list of bound variables.
Take a leaf, say decorated with . To this leaf is associated a word, denoted by , which is formed by the symbols of gates which are on the path which connects (from the bottom-up) the leaf with the root, together with information about which way, left (L) or right (R), the path passes through the gates. Such a word is formed by the letters , , and .
If the first letter of the word is then add to the list the pair formed by the variable name , and the associated word (describing the path to follow from the respective leaf to the root). Then pass to a new leaf.
Else continue along the path to the root. If we arrive at a abstraction gate, this can happen only coming from the right leg of the abstraction gate, thus we can find only the letter. In such a case look at the variable which decorates the left leg of the same gate. If then add to the syntactic tree a new arrow, from to and proceed further along the path, else proceed further. If the root is attained then pass to next leaf.
Examples: the graphs associated to the mentioned lambda terms, together with the list of bound variables, are the following. (The added arrows are figured in red.)
- The term has associated list , the term has the list and the term has the list . The syntactic trees with added arrows are:
- The term has the list and the term has the list . The syntactic trees with added arrows are:
As you can see, there is a conflict of orientation of the red and black arrows. Therefore replace at this step the “square” gates of abstraction by the gates of graphic lambda calculus. Now the orientation of arrows is no longer conflicting.
C. Elimination of bound variables, part II. The list describes the bound variables. If the list is empty then go to the next step. Else, do the following, starting from the first element of the list, until the list is finished.
The variable name part of an element of the list, say the from the pair , is either connected to other leaves by one or more arrows added at step 1, or not. If it is not connected then erase the variable name with the associated path and replace it by a termination gate.
If it is connected then erase it and replace it by a tree formed by gates, which starts at the place where the element of the list was before the erasure and stops at the leaves which were connected to . Erase all decorations which were joined to and also erase all arrows which were added at step 1 to the leaf from the list.
Examples: after the step 2, the graphs associated to the mentioned lambda terms are the following.
- the graphs of are these:
- the graphs of and are
Remark that there may be more than one possible tree of gates , at each elimination of a bound variable (in case a bound variable has at least tree occurrences). One may use any tree of gates which is fit. The problem of multiple possibilities is solved by the CO-ASSOC move, in the sense that we may pass from one choice of a tree of gates to another by a succession of CO-ASSOC moves.
D. The last step. We may still have leaves decorated by free variables. Starting from the left to the right, group them together in case some of them occur in multiple places, then replace the multiple occurrences of a free variable by a tree of gates with a free root, which ends exactly where the occurrences of the respective variable are. Again, there are multiple ways of doing this, but we may pass from one to another by a sequence of (CO-ASSOC) moves.
Examples: after the step 3, all the graphs associated to the mentioned lambda terms, excepting the last one, are left unchanged. The graph of the last term, changes like in the right hand side of the following figure.
We end up with graphs in .