#
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)))
(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 + (
`add`

) (not in terms of repeated application of
`add-1`

).

```
(define zero (lambda (f) (lambda (x) x)))
(define (add-1 n)
(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)
(check-equal? (church->nat (add (add two one) zero)) 3)
(check-equal? (church->nat (add (add two one) one)) 4)
```