[Lisp]Chruch Number and Common Lisp

墙内地址http://www.jdxyw.com/?p=1098

When we talk about the number,plus,sub or mul, what is the first thing hitting your head? For the most of us, I think, the first thing we think must be 1 2 3, or 1+3=4 or 5-3=2 or something like it. Have you ever thought that we can use other forms to express the number,plus and sub?  This must be strange to use others instead of the normal number, let alone the operation,such as sub, plus.

But, if you have already heard the Lambda Calculus and Church Encoding, then these things seem very reasonable. If you are interested in it, you can read the instruction on Wikipedia. Common Lisp is ideal to implement it.(Actually, Schema is more convenient.)

The brief instruction below comes from wikipeida.

Church numerals are the representations of natural numbers under Church encoding. The higher-order function that represents natural number n is a function that maps any other function f to its n-fold composition. In simpler terms, the “value” of the numeral is equivalent to the number of times the function encapsulates its argument.

Church numerals 0, 1, 2, …, are defined as follows in the lambda calculus:

0 ≡ λf.λx. x1 ≡ λf.λx. f x2 ≡ λf.λx. f (f x)3 ≡ λf.λx. f (f (f x))…n ≡ λf.λx. fⁿ x

The addition function plus(m,n)=m+n uses the identity f^(m + n)(x) = f^m(fⁿ(x)).

plus ≡ λm.λn.λf.λx. m f (n f x)

The successor function succ(n)=n+1 is β-equivalent to (plus 1).

succ ≡ λn.λf.λx. f (n f x)

The multiplication function mult(m,n)=m*n uses the identity f^(m * n) = (f^m)ⁿ.

mult ≡ λm.λn.λf. n (m f)

The exponentiation function exp(m,n)=m^n is straightforward given our definition of church numerals.

exp ≡ λm.λn. n m

The predecessor function  works by generating an n-fold composition of functions that each apply their argument g tof; the base case discards its copy of f and returns x.

pred ≡ λn.λf.λx. n (λg.λh. h (g f)) (λu. x) (λu. u)

The subtraction function can be written based on the predecessor function.

sub ≡ λm.λn. (n pred) m

The zero predicate can be written as:

zero? ≡ λn. n (λx.F) T

From the brief instruction above, we know that the church number is based on the lambda calculus. Actually, all numbers are lambda calculus, or function, this name may be more easily understandable.

(defvar zero
  (lambda(f)
    (lambda(x) x)))

(defun succ(n)
  (lambda(f)
    (lambda(x) (funcall f (funcall (funcall n f) x)))))

(defun plus(m n)
  (lambda (f)
    (lambda(x)(funcall (funcall m f) (funcall (funcall n f) x)))))

(defun mult(m n)
  (lambda (f)
    (funcall n (funcall m f))))

(defun pred(n)
  (lambda (f)
    (lambda (x)
      (funcall (funcall (funcall n (lambda(g)
                    (lambda(h)
                        (funcall h (funcall g f)))))
            (lambda(u) x))
           (lambda(u)u)))))

(defun sub(m n)
  (funcall (funcall n #'pred) m))

(defun cexp(m n)
  (funcall n m))

(defun czerop(n)
  (funcall (funcall n (lambda(x) nil)) t))

(defun int-to-cn(n)
  (if (= n 0)
      (lambda (f)
    (lambda(x) x))
      (lambda (f)
    (lambda (x)
      (funcall f (funcall (funcall (int-to-cn (- n 1)) f) x))))))

(defun cn-to-int(cn)
  (funcall (funcall cn (lambda(x)(+ x 1))) 0))