5 Recursion

5.8 The λ-Calculus

Oh, yeah. We just went there: the λ-calculus.

Take heart, though... this is going to be fun. And after this bit, we'll finally get to the practical coding bits :-)

Keep in mind that the Peano axioms made use of recursion, that Giuseppe Peano played a key role in Bertrand Russell's development of the Principia, that Alonzo Church sought to make improvements on the Principia, and the lambda calculus eventually arose from these efforts.

Church realized when creating the λ-calculus that with only a lambda at his disposal, he could define numbers and perform arithmetic upon them. This is known as "Church encoding". Using what we have defined above, we should be able to peer into this forest of lambdas and perhaps perceive some trees.

Church, with his now-famous students Stephen Kleene and J. Barkley Rosser, established the λ-calculus as equivalent to a Turing machine for determining the computability of a given function. In particular, the Church-Turing Thesis states that the class of functions which are partial recursive functions has the same members as the class of functions which are computable functions.

Previously, we examined natural numbers and operations such as addition in the context of positive integers. However, in the sections below, we will be leaving behind the comfort of the familiar. The λ-calculus does not concern itself with natural numbers per se; rather the ability to do something a given number of times.

5.8.1 A Quick Primer

In the literature, you will see such things as:






This is standard notation for the λ-calculus, and here's how you read it:

  • an expression can be a name, a function, or an application, e.g.: x or λx.x or (λx.x)3
  • a function is represented by a lambda followed by a name, a dot, and an expression, e.g.: λx.x
  • an application is represented as two expressions right next to each other, e.g.: (λx.x)3

As such, one says that λx.x is a function that takes one parameter, x, and produces one output, x. λxy.y takes two parameters, x and y and produces one output, y.

5.8.2 Church Encoding

Let's get our feet wet with figuring out how we can define the natural numbers under Church encoding, starting with zero. In the standard λ-calculus, this is done in the following manner:


We are defining the successor function from above as s. We are also defining x as "that which represents zero". So this reads something like "We pass our counting function represented as s as the first parameter; there's nothing to do but then pass the second parameter x to the next function, which returns x". We never do anything with s and only return x itself.

In the λ-calculus, zero is defined as taking the successor function, doing nothing with it, and returning the value for zero from the identify function. In LFE, this is simple:

(defun zero ()
  (lambda (s)
    (lambda (x) x)))

We've got some nested functions that represent "zero"; now what? Well, we didn't use the successor inside the zero function, if we do, we should get "one", yes? But how? Well, we'll "apply" the successor function that is passed in, as opposed to ignoring it like we did in zero. Here's the Church numeral definition for one:

λs.λx.s x

Let's try that in LFE:

(defun one ()
  (lambda (s)
    (lambda (x)
      (funcall s x))))

Congratulations, you've written your second Church numeral in LFE now :-) Successive numbers are very similar: an additional (funcall s before the (funcall s x.

A small but significant caveat: technically speaking, the functions zero and one are not actual Church numerals, rather they wrap the Church numberals. Once you call these functions, you will have the Church numberals themselves (the lambda that is returned when the numberal functions are called).

Now that we see Church numerals are nested lambdas with nested calls on the successor function, we want to peek inside. How does one convert a Church numeral to, say, an interger representation? Looking at the one function, we can make an educated guess:

  1. We will need to call one so that the top-most lambda is "exposed".
  2. We will need to apply (funcall; it's more convenient) our choice of successor function to that top-most lambda.
  3. We will need to apply our representation of "zero" to the next lambda.

With each of those done we end up with a solution that's actually quite general and can be used on any of our Church numerals. Here's a practical demonstration:

> (slurp "church.lfe")
#(ok church)
> (one)
> (funcall (funcall (one) #'successor/1) 0)

Typing that into the REPL whenever we want to check our Church numeral will be tedious. Let's write a function that allows us to get the integer representation of a Church numeral more easily. There are a couple ways to do this. First:

(defun church->int1 (church-numeral)
  (funcall (funcall church-numeral #'successor/1) 0))

This would require that we call our Church numeral in the following manner (assuming that we've re-slurped the church.lfe file):

> (church->int1 (one))

Alternatively, we could do this:

(defun church->int2 (church-numeral)
  (funcall (funcall (funcall church-numeral) #'successor/1) 0))

This second approach lets us pass the Church numeral without calling it:

> (church->int2 #'one/0)

As mentioned earlier, we know that we can get successive Church numerals by adding more (funcall s applications (i.e., incrementing with a successor function). For instance, here is the Church numeral four:

(defun four ()
  (lambda (s)
    (lambda (x)
      (funcall s
        (funcall s
          (funcall s
            (funcall s x)))))))

Using this method of writing out Church numerals is going to be more tedious that putting beans in a pile to represent integers. What can we do? Well, we need a general (i.e., non-integer) λ-calculus representation for a successor function. Then we need to be able to apply that to zero n times in order to get the desired Church numeral. Let's start with a Church numeral successor function:

λn.λs.λx. s (n s x)

We translate that to LFE with the following:

(defun church-successor (n)
  (lambda (s)
    (lambda (x)
      (funcall s
          (funcall n s) x)))))

Next we need a function that can give us a Church numeral for a given number of applications of the church-successor:

(defun get-church (church-numeral count limit)
  (cond ((== count limit) church-numeral)
        ((/= count limit)
         (get-church (church-successor church-numeral) (+ 1 count) limit))))

We're getting a little bit ahead of ourselves, since we haven't yet talked about countdown or countup recursive functions in LFE; consider this a teaser ;-)

Our get-church function keeps track of how many times it is recursed and returns the appropriate Church numeral when the limit has been reached. However, it's a bit cumbersome to use. Let's see if we can do better:

(defun get-church (integer)
  (get-church (zero) 0 integer))

Now we've got two get-church functions, each with different arity. get-church/1 calls get-church/3 with the appropriate initial arguments, at which point get-church/3 calls itself until the limit is reached and returns a Church numeral.

Let's take a look:

> (slurp "examples/church.lfe")
#(ok church)
> (get-church 0)
> (== (zero) (get-church 0))
> (get-church 1000)

Looks good so far. Let's check out the values:

> (church->int1 (get-church 1)))
> (church->int1 (get-church 50)))
> (church->int1 (get-church 100)))
> (church->int1 (get-church 2000)))
> (church->int1 (get-church 10000)))

That last one caused a little lag in the LFE REPL, but still quite impressive given the fact that it just applied so many thousands of lambdas!

How fortunate that we didn't have to type 10,000 funcalls (and the corresponding set of opening and closing parentheses 10,000 times).

5.8.3 Arithmetic

We looked at basic arithmetic when we were exploring Peano's axioms. Now we're going to do arithmetic at a whole new level, with church encoding.

In the previous section, we defined a Church successor function in the following manner:

λn.λs.λx. s (n s x)

Then we translated that into LFE:

(defun church-successor (n)
  (lambda (s)
    (lambda (x)
      (funcall s
          (funcall n s) x)))))

We bring this up now because an addition function will make use of it. Here is addition as defined in the λ-calculus:

λm.λn.λs.λx. m s (n s x)

We can express this in English with the following: given a Church numeral m and another Church numeral n,

Here's how we would implement it in LFE:

(defun add (m n)
  (lambda (s)
    (lambda (x)
      (funcall m s
          (funcall n s) x)))))

5.8.4 Logic

5.8.5 Church Pairs

5.8.6 List Encoding