# Church numerals

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

(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 + ( `add` ) (not in terms of repeated application of `add-1` ).

##### Authentication required

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

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

(define (inc x) (+ x 1))

(define (church->nat n) ((n inc) 0))

(check-equal? (church->nat zero) 0)
(check-equal? (church->nat one) 1)
(check-equal? (church->nat two) 2)
(check-equal? (church->nat (add one one)) 2)
(check-equal? (church->nat (add two one)) 3)