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)