Lambda calculus and the fixed point combinator in chemlambda (IV)

This is the 4th  (continuing from part I  and part II  and part III)   in a series of expository posts where we put together in one place the pieces from various places about:

  • how is treated lambda calculus in chemlambda
  • how it works, with special emphasis on the fixed point combinator.

I hope to make this presentation  self-contained. (However, look up this page, there are links to online tutorials, as well as already many posts on the general subjects, which you may discover either by clicking on the tag cloud at left, or by searching by keywords in this open notebook.)

_________________________________________________________

This series of posts may be used as a longer, more detailed version of sections

  • The chemlambda formalism
  • Chemlambda and lambda calculus
  • Propagators, distributors, multipliers and guns
  • The Y combinator and self-multiplication

from the article M. Buliga, L.H. Kauffman, Chemlambda, universality and self-multiplication,  arXiv:1403.8046 [cs.AI],  which is accepted in the ALIFE 14 conference, 7/30 to 8/2 – 2014 – Javits Center / SUNY Global Center – New York, (go see the presentation of Louis Kauffman if you are near the event.) Here is a link to the published  article, free, at MIT Press.

_________________________________________________________

2.  Lambda calculus terms as seen in  chemlambda .

In this post is explained how to associate to any untyped lambda calculus term a g-pattern.

Important. Not any g-pattern, i.e. not any pattern, and not any molecule from chemlambda is associated to a lambda term!

Recall first what is a(n untyped) lambda term.

<lambda term> ::= <variable> |  ( <lambda term> <lambda term> ) | ( L <variable> . <lambda term>)

The operation which associates to a pair of lambda terms A and B the term AB is called application.

The operation which associates to a variable x and a term A the term Lx.A  is called (lambda) abstraction.

Every variable which appears in a term A is either bound or free. The variable x is bound if it appears under the scope of an abstraction, i.e. there is a part of A with the form Lx. B .

It it allowed to rename the bound variables of a term. This is called alpha renaming or alpha conversion. Two terms which differ only by alpha renaming are considered to be the same one.

It is then possible to rename the bound variables of a term such that if x is a bound variable then it appears under the scope of only one abstraction and moreover it does not appear as a free variable.

Further is an algorithm   which transforms a lambda term, in this form which eliminates the ambiguities of the names of bound variables, into a g-pattern. See the post Conversion of lambda calculus terms into graphs for an algorithm which transforms a general lambda term into a GLC graph.

In this algorithm, a variable is said to be “fresh” if it does not appear before the step of the algorithm in question.

We start from declaring that we shall use (lambda terms) variables as port variables.

 

Let  Trans[a,A]  be the translation operator, which has as input a variable  and a lambda term and as output a mess (see part II for the definition of a mess:  “A mess is any finite multiset of graphical elements in grammar version.”)

The algorithm defines Trans.

We start from an initial pair a0,  A0 , such that a0 does not occur in A0.

Then we define Trans recursively by

  • Trans[a, AB] = A[a’, a”, a]  Trans[a’,A] Trans[a”,B]  with  a’ and a” fresh variables,
  • Trans[a, Lx.A] = L[a’,x,a] Trans[a’,A]  with a’ a fresh variable
  • Trans[a,x] =  Arrow[x,a]  .

Practically, Trans gives a version of the syntactic tree of the term, with some peculiarities related to the use of the grammar version of the graphical elements instead of the usual gates notation for the two operations, and also the strange orientation of the arrow of the lambda node which is decorated by the respective bound variable.

Trans[a0,A0] is a mess and not a g-pattern because there may be (port) variables which occur more than twice. There are two  possible cases for this:

  • (a) either a port variable occurs once as an  out port variable and more than once as an  in port variable,
  • (b)  or it does not occur as an out port variable but it occurs more than once as an in port variable,

Let’s see examples:

  • (a)  start with a0 = a and A0 = Lx.(xx) .  Then Trans[a,Lx.xx] = L[a1,x,a] Trans[a1, xx] = L[a1, x, a] A[a2,a3,a_1] Trans[a2,x] Trans[a3,x] = L[a1,x,a] A[a2,a3,a1] Arrow[x,a2] Arrow[x,a3]

 

first_ex

As you see the port variable x appears 3 times, once as an out port variable, in L[a1,x,a] , and twice as an in port variable, in Arrow[x,a2] Arrow[x,a3] .

  • (b)  start with a0 = a and A0 = (xz)(yz) . Then Trans[a,(xz)(yz)] = A[a1,a2,a] Trans[a1,xz] Trans[a2,yz] = A[a1,a2,a] A[a3,a4,a1] Trans[a3,x] Trans[a4,z] A[a5,a6,a2] Trans[a5,y] Trans[a6,z] = A[a1,a2,a] A[a3,a4,a1]  Arrow[x,a3]  Arrow[z,a4]  A[a5,a6,a2]  Arrow[y,a5] Arrow[z,a6]

 

second_ex

In this case the port variable z does not occur as a out port variable, but it appears twice as a in port variable, in Arrow[z,a4] Arrow[z,a6].

 

To pass from a mess to a g-pattern is easy now: we shall introduce fanout nodes.

Indeed, an FO  tree with free in port a and free out ports a1, a2, …, aN  is, by definition, ANY g-pattern formed by the rules:

  •  FO[a,a1,a2]  is an FO tree
  • if  FOTREE[a,a1,…,aN] is an FO tree which has a as the only free in port variable and a1, …, aN the only free out port variables, then for every j=1,…,N and for any u,v fresh port variables  FOTREE[a,a1,…,aN] FO[aj,u,v]  is an FO tree with a as the only free port in variable and a1, …, aN, u, v  with the aj removed from the list as the free out port variables.

Remark that by a sequence of CO-COMM and  CO-ASSOC moveswe can pass from any FO tree with free in port variable a and free out port variables a1, …, aN to any other FO tree with the same free in or out port variables.

We shall not choose a canonical FO tree associated to a pair formed by one free in port variable and a finite set of free out port variables, for this reason. (However, in any algorithm where FO trees have to be constructed, such a choice will be embedded in the respective algorithm.]

In order to transform the mess which is outputted by the Trans operator, we have to solve the cases (a), (b) explained previously.

(a) Suppose that there is a port variable x which satisfies the description for (a), namely that x occurs once as an  out port variable and more than once as an  in port variable. Remark that, because of the definition of the Trans operator, the port variable x will appear at least twice in a list Arrow[x,a1] … Arrow[x,aN] and only once somewhere in a node L[b,x,c].

Pick then an FO tree FOTREE[x,a1,…,aN]  with the only free in port variable x and the only free out port variables a1, …, aN. Erase then from the mess outputted by Trans the collection Arrow[x,a1] … Arrow[x,aN]  and replace it by FOTREE[x,a1,…,aN].

In this way the port variable x will occur only once in a out port, namely in L[b,x,c] and only once in a in port, namely the first FO[x,…] element of the FO tree FOTREE[x,a1,…,aN].

Let’s see for our example, we have

Trans[a, Lx.xx] = L[a1,x,a] A[a2,a3,a1] Arrow[x,a2] Arrow[x,a3]

so the variable x appears at an out port in the node L[a1,x,a] and at in ports in the list Arrow[x,a2] Arrow[x,a3] .

There is only one FO tree with the free in port x and the free out ports a2, a3, namely FO[x,a2,a3].  Delete the list Arrow[x,a2] Arrow[x,a3] and replace it by FO[x,a2,a3]. This gives

L[a1,x,a] A[a2,a3,a1] FO[x,a2,a3]

which is a g-pattern! Here is what we do, graphically:

fo_first_ex

(b) Suppose that there is a port variable x which satisfies the description for (b), namely that x  does not occur as an out port variable but it occurs more than once as an in port variable. Because of the definition of the Trans operator, it must be that x will appear at least twice in a list Arrow[x,a1] … Arrow[x,aN] and nowhere else.

Pick then a FO tree FOTREE[x,a1,…,aN] with the only free in port variable x and the only free out port variables a1, …, aN.

Delete Arrow[x,a1] … Arrow[x,aN]  and replace it by FOTREE[x,a1,…,aN] .

In this way the variable x will appear only once, as a free in port variable.

For our example, we have

Trans[a,(xz)(yz)] =  A[a1,a2,a] A[a3,a4,a1]  Arrow[x,a3]  Arrow[z,a4]  A[a5,a6,a2]  Arrow[y,a5] Arrow[z,a6]

and the problem is with the port variable z which does not occur in any out port, but it does appear twice as an in port variable, namely in Arrow[z,a4]  Arrow[z,a6] .

We delete Arrow[z,a4]   Arrow[z,a6] and replace it by FO[z,a4,a6] and we get the g-pattern

A[a1,a2,a] A[a3,a4,a1]  Arrow[x,a3]  FO[z,a4,a6]  A[a5,a6,a2]  Arrow[y,a5]

In graphical version, here is what has been done:

fo_second_ex

 

OK, we are almost done.

It may happen that  there are out port variables which appear  from  Lx.A with x not occuring in A (i.e. free).  For example let’s start with a0=a and  A0 = Lx.(Ly. x) . Then Trans[a,Lx.(Ly.x)] = L[a1,x,a] Trans[a1, Ly.x] = L[a1,x,a] L[a2,y,a1] Trans[a2,x] = L[a1,x,a] Arrow[x,a2] L[a2,y,a1].

There is the port variable y which appears only as an out port variable in a L node, here L[a2,y,a1], and not elsewhere.

For those port variables x which appear only in a L[a,x,b] we add a termination node T[x].

In our example L[a1,x,a] Arrow[x,a2] L[a2,y,a1] becomes L[a1,x,a] Arrow[x,a2] L[a2,y,a1] T[y]. Graphically this is

third_ex

We may still have Arrow elements which can be absorbed into the nodes ports, therefore we close the conversion algorithm by:

Apply the COMB moves (see part III)  in the + direction and repeat until there is no place to apply them any more.

 

Exercice: Consider the Y combinator

Y = Lf.(  (Lx. f(xx))    (Ly. f(yy))   )

Find it’s conversion as a g-pattern.

________________________________________________________________

Advertisements

12 thoughts on “Lambda calculus and the fixed point combinator in chemlambda (IV)”

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