Arithmetic with Church Numerals

Question

I am working through SICP, and the problem 2.6 has put me in something of a quandary. In dealing with Church numerals, the concept of encoding zero and 1 to be arbitrary functions that satisfy certain axioms seems to make sense. Additionally, deriving the direct formulation of individual numbers using the definition of zero, and an add-1 function makes sense. I do not understand how a plus operator can be formed.

Thus far I have this.

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

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

Looking through the wikipedia entry for lambda calculus, I found that the definition of plus was PLUS := λmnfx.m f (n f x). Using that definition I was able to formulate the following procedure.

(define (plus n m)
  (lambda (f) (lambda (x) ((m f) ((n f) x)))))

What I don't understand, is how that procedure can be derived directly using only the information given by the previously derived procedures. Can anyone answer this in some kind of rigorous proof-like form? Intuitively, I think I understand what's going on, but as Richard Feynman once said, "If I can't build it, I can't understand it..."

Answer 1

It's actually pretty simple. This will probably be viewed as flamebait, but the parens make it harder to see -- a better way to see what happens is either imagine that you're in a curried language, or just use the fact that Scheme has multi-argument functions and embrace that... Here's an explanation that uses lambdas and multiple argument where convenient:

• Every number N is encoded as

  (lambda (f x) ...apply (f (f (f ... (f x)))) N times...)
  

• This means that the encoding of N is actually

  (lambda (f x) (f^N x))
  

  where f^N is functional exponentiation.

• A simpler way to say this (assuming currying): the number N is encoded as

  (lambda (f) f^N)
  

  so N is actually a "raise to the power of N" function

• Now take your expression (looking inside the lambdas here):

  ((m f) ((n f) x))
  

  since n is is an encoding of a number, it's that exponentiation, so this is actually:

  ((m f) (f^n x))
  

  and the same for m:

  (f^m (f^n x))
  

  and the rest should be obvious... You have m applications of f applied on n applications of f applied on x.

• Finally, to leave some fun -- here's another way to define plus:

  (define plus (lambda (m) (lambda (n) ((m add1) n))))
  

  (Well, not too much fun, since this one is probably more obvious.)