Lambda Calculus, Pt. 1

If you haven't read the introduction, read that first. It goes over what lambda calculus is, as well as the syntax I'll be using throughout this post.

Natural Numbers

There are various ways to encode natural numbers (whole numbers ≥ 0) in lambda calculus. The most common is using Church numerals, where:

• 0 = (λx,y -> y)
• 1 = (λx,y -> (x y))
• 2 = (λx,y -> (x (x y)))
• 3 = (λx,y -> (x (x (x y))))

...and so on. We can think of this encoding a number N by applying the first function N times to the second function.

One of the most important functions on natural numbers is the successor function, which takes a natural number a and returns the next natural number a+1. This can be implemented as follows:

(succ a) = (λx,y -> (x (a x y)))

Essentially, we:

• "set up" a number by creating a function of 2 variables (λx,y ->
• "get" the expression inside a by applying the 2 variables to it (a x y)
• apply x one more time (x

For example,

(succ 2)
= (λx,y -> (x (2 x y)))
= (λx,y -> (x (x (x y))))
= 3

The above definition would be acceptable in Haskell, but to make this a proper lambda calculus expression, we need to abstract a as a function parameter:

succ = (λa -> (λx,y -> (x (a x y))))

However, abstracting is a trivial step and makes it harder to understand the expression, so I won't abstract any of the future definitions.

Basic Arithmetic

Using the same idea as succ, we can write a function add3:

(add3 a) = (λx,y -> (x (x (x (a x y)))))

Or, we can simply use succ as previously defined:

(add3 a) = (succ (succ (succ a)))

Remember that named functions don't exist in lambda calculus. The above is just a shorthand for inserting the full definition of succ 3 times. In fact, doesn't applying a function N times sound familiar? We can rewrite add3 as:

(add3 a) = (3 succ a)

To be explicit, this applies succ 3 times to a, which is exactly what we want. We can use this to implement the general function add, which sums two natural numbers together.

(add a b) = (a succ b)

Pretty cool, eh? Try to think about how to define mult next. There's one implementation using add, and a simpler one using a construction similar to succ.

• (mult a b) = (a (add b) 0)

This one was more intuitive for me. This simply applies (add b) to 0, a times. For example,

(mult 3 2)
= (add 3 (add 3 0))
= (add 3 3)
= 6

The other implementation is more clever.

• (mult a b) = (λx,y -> (a (b x) y))

Similar to succ, we first "construct" a number by accepting two variables, then apply (b x) to y, a times. For example,

(mult 3 2)
= (λx,y -> (3 (2 x) y)
= ((2 x) ((2 x) (2 x y)))
= ((2 x) ((2 x) (x (x y))))
= (x (x (x (x (x (x y))))))
= 6

We can think of it as applying (2 x) = (x (x three times to y.

How about exponentiation? Again, there's the intuitive implementation:

(exp b e) = (e (mult b) 1)

which simply applies (mult b) to 1, e times. The clever implementation is even simpler than mult:

(exp b e) = (e b)

Essentially, we apply the base to itself... e times. This can be a bit confusing, so I'll work out (3 2).

(3 2)
= (λy -> (3 (3 y)))
= (λy -> (λz -> ((3 y) ((3 y) ((3 y) z)))))¹
= (λy -> (λz -> ((3 y) ((3 y) (y (y (y z))))))

which we can see evaluates correctly to 9. The trick is that we need to generate ((3 y) 3 times in order to get 3*3, and for larger exponents, we just generate that 3 times (and continue on as necessary). If we were doing (3 4) instead, the first application would give us:

(λy -> (3 (3 (3 (3 y)))))

which applies the chains of ((3 y) 3 times, and then does that 4 times onto z, resulting in 81.

Whew! I recommend working some of these examples out manually to improve your intuition. Next we'll cover booleans and pairs, which will help us define logical operators as well as subtraction.