SICP Exercise 2.6: A Little Churchin' Up

In case representing pairs as procedures wasn't mind-boggling enough, consider that, in a language that can manipulate procedures, we can get by without numbers (at least insofar as nonnegative integers are concerned) by implementing 0 and the operation of adding 1 as

(define zero (lambda (f) (lambda (x) x)))

(define (add-1 n)
  (lambda (f) (lambda (x) (f ((n f) x)))))

This representation is known as Church numerals, after its inventor, Alonzo Church, the logician who invented the λ calculus.

Define one and two directly (not in terms of zero and add-1). (Hint: Use substitution to evaluate (add-1 zero)). Give a direct definition of the addition procedure + (not in terms of repeated application of add-1).

Let's take the hint and run with it...

  (add-1 zero)
= (add-1 (lambda (f) (lambda (x) x)))
= (lambda (f) (lambda (x) (f (((lambda (f) (lambda (x) x)) f) x))))
= (lambda (f) (lambda (x) (f ((lambda (x) x) x))))
= (lambda (f) (lambda (x) (f x)))

That give us a definition for one:

(define one
  (lambda (f) (lambda (x) (f x))))

And we can do the same to figure out two:

  (add-1 one)
= (add-1 (lambda (f) (lambda (x) (f x))))
= (lambda (f) (lambda(x) (f (((lambda (f) (lambda (x) (f x))) f) x))))
= (lambda (f) (lambda(x) (f (((lambda (x) (f x)) x))))
= (lambda (f) (lambda(x) (f (f x))))

So two is:

(define two
  (lambda (f) (lambda (x) (f (f x)))))

Looking at the pattern we can see that the Church numeral representation of the positive integer n is fⁿ(x) (i.e. (f ο f ο…ο f ο f)(x), with n occurrences of f). Also, to assist with the remainder of the exercise, we should note that:

• zero produces a single-parameter lambda expression that ignores its parameter and returns a single-parameter lambda expression that returns its parameter. So we can convert zero to its integer equivalent value using the expression ((zero f) 0), where f is any value.
• one produces a single-parameter, f, lambda expression that returns a new single-parameter lambda expression that returns the results of applying f to its parameter. So, assuming we pass 0 as the parameter to the second lambda expression as with zero, then we can convert one to its integer equivalent value using the expression ((one inc) 0), where inc is the increment procedure defined earlier.
• two produces a single-parameter, f, lambda expression that returns a new single-parameter lambda expression that returns the results of applying f to the results of applying f to its parameter. So similar to one, we can convert two to its integer equivalent value using the expression ((two inc) 0).

We can generalize this to saying that for any Church numeral, n, we can convert it to its integer equivalent value using the expression ((n inc) 0). Here's a procedure that encapsulates this logic which we can use to allow easy testing of our work with Church numerals:

(define (unchurch n)
  ((n inc) 0))

For example:

> (unchurch zero)
0
> (unchurch one)
1
> (unchurch two)
2

Now onto defining + for Church numerals. We know that we want this to produce a valid Church numeral. I.e. a single-parameter lambda expression whose parameter, f, is a procedure and that returns a single-parameter lambda expression. We also know that, given two Church numerals representing the nonnegative integers a and b, we want the evaluation of (((+ a b) f) x) to apply f repeatedly, starting with x as the initial input, for a total of a+b times. How can we do this? Well evaluating ((a f) x) will apply f a total of a times to whatever is passed to it as x, and ((b f) x) will apply f a total of b times to whatever is passed to it as x. So we can produce a composite function that evaluates ((b f) x) and then uses that as the value of x for evaluating ((a f) x) (or vice versa). Here's my definition

(define (+ a b)
  (lambda (f) (lambda (x) ((a f) ((b f) x)))))

And to check it works:

> (unchurch (+ one two))
3
> (unchurch (+ (+ one two) two))
5

Of course we can go much further with Church numerals - there's a whole raft of definitions for various computations. Just for fun I also defined * for Church numerals:

(define (* a b)
  (lambda (f) (lambda (x) ((a (b f)) x))))

And here it is in action:

> (unchurch (* (+ one two) two))
6
> (unchurch (* (+ two two) (+ one two)))
12
> (unchurch (* (* two two) (* one two)))
8