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:
λx.x
or
(λx.x)y
or
(λwyx.y(wyx))(λsz.z)
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.:
xorλx.xor(λ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:
λs.λx.x
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:
- 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:
> (slurp "church.lfe")
#(ok church)
> (one)
#Fun<lfe_eval.10.53503600>
> (funcall (funcall (one) #'successor/1) 0)
1Typing 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))
1Alternatively, 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
(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)
#Fun<lfe_eval.10.53503600>
> (== (zero) (get-church 0))
true
> (get-church 1000)
#Fun<lfe_eval.10.53503600>Looks good so far. Let's check out the values:
> (church->int1 (get-church 1)))
1
> (church->int1 (get-church 50)))
50
> (church->int1 (get-church 100)))
100
> (church->int1 (get-church 2000)))
2000
> (church->int1 (get-church 10000)))
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
(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
(funcall n s) x)))))