Conversion of lambda calculus terms into graphs

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 GRAPH.  (Source used: Local and global moves on locally planar trivalent graphs, lambda calculus and lambda-Scale, arXiv:1207.0332 [cs.LO], section 3.)

 A. Terms in lambda calculus. We have an infinite list of variable names x, y, z, .... 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 A, B are terms then $AB$ is a term,
  • if x is a variable and A is a term then \lambda x. A is a term.

There are two operations:

  • the application, which sends a pair of terms (A,B) to the term AB,
  • lambda abstraction, sending a pair (x,A), made by a variable and a term, to the term \lambda x.A.

I shall therefore represent terms as syntactic trees. For the application operation I shall use the gate \curlywedge and for the lambda abstraction I shall use a gate decorated by a \lambda inscribed into a square.

syntrees

Notice that the gate for the lambda abstraction is not the \lambda 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: I = \lambda x . x, K = \lambda x. (\lambda y . (xy)), S = \lambda x . ( \lambda y . (\lambda z . ((xz)(yz)))) (the SKI combinators),  and other two famous terms, \Omega = (\lambda x. (xx)) (\lambda x. (xx)) and T = (\lambda x . (xy)) (\lambda x . (xy)).
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 B of bound variables.

Take a leaf, say decorated with x \in X. To this leaf is associated a word,   denoted by w(x),  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 \lambda^{L}\lambda^{R}\curlywedge^{L} and  \curlywedge^{R}.

If the first letter of the word w(x) is \lambda^{L} then add to the list  B the pair (x, w(x)) formed by the variable name x, 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 \lambda abstraction gate, this can happen only coming from the right leg of the \lambda abstraction gate, thus we can find only the letter\lambda^{R}. In such a case look at the variable y which decorates the left leg of the same \lambda gate. If x =y then add to the syntactic tree a new arrow, from y to x 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 I = \lambda x . x has associated list B = \left\{ (x, \lambda^{L}) \right\}, the term K = \lambda x . (\lambda y. (xy)) has  the list B = \left\{ (x, \lambda^{L}), (y, \lambda^{L} \lambda^{R}) \right\} and the term  S = \lambda x . ( \lambda y . (\lambda z . ((xz)(yz)))) has the list B = \left\{ (x, \lambda^{L}) , (y, \lambda^{L} \lambda^{R}) , (z, \lambda^{L} \lambda^{R} \lambda^{R}) \right\}. The syntactic trees with added arrows are:

step1_1

  • The term  \Omega = (\lambda x. (xx)) (\lambda x. (xx)) has the list B = \left\{ (x, \lambda^{L} \curlywedge^{L}) , (x, \lambda^{L} \curlywedge^{R}) \right\} and  the term T = (\lambda x . (xy)) (\lambda x . (xy)) has the list  B = \left\{ (x, \lambda^{L} \curlywedge^{L}) , (x, \lambda^{L} \curlywedge^{R}) \right\}. The syntactic trees with added arrows are:

step1_2

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 \lambda abstraction by the \lambda gates of graphic lambda calculus. Now the orientation of arrows is no longer conflicting.

C. Elimination of bound variables, part II.  The  list B  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 x from the pair (x, w(x)), 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 w(x)  and replace it by a termination gate.
If it is connected then erase it and replace it by a tree formed by \Upsilon 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 x. Erase all decorations which were joined to x and also erase all arrows which were added at step 1 to the leaf x from the list.

Examples: after the step 2, the graphs associated to the mentioned lambda terms  are the following.

  • the graphs of I, K, S are these:

step2_1

  •   the graphs of \Omega and T are

step2_2

Remark  that there may be more than one possible tree of gates \Upsilon, at each elimination of a bound variable (in case a bound variable has at least tree occurrences). One may use any tree of \Upsilon 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 \Upsilon 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 \Upsilon 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.

step3_2

We end up with graphs in GRAPH.

Advertisements

23 thoughts on “Conversion of lambda calculus terms into graphs”

  1. Pingback: chorasimilarity
  2. If we think of the space of everyday experience as an ordered set of “places where objects could be found” and those “places” are named, the elimination of the naming scheme would be equivalent to reducing the “space” to just a collection of location invariant relations between the objects.

    1. Yes! And also, “ordered set” should be understood as a trivalent relation of the type “(a,b) is a (map,territory) relation relative to c”, where a,b,c are themselves involved in either some map, territory or relative to place, until you descend to one of the objects.

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