Exercise 2.6: Church Numerals

Exercise 2.6 Define one and two directly (not in terms of zero and add-1).

The exercise gives the following definitions of zero and add-1

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

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

OK. Not that I understand how these represent zero and add-1, because trying to evaluate them just returns a procedure.

zero

;Value 22: #[compound-procedure 22 zero]

(add-1 zero)

;Value 23: #[compound-procedure 23]

Still, I'll play along. I'll use the substitution rules to figure out one and two.

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

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

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

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

At this point i can see a pattern emerge. I'm going to venture a guess that three would look like this:

(define three
    (lambda (f) (lambda (x) (f (f (f x)))))

So I don't really know what I did or how to verify whether its right. A little googling reveals a great page on this exercise by Bill the Lizard. And (surprise!) it looks like my substitutions above came out OK.

Reading over Bill's solution, I realize I forgot to define add. So I try not to look at Bill's solution, and work on my own. I do crib Bill's suggestion on how to test these numbers with inc.

So, I start looking at the pattern closer. I know that

(add zero one)

should result in

(lambda (f) (lambda (x) (f x)))

and that

(add one one)

should result in

(lambda (f) (lambda (x) (f (f x))))

And just to make sure I understand what's going on, I define add-2

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

This seems to work based on my
inc test.

(((add-2 zero) inc) 0)

;Value: 2

I have a procedure to increase the value of a number. I need to generalize it so that I can increase it value of a number a b times. As it turns out, this "number" b is a procedure which repeats another procedure. So I'll just apply b to (a f) like this.

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

This look promising at first, but, until I get to adding two and two.

(((add zero one) inc) 0)

;Value: 1

(((add one one) inc) 0)

;Value: 2

(((add one two) inc) 0)

;Value: 3

(((add two two) inc) 0)

;Value: 5

(((add two zero) inc) 0)

;Value: 1

(((add two one) inc) 0)

;Value: 3

So I played around with it until my head hurt. In the end, I read the end of Bill's article. The final solution is this.

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

Now that I see it, it makes sense. I need b applications of f to ((a f) x), and the way to do this is with the procedure(b f), which will result in the application of procedure f b times. The repeated application of this procedure should be applied to ((a f) x).

Definitely one of the hardest problems I've encountered. I'll have to do some study on church numbers and come back to it.