Natural Numbers as Church Numerals
----------------------------------

Natural numbers are non-negative. Given a successor function, succ, 
which adds one, we can define the natural numbers in terms of
zero and succ:

    1 = (succ 0)
    2 = (succ 1)
      = (succ (succ 0))
    3 = (succ 2)
      = (succ (succ (succ 0)))

and so on. Therefore a number n will be that number of
successors of zero. Just as we adopted the convention TRUE = first,
and FALSE = second, we adopt the following convention:

     zero  = Lf.Lx.x
     one   = Lf.Lx.(f x)
     two   = Lf.Lx.(f (f x))
     three = Lf.Lx.(f (f (f x)))
     four  = Lf.Lx.(F (f (f (f x))))


Therefore we have a "unary" representation of the natural
numbers, such that n is represented as n applications of the
function f to the argument x. This representation is refered to as
CHURCH NUMERALS. 

We can define the function succ as follows:

  succ = Ln.Lf.Lx.(f ((n f) x))

and therefore one as follows:

  one = (succ zero)
      => (Ln.Lf.Lx.(f ((n f) x)) zero)
      => Lf.Lx.(f ((zero f) x))
      => Lf.Lx.(f ((Lg.Ly.y f) x)) (* alpha conversion avoids clash *)
      => Lf.Lx.(f (Ly.y x))
      => Lf.Lx.(f x)

and two as follows:

  two = (succ one)
      => (Ln.Lf.Lx.(f ((n f) x)) one)
      => Lf.Lx.(f ((one f) x))
      => Lf.Lx.(f ((Lg.Ly.(g y) f) x)) (* again, alpha conversion *)
      => Lf.Lx.(f (Ly.(f y) x)
      => Lf.Lx.(f (f x))

val succ = fn n => fn f => fn x => (f ((n f) x));

NOTE that ((two g) y) = (g (g y)). So if we had some function, say
one that increments n:
 
   inc = Ln.(n+1)

then we can get a feel for a Church Numeral as follows:

   ((two inc) 0)
   => ((Lf.Lx.(f (f x)) inc) 0)
   => (Lx.(inc (inc x) 0)
   => (inc (inc 0))
   => (Ln.(n+1) (Ln.(n+1) 0))
   => (Ln.(n+1) (0 + 1))
   => ((0 + 1) + 1)
   => 2

We are now in a position to define addition in terms of succ:

   add = Lm.Ln.Lf.Lx.((((m succ) n) f) x);

Therefore four may be computed as follows:

   four = ((add two) two)
        => ((Lm.Ln.Lf.Lx.((((m succ) n) f) x) two) two)
        => (Ln.Lf.Lx.((((two succ) n) f) x)
        => Lf.Lx.((((two succ) two) f x)
        => Lf.Lx.((((Lg.Ly.(g (g y)) succ) two) f x)
        => Lf.Lx.(((Ly.(succ (succ y)) two) f) x)
        => Lf.Lx.(((succ (succ two)) f) x)
        => Lf.Lx.(((succ (Ln.Lf.Lx.(f ((n f) x)) two)) f) x)


Multiplication is defined as follows:

   mult = Lm.Ln.Lx.(m (n x))

   six  = ((mult two) three)
        => ((Lm.Ln.Lx.(m (n x)) two) three)
        => (Ln.Lx.(two (n x) three)
        => Lx.(two (three x))
        => Lx.(two (Lg.Ly.(g (g (g y))) x))
        => Lx.(two Ly.(x (x (x y))))
        => Lx.(Lf.Lz.(f (f z)) Ly.(x (x (x y))))
        => Lx.Lz.(Ly.(x (x (x y))) (Ly.(x (x (x y))) z))
        => Lx.Lz.(Ly.(x (x (x y))) (x (x (x z))))
        => Lx.Lz.(x (x (x (x (x (x z))))))


And exponentiation as follows:

    power = Lm.Ln.(m n);

    nine  = ((power two) three)
          => ((Lm.Ln.(m n) two) three)
          => (Ln.(two n) three)
          => (two three)
          => (Lf.Lx.(f (f x)) three)
          => Lx. (three (three x))
          => Lx. (three (Lg.Ly.(g (g (g y))) x))
          => Lx. (three Ly.(x (x (x y))))
          => Lx. (Lg.Lz.(g (g (g z))) Ly.(x (x (x y))))
          => Lx.Lz.(Ly.(x (x (x y))) 
                    (Ly.(x (x (x y)))
                     (Ly.(x (x (x y))) z)))
          => Lx.Lz.(Ly.(x (x (x y)))
                    (Ly.(x (x (x y)))
                      (x (x (x z)))))
          => Lx.Lz.(Ly.(x (x (x y)))
                     (x (x (x (x (x (x z)))))))
          => Lx.Lz.(x (x (x (x (x (x (x (x (x z)))))))))


The following lambda function tests for zero:

   third = Lx.Ly.Lz.z
   iszero = Ln.((n third) first)


And the lambda function pred delivers the predecessor of a
Church Numeral:


    pair = Lx.Ly.Lf.((f x) y);
    prefn = Lf.Lp.((pair (f (p first))) (p first))
    pred = Ln.Lf.Lx.(((n (prefn f)) (pair x x)) second)

   
It should be of interest to note the following. A major
landmark in Lambda Calculus occurred in the 1930's when
Kleene discovered how to express the operation of
subtraction within Church's scheme (yes, that means that even
though Church invented/discovered the Lambda Calculus he was
unable to implement subtraction and subsequently division, within
that calculus)! Other landmarks then followed, such as the recursive 
function Y. In 1937 Church and Turing, independently, showed that every 
computable operation (algorithm) can be achieved in a Turing machine
and in the Lambda Calculus, and therefore the two are equivalent.  
Similarly Godel introduced his description of computability, again 
independently, in 1929, using a third approach which was again shown 
to be equivalent to the other 2 schemes.

It appears that there is a "platonic reality" about
computability. That is, it was "discovered" (3 times idepenedently)
rather than "invented". It appears to be natural in some
sense.


(********************** ml source ***********************)

(* Church Numerals *)

val zero = fn f => fn x => x;
val succ = fn n => fn f => fn x => (f ((n f) x));
val add = fn m => fn n => fn f => fn x => ((((m succ) n) f) x);
val mult = fn f => fn g => fn x => (f (g x));
val power = fn f => fn g => (f g);

(* Church Numerals *)
val one = (succ zero);
val two = (succ one);

val inc = fn n => n+1;

(* More Church Numerals *)
val four = (add one (add one (add one (add one zero))));
val three = ((add one) two);
val five = ((add three) two);
val six = ((mult three) two);
val nine = ((power two) three);
val ten = ((mult two) five);

(* A test to show what a Church Numeral does *)

((zero inc) 0);
((five inc) 0);
((ten inc) 0);

val first = fn x => fn y => x;
val second = fn x => fn y => y;
val third = fn x => fn y => fn z => z;

val iszero = fn n => ((n third) first);
(* Predicate, is a Church Numeral zero? *)

val pair = fn x => fn y => fn f => ((f x) y);

val prefn = fn f => fn p => ((pair (f (p first))) (p first));
val pred = fn n => fn f => fn x => (((n (prefn f))(pair x x)) second);
(* predecessor function *)

val eight = (pred nine);