(Make sure you understand higher-order functions). In Alonzo Church's untyped lambda calculus a function is the only primitive data type. There are no numbers, booleans, lists or anything else, only functions. Functions can have only 1 argument, but functions can accept and/or return functions—not values of these functions, but functions themselves. Therefore to represent numbers, booleans, lists and other types of data, you must come up with a clever way for anonymous functions to stand for them. Church numerals is the way to represent natural numbers. Three most primitive constructs in untyped lambda calculus are:
λx.x
, an identity function, accepts some function and immediately returns it.
λx.x x
, self-application.
λf.λx.f x
, function application, takes a function and an argument, and applies a function to an argument.
How do you encode 0, 1, 2 as nothing else but functions? We somehow need to build the notion of quantity into the system. We have only functions, every function can be applied only to 1 argument. Where can we see anything resembling quantity? Hey, we can apply a function to a parameter multiple times! There's obviously a sense of quantity in 3 repeated invocations of a function: f (f (f x))
. So let's encode it in lambda calculus:
- 0 =
λf.λx.x
- 1 =
λf.λx.f x
- 2 =
λf.λx.f (f x)
- 3 =
λf.λx.f (f (f x))
And so on. But how do you go from 0 to 1, or from 1 to 2? How would you write a function that, given a number, would return a number incremented by 1? We see the pattern in Church numerals that the term always starts with λf.λx.
and after you have a finite repeated application of f, so we need to somehow get into the body of λf.λx.
and wrap it into another f
. How do you change a body of an abstraction without reduction? Well, you can apply a function, wrap the body in a function, then wrap the new body into the old lambda abstraction. But you don't want arguments to change, therefore you apply abstractions to the values of the same name: ((λf.λx.f x) f) x → f x
, but ((λf.λx.f x) a) b) → a b
, which is not what we need.
That's why add1
is λn.λf.λx.f ((n f) x)
: you apply n
to f
and then x
to reduce the expression to the body, then apply f
to that body, then abstract it again with λf.λx.
. Exercise: too see that it's true, quickly learn β-reduction and reduce (λn.λf.λx.f ((n f) x)) (λf.λx.f (f x))
to increment 2 by 1.
Now understanding the intuition behind wrapping the body into another function invocation, how do we implement addition of 2 numbers? We need a function that, given λf.λx.f (f x)
(2) and λf.λx.f (f (f x))
(3), would return λf.λx.f (f (f (f (f x))))
(5). Look at 2. What if you could replace its x
with the body of 3, that is f (f (f x))
? To get body of 3, it's obvious, just apply it to f
and then x
. Now apply 2 to f
, but then apply it to body of 3, not to x
. Then wrap it in λf.λx.
again: λa.λb.λf.λx.a f (b f x)
.
Conclusion: To add 2 numbers a
and b
together, both of which are represented as Church numerals, you want to replace x
in a
with the body of b
, so that f (f x)
+ f (f (f x))
= f (f (f (f (f x))))
. To make this happen, apply a
to f
, then to b f x
.