Q:

Church Numerals - implement one, two, and addition

Given the following exercise:

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

I wrote this solution.  I'm not 100% certain what the correct answer is, and I'm not sure the best way to check my solution so it's possible that I have made a mistake in my answer.  Please let me know what you think.
;given definitions
(define zero (lambda (f) (lambda (x) x)))
(define (add-1 n)
  (lambda (f) (lambda (x) (f ((n f) x)))))
; exercise 2.6: define one and two directly -
; not in terms of zero or add-1
(define one
  (lambda (f) (lambda (x) (f (f x)))))
(define two
  (lambda (f) (lambda (x) (f ((f (f x)) x)))))

(define (church-plus a b)
  (define (church-num n)
    (cond ((= 0 a) (lambda (x) x))
          ((= 1 a) (lambda (f) (lambda (x) (f ((n f) x)))))
          (else (church-num (- n 1)))))
  (church-num (+ a b)))

A:

Church defined numerals as the repeated application of a function.  The first few numerals are defined thus:
(define zero (lambda (f) (lambda (x) x)))
(define one (lambda (f) (lambda (x) (f x))))
(define two (lambda (f) (lambda (x) (f (f x)))))

... and so on.
To see how one is derived, begin by defining one as (add-1 zero) and then perform the applications in order as shown in the steps below (I have written each function to be applied and its single argument on separate lines for clarity):
;; Givens
(define add-1 (lambda (n) (lambda (f) (lambda (x) (f ((n f) x))))))
(define zero (lambda (f) (lambda (x) x)))

(define one
  (add-1    ;; substitute with definition of add-1
   zero))

(define one
  ((lambda (n)    ;; apply this function to argument zero
     (lambda (f) (lambda (x) (f ((n f) x)))))
   zero))

(define one
  (lambda (f) (lambda (x) (f ((zero    ;; substitute with definition of zero
                               f) x)))))

(define one
  (lambda (f) (lambda (x) (f (((lambda (f)    ;; apply this function to argument f
                                 (lambda (x) x))
                               f)
                              x)))))

(define one
  (lambda (f) (lambda (x) (f ((lambda (x)    ;; apply this function to argument x
                                x)
                              x)))))

(define one
  (lambda (f) (lambda (x) (f x))))    ;; we're done!

You may try your hand at two in a similar fashion. =)
By definition, Church numerals are the repeated application of a function.  If this function were the integer increment function and the initial argument were 0, then we could generate all natural numbers 0, 1, 2, 3, ....  This is an important insight.
Thus, a Church numeral is a function that takes one argument, the increment function, and returns a function that also takes one argument, the additive identity.  Thus, if we were to apply a Church numeral to the integer increment function (lambda (n) (+ 1 n)) (or simply add1 in Scheme), which we then apply to the integer additive identity 0, we would get an integer equivalent to the Church numeral as a result.  In code:
(define (church-numeral->int cn)
  ((cn add1) 0))

A few tests:
> (church-numeral->int zero)
0
> (church-numeral->int one)
1
> (church-numeral->int two)
2
> (church-numeral->int (add-1 two))
3
> (church-numeral->int (add-1 (add-1 two)))
4

A Church-numeral addition should take two Church numerals as input, and not integers, as in your code.
We use the insight above about increment functions and additive identities to notice that integer addition is simply repeated incrementing.  If we wish to add integers a and b, we begin with the number b and increment it a times to get a + b.
The same applies to Church numerals.  Instead of using integer increment function and integer additive identity, we use the Church increment function add-1 and we begin with a Church numeral as the additive identity.  Thus, we can implement Church-numeral addition as:
(define (plus cn-a cn-b)
  ((cn-a add-1) cn-b))

A few examples:
(define three (plus one two))
(define four (plus two two))
(define five (plus two three))
(define eight (plus three five))

... and associated tests:
> (church-numeral->int three)
3
> (church-numeral->int four)
4
> (church-numeral->int five)
5
> (church-numeral->int eight)
8

