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.:
- a function is represented by a lambda followed by a name, a dot, and an
- an application is represented as two expressions right next to each other,
As such, one says that
λx.x is a function that takes one parameter,
produces one output,
λxy.y takes two parameters,
produces one output,
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
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:
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
Let's try that in LFE:
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
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:
- We will need to call
oneso that the top-most lambda is "exposed".
- We will need to apply (
funcall; it's more convenient) our choice of successor function to that top-most lambda.
- 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:
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:
This would require that we call our Church numeral in the following manner
(assuming that we've re-
Alternatively, we could do this:
This second approach lets us pass the Church numeral without calling it:
As mentioned earlier, we know that we can get successive Church numerals by
(funcall s applications (i.e., incrementing with a successor
function). For instance, here is the Church numeral
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
n times in order to
get the desired Church numeral. Let's start with a Church numeral successor
λn.λs.λx. s (n s x)
We translate that to LFE with the following:
Next we need a function that can give us a Church numeral for a given number of
applications of the
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 ;-)
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:
Now we've got two
get-church functions, each with different arity.
get-church/3 with the appropriate initial arguments, at
get-church/3 calls itself until the limit is reached and returns
a Church numeral.
Let's take a look:
Looks good so far. Let's check out the values:
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).
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:
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
Here's how we would implement it in LFE: