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.)

Answer 2

^{(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:

1. λx.x, an identity function, accepts some function and immediately returns it.
2. λx.x x, self-application.
3. λ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.

Answer 3

Eli's answer is technically correct but since at the point that this question is asked the #apply procedure has not been introduced, I don't think that the authors intended the student to have knowledge of that or of concepts such as currying to be able to answer this question.

They pretty much guide one to the answer by suggesting that one apply the substitution method, and then from there one should notice that the effect of the addition is a composition of one number onto the other. Composition is a concept was introduced in exercise 1.42; and that's all that is required to understand how an additive procedure can work in this system.

; The effect of procedure #add-1 on `one`, and `two` was the composition of `f` 
; onto `one` and `f` onto `two`.
;
; one   : (λ (f) (λ (x) (f x)))
; two   : (λ (f) (λ (x) (f (f x))))
; three : (λ (f) (λ (x) (f (f (f x)))))
;
; Thus one may surmise from this that an additive procedure in this system would
; work by composing one number onto the other.
;
; From exercise 1.42 you should already have a procedure called #compose.
;
; With a little trial and error (or just plain be able to see it) you get the
; following solution.

(define (adder n m)
  (λ (f)
    (let ((nf (n f))
          (mf (m f)))
      (compose nf mf))))