1 From zero to zero
Just for kicks - in no way premeditatively or anything - I’m going write a silly little function called
This function takes an argument
f, returns a new function accepting an argument
x, and just returns
x. It forgets about
Of what use could this possibly be, you ask? I have a different question: why did I name it
What about this function relates to the number 0? Maybe it’ll be clearer if I show the next silly little function:
Both functions took two arguments;
_0 used the first one 0 times, and
_1 used it 1 time. And I bet you’ll never guess what the name of this function is:
If you guessed
Indeed, if you play with it you’ll see that
actualNumber(_0) = 0 actualNumber(_1) = 1 actualNumber(_2) = 2
and so on. We might be on to something here!
2 A trip to Church
A long time ago a fellow named Alonzo Church started fooling around with these. They’re now called Church numerals. But why?
He was studying a subject called lambda calculus. Lambda calculus is really quite simple: it is the study and application of so-called lambda functions. Lambda functions are traditionally written like thisThe little “λ” is the Greek lower-case letter lambda, by the way.
λf. λx. f x
You may notice this bears striking resemblance to our friend
_1 and that’s because, well, it is
In lambda calculus, the only thing you work with are lambda functions. At its foundation there are no numbers, no addition or multiplication, no nothing. Functions take functions as arguments, and produce functions as results.
And yet lambda calculus forms the theoretical underpinnings of computer science and can serve as the foundation for mathematics. How?! Easy: he simply constructed numbers and arithmetic out of lambda functions.
The purpose of this post is to retrace those steps.
3 One more time!
Church numerals are are just functions. They ask for two parameters and then apply the first one to the second some number of times and in this way they encode real data.
But if they’re really numbers, then I should be able to add them, right? Adding
_2 should give me
_3 and multiplying
_3 should give
_6. Can we do that?
Let’s start small. Let’s write a function which, given a Church numeral, increments it by 1. We know that this function’s argument is going to be some numeral - say,
n - so let’s not overthink this too much:
The result of the function is going to be a Church numeral, right? Thus the beginning of the result is going to take an
f and an
x. We may proceed pretty mindlessly:
Now here’s the tricky part.
n is a function taking
x, too, and it will apply
x some number of times. So we know we need to give
n its arguments:
This isn’t quite right, though. Giving
x will apply
x a certain number of times, but we want to apply
f one more time.
Again, let’s not overthink this. We already have
f so let’s … apply
f one more time:
Let’s be sure this works:
incr(_1) => (λn. λf. λx. f ((n f) x)) (λf. λx. f x) \-------- incr ---------/ \--- _1 ----/ => λf. λx. f (( (λf. λx. f x) f ) x) => λf. λx. f ( f x )
Sure enough, that’s
_2! How about
incr(_0) => (λn. λf. λx. f ((n f) x)) (λf. λx. x) \-------- incr ---------/ \-- _0 ---/ => λf. λx. f (( (λf. λx. x) f ) x) => λf. λx. f (x)
I don’t know about you but I’m convinced.
4 Additionally …
Now we are ready to tackle a slightly more complex problem: adding two Church numerals. So we have some number
a which applies
f some number a times and some number
b which applies
f some number b times.
incr we know that we’re going to take two numbers and return a third so we can get this out of the way:
Cool. A Church numeral applies its first argument to its second argument any number of times. We’re adding
b so we know we want
f applied at least a times:
We want to take the result of
a(f)(x) and then apply
b more times to it. It’s really easy to over think this!
b will do the work of applying
f b times, and
a will do the work of applying
f a times.
Let’s test our function by adding
add(_1)(_2) => (λa. λb. λf. λx. (b f)((a f) x)) (λf. λx. f x) (λf. λx. f (f x)) \----------- add --------------/ \--- _1 ----/ \----- _2 ------/ => λf. λx. ((λf. λx. f (f x)) f) (((λf. λx. f x) f) x) \------- _2 --------/ \-------- _1 -------/ => λf. λx. (λx. f (f x)) (((λf. λx. f x) f) x) => λf. λx. (f (f (((λf. λx. f x) f) x))) => λf. λx. f (f (f x))
f is applied three times so we indeed got
5 Do you have the times?
Triumphant and cocky let’s now try our hands at multiplication. This is trickier: for each time
a would normally apply
f, we want to apply it b times instead. You know the drill:
a will apply its first argument to its second a times;
b will similarly apply
f b times.
So what if
(b f) was the function given as the first argument to
a would apply
(b f) a times and each time
b would apply
f b times.
I’ll leave it as an exercise for the reader to work this one out.
6 Don’t be listless, this is where it gets good
It’s pretty interestingWell, I think so.
that we can represent numbers and arithmetic using lambda calculus, but what else can we do?
I’m going to provocatively rename
Imagine if the
f that we gave our Church numerals required 2 values? Something like, I don’t know,
prepend does exactly what it says: takes a value and an array and prepends the value to the array.
incr function would have to look a little bit different: “incrementing” isn’t just applying
x one more time, it means giving
f another value and then applying it to
To ruin the surprise I’ll name this modified incrementer
Let’s see it in action:
That was anti-climactic. Of course, just like with Church numerals, we have to provide a little conversion function:
Let’s try again:
HOLY MOLY. So we can represent lists, too! We just made a data structure out of lambda functions.
Note, though, that we could actually use any two-argument function and any base starting value. Let’s write a function I’ll call
What’s the big deal here?
foldr is a right fold - what a lucky coincidence I gave it that name, huh?
I could go on about folds and how you can define data structures by the way in which you destroy them, and then subsequently wax romantic about how this really is the nature of existence, but I’ll stop here.
7 The Big Picture
I think it’s very profound that we are able to construct data out of functions, blurring the line between the two. This turns out to give lambda calculus sufficient expressive power to compute anything which can be computed.
The Church-Turing thesis showed that Turing machines are equivalent to the lambda calculus and thus are also powerful enough to express any computation.
And, notably, in a Turing machine there is no distinction between code and data.
In practice programming languages assume the ability to perform arithmetic, create and iterate through lists, perform side effects, and other sophisticated operations for readability and efficiency.
But ultimately, they all reduce to the lambda calculus, and I hope this essay was able to hint at how and why.