From: stone@hilbert.math.grin.EDU (John David Stone)
Subject: Church numerals
Organization: The Internet
Date: Thu, 13 Aug 1992 13:48:34 GMT

        Here's the classic approach to arithmetic with Church numerals:

(define zero
  (lambda (x)
    (lambda (y) y)))

(define successor
  (lambda (u)
    (lambda (x)
      (lambda (y) (x ((u x) y))))))

(define one (successor zero))

(define add
  (lambda (m)
    (lambda (n)
      (lambda (f)
        (lambda (x) ((m f) ((n f) x)))))))

(define mult
  (lambda (m)
    (lambda (n)
      (lambda (f) (m (n f))))))

(define power
  (lambda (m)
    (lambda (n) (n m))))

        And for direct definition of recursive functions (without Y,
incidentally!):

(define constant
  (lambda (x)
    (lambda (y) x)))

(define ordered-pair
  (lambda (x)
    (lambda (y)
      (lambda (z) ((z (constant y)) x)))))

The idea of the ordered-pair notation is that ((ordered-pair x) y) is a
function that yields x when applied to zero and y when applied to any other
Church numeral, thus giving the effect of a test for equality with zero.

(define extender
  (lambda (y)
    (lambda (v)
      ((ordered-pair (successor (v zero))) ((y (v zero)) (v one))))))

You can think of extender as a function that takes a function y and an
ordered pair v, where v's two elements are a counter and a previously
generated value, and yields an ordered pair consisting of the counter
incremented once and a value obtained by applying y to the old value of
the counter and the previously generated value.

(define recurser
  (lambda (x)
    (lambda (y)
      (lambda (u)
        (((u (extender y)) ((ordered-pair zero) x)) one)))))

Recurser takes an initial value x, a transition function y, and a Church
numeral u and delivers the result of applying the transition function to
the initial value u times in succession.  (Actually, you think of y as
applying to two arguments to give its value -- the count of the number
of times it's been applied previously, and the value resulting from those
earlier applications.)

        Now recursive definitions simply fall out of applications of
recurser:

(define recursive-add
  (lambda (n) ((recurser n) (constant successor))))

(define recursive-multiply
  (lambda (n) ((recurser zero) (constant (recursive-add n)))))

(define recursive-power
  (lambda (m)
    (lambda (n) (((recurser one) (constant (recursive-multiply m))) n))))

(define factorial
  ((recurser one) (lambda (x) (recursive-multiply (successor x)))))

        In testing these, you may find the following Scheme procedures
useful:

(define int->Church
  (lambda (n)
    (if (zero? n)
        zero
        (successor (int->Church (- n 1))))))

(define Church->int
  (lambda (numeral)
    ((numeral (lambda (x) (+ 1 x))) 0)))

as in:

(Church->int (factorial (int->Church 4)))

(Church->int ((recursive-power (int->Church 5)) (int->Church 3)))

which yield 24 and 125 respectively.

        I found the idea behind extender and recurser in Hindley and
Seldin's _Introduction to Combinators and the Lambda-Calculus_, where it is
ascribed to the logician P. Bernays.

------  John David Stone - Lecturer in Computer Science and Philosophy  -----
--------------  Manager of the Mathematics Local-Area Network  --------------
--------------  Grinnell College - Grinnell, Iowa 50112 - USA  --------------
--------  stone@math.grin.edu - (515) 269-3181 - stone@grin1.bitnet  --------