;; church.scm --- simple demonstration of Church numerals
;; Author: Noah Friedman <friedman@prep.ai.mit.edu>
;; Created: 1995-03-21
;; Public domain

;; $Id: church.scm,v 1.7 1995/04/13 02:50:36 friedman Exp $

;;; Commentary:

;; The following functions are presently defined on zero and all
;; successors: successor, predecessor, sum, difference, product, divide,
;; modulus, power, and factorial.  In addition, some control constructs are
;; defined, namely if-zero, if-equal, and if-less-than.  All use nothing
;; but the lambda calculus.

;; The functions church->arabic and arabic->church will perform the
;; appropriate conversion between arabic and church numerals.

;;; Code:

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

(define successor
  (lambda (n)
    (lambda (f x)
      (n f (f x)))))

;; This function uses a pair to keep track of two values: a flag indicating
;; whether this is the first composition, and a successor value which will
;; ultimately be n-1.  The reason why the first composition is special is
;; that it is composed n times, each nested level returning the successor
;; of the previous number returned.  We can easily generate the nth order
;; composition of this function using n itself.  But we only want to take
;; the successor n-1 times, so the first time we do nothing.
;;
;; Claim: for all numerals n, (predecessor (successor n)) = n and
;; if n is not zero, then (successor (predecessor n)) = n.
;; I.e., (successor (predecessor n) n) = (if-zero n (successor zero) n).
;;
;; We allow (predecessor zero) to be zero to avoid having to deal with ways
;; to signal a domain error (ideally predecessor is only defined on
;; (successor zero) and higher), which would be considerably more complicated.
(define predecessor
  (lambda (n)
    (pair-second (n (lambda (x)
                      (if-zero (pair-first x)
                               (pair (successor zero) zero)
                               (pair (successor zero)
                                     (successor (pair-second x)))))
                    (pair zero zero)))))

(define sum
  (lambda (m n)
    (m successor n)))

(define difference
  (lambda (m n)
    (n predecessor m)))

(define product
  (lambda (m n)
    (m (lambda (x)
         (sum n x))
       zero)))

;; `quotient' is an R4RS essential procedure, so don't redefine it.
;; Note that if n=zero, this function will never return.
;; (Actually, it will return one if m=n=zero, but who cares.)
(define divide
  (lambda (m n)
    ((Y (lambda (f)
          (lambda (k)
            ((if-equal m k
                       (lambda () (successor zero))
                       (lambda ()
                         ((if-zero (difference m k)
                                   (lambda () zero)
                                   (lambda ()
                                     (successor (f (sum k n))))))))))))
     n)))

;; the remainder of m/n
(define modulus
  (lambda (m n)
    (difference m (product (divide m n) n))))

;; returns m^n
(define power
  (lambda (m n)
    (n (lambda (x)
         (product m x))
       (successor zero))))

;; This starts to get pretty slow around (factorial nine) on a sparc10
(define factorial
  (lambda (n)
    ((if-zero n
              (lambda () (successor zero))
              (lambda () (product n (factorial (predecessor n))))))))


;; Return f if numeral n is equivalent to zero, g otherwise.
(define if-zero
  (lambda (n f g )
    (n (lambda (x) g) f)))

;; return f if numerals m and n are equivalent, g otherwise.
;; Note we must compute two differences since even if n is larger than m,
;; the difference is still zero because we do not have negative numbers.
(define if-equal
  (lambda (m n f g)
    ((if-zero (difference m n)
              (lambda () (if-zero (difference n m) f g))
              (lambda () g)))))

;; Return f if m<n, g otherwise.
(define if-less-than
  (lambda (m n f g)
    ((if-zero (difference m n)
              (lambda () (if-zero (difference n m) g f))
              (lambda () g)))))


;; helper functions

;; The Y combinator is used to create anonymous recursive functions.
;; It would take too long to explain how it works here, but the interested
;; reader is referred to Joseph E. Stoy, "Denotational Semantics" (1977),
;; for more information.
(define Y
  (lambda (f)
    ((lambda (g) (f (lambda (x) ((g g) x))))
     (lambda (g) (f (lambda (x) ((g g) x)))))))

;; lambda calculus analogue of a cons
(define pair
  (lambda (a b)
    (lambda (x)
      (if-zero x a b))))

;; return the first element of a pair
(define pair-first (lambda (x) (x zero)))

;; return the second element of a pair
(define pair-second (lambda (x) (x (successor zero))))

(define church->arabic
  (lambda (c) (c 1+ 0)))

(define arabic->church
  (lambda (n)
    (if (zero? n)
        zero
        (successor (arabic->church (1- n))))))


;; Define a few church numerals just to have something to play with.

(define one   (successor zero))
(define two   (successor one))
(define three (successor two))
(define four  (successor three))
(define five  (successor four))
(define six   (successor five))
(define seven (successor six))
(define eight (successor seven))
(define nine  (successor eight))
(define ten   (successor nine))

;; define the first few squares not already defined
(define sixteen     (power four  two))
(define twenty-five (power five  two))
(define thirty-six  (power six   two))
(define forty-nine  (power seven two))
(define sixty-four  (power eight two))
(define eighty-one  (power nine  two))
(define one-hundred (power ten   two))

;;; church.scm ends here