Definition of a Recursive Function
----------------------------------

Clearly, what we would like is something of the form

 fact = Ln.(((IF (iszero n)) one) ((times n) (fact (pred n))))

That is, we would like to be able to recursively define functions.
Unfortunately, the lambda calculus will not allow the above because 
"all names in expressions are replaced with their definitions before the 
expression is evaluated." In the above example:

 fact = Ln.(((IF (iszero n)) one) ((times n) (fact (pred n))))
      == Ln.(((IF (iszero n)) one) ((times n)
          (Ln.(((IF (iszero n)) one) ((times n) (fact (pred n)))) (pred n))))
      == Ln.(((IF (iszero n)) one) ((times n)
          (Ln.(((IF (iszero n)) one) ((times n)
           (Ln.(((IF (iszero n)) one) ((times n) 
              (fact (pred n)))) (pred n)))) (pred n))))
      == .....

It doesnae terminate Jimmy!


A Constructor Function, Y
-------------------------
A more general approach to recursion is to find a constructor function to 
build a recursive function from a non-recursive function, with a single 
abstraction at the recursion point.

For example we would hope to do as follows:

 fact = Lf.Ln.(((IF (iszero n)) one) ((times n) (f (pred n))))

Therefore we have removed self reference at the abstraction point with f. 
f is the abstraction point, and we would hope to substitute fact for f. 
That is we hope that we can say that:

  factorial = (fact fact)

Unfortunately this does not give us what we want:

   (fact fact)
    => (Lf.Ln.(((IF (iszero n)) one) ((times n) (f (pred n)))) fact)
    => Ln.(((IF (iszero n)) one) ((times n) (fact (pred n))))
    == Ln.(((IF (iszero n)) one) ((times n)
           (Lf.Ln.(((IF (iszero n)) one) ((times n) (f (pred n)))) (pred n))))

We are now in the situation where we want to make the reduction that replaces 
f with (pred n). This is not what we want. What we would like is
some function, lets call it "recursive", that constructs a recursive function:

    factorial = (recursive fact)

This function "recursive" is refered to as Y 

 Y = Lf.(Ls.(f (s s)) Ls.(f (s s)))

 (Y g) = (Lf.(Ls.(f (s s)) Ls.(f (s s))) g)
       => (Ls.(g (s s)) Ls.(g (s s)))
       => (g (Ls.(g (s s)) Ls.(g (s s))))
       = (g (Y g))

Therefore, we can replace (Y g) with (g (Y g)). More generally, 

  (Y g) => (g (Y g))
        -> (g (g (Y g)))
        -> (g (g (g (Y g))))
        :
        :
        -> (g (g (g ... (g (g (Y g))) ...)))

Therefore, in some ways we've got what we want (recursive applications
of g) but in others we have too much (a monster! how do we prevent an
infinite series of nested applications of g when we use applicative order?). 
Clearly if we are simply using applicative order (call-by-value) the function 
application (Y g) will not terminate.


Example, Factorial
------------------

 fact1 = Lf.Ln.(((IF (iszero n)) one) ((times n) (f (pred n))))

Therefore we have used abstraction, by the use of Lf, and f at the recursion 
point (f (pred n)). Therefore

 fact = (Y fact1)

 In above, replace Y with its definition
           Y = Lf.(Ls.(f (s s)) Ls.(f (s s)))
           to give:

      == (Lf.(Ls.(f (s s)) Ls.(f (s s))) fact1)
 
 In above, replace f 
           in Lf.(Ls.(f (s s)) Ls.(f (s s)))
           with the argument fact1 
           to give:

      => (Ls.(fact1 (s s)) Ls.(fact1 (s s)))

 In above, replace s 
           in Ls.(fact1 (s s))
           with the argument Ls.(fact1 (s s))
           to give:

      => (fact1 (Ls.(fact1 (s s)) Ls.(fact1 (s s))))

 In above, replace the first instance of fact1 with its definition
           fact1 = Lf.Ln.(((IF (iszero n)) one) ((times n) (f (pred n))))
           to give:

      == (Lf.Ln.(((IF (iszero n)) one) ((times n) (f (pred n))))
            (Ls.(fact1 (s s)) Ls.(fact1 (s s))))

 In above, replace f
           in Lf.Ln.(((IF (iszeron)) one) ((times n) (f (pred n))))
           with the argument (Ls.(fact1 (s s)) Ls.(fact1 (s s)))
           to give:

      => Ln.(((IF (iszero n)) one) 
              ((times n) ((Ls.(fact1 (s s)) Ls.(fact1 (s s))) (pred n))))

 And this gives us the definition of factorial, namely


     fact = Ln.(((IF (iszero n)) one)
               ((times n) ((Ls.(fact1 (s s)) Ls.(fact1 (s s))) (pred n))))


For example, we will now try:

 (fact three)
      == (Ln.(((IF (iszero n)) one) 
                ((times n) ((Ls.(fact1 (s s)) Ls.(fact1 (s s))) (pred n))))
            three)
      => (((IF (iszero three)) one) 
                ((times three) ((Ls.(fact1 (s s)) Ls.(fact1 (s s)))
          (pred three))))
      => .......      
      => ((times three)
          ((Ls.(fact1 (s s)) Ls.(fact1 (s s))) (pred three)))

The above step is important. We have used a succession of normal order beta
reductions. To quote from the section "Normal Order Beta Reduction" above:

   "Normal order beta reduction requires the evaluation of the leftmost redex 
    in an  expression. In a function application, evaluate the , 
    then substitute in unevaluated  . That is, the evaluation of 
    the argument is delayed."

Therefore, the left most expression (IF (iszero n)), reduces to (IF FALSE),
which reduces to Lx.Ly.y, which is second. This function application

  ((Lx.Ly.y one) ((times three) ((Ls.(fact1 (s s)) Ls.(fact1 (s s))) 
   (pred three))))

then reduces to 

   ((times three) ((Ls.(fact1 (s s)) Ls.(fact1 (s s))) (pred three)))

We then continue with normal order reduction over the function
application (Ls.(fact1 (s s)) Ls.(fact1 (s s)))

      => ((times three)
          ((fact1 (Ls.(fact1 (s s)) Ls.(fact1 (s s)))) (pred three)))

Replace the first occurence of fact1 with its definition

      == ((times three)
          ((Lf.Ln.(((IF (iszero n)) one) ((times n) (f (pred n)))) 
            (Ls.(fact1 (s s)) Ls.(fact1 (s s))))
           (pred three)))

We now do another (yet another?) reduction replacing f in function expression

  Lf.Ln.(((IF (iszero n)) one) ((times n) (f (pred n))))

with the argument expression

  (Ls.(fact1 (s s)) Ls.(fact1 (s s)))

which gives us 

      => ((times three)
          (Ln.(((IF (iszero n)) one) ((times n)
                ((Ls.(fact1 (s s)) Ls.(fact1 (s s))) (pred n)))) 
             (pred three)))

If we examine the above, the function expression:

    Ln.(((IF (iszero n)) one) ((times n)
                ((Ls.(fact1 (s s)) Ls.(fact1 (s s))) (pred n))))

is of course "fact". Therefore we have:

         ((times three) (fact (pred three)))

Again, we carry out a succession of normal order reductions, which eventually
result in:

      => ((times three)
           ((times two)
             ((fact1 (Ls.(fact1 (s s)) Ls.(fact1 (s s)))) (pred two))))

As might be expected, this ultimately terminates in

      => ((times three)
          ((times two)
           ((times one) one)))


Exhausted?
---------
The function Y is known as a PARADOXICAL COMBINATOR, or a FIXED POINT FINDER.
It should be interesting to note that ml has such a combinator, and it is 
called "rec", for recursive:

    val rec f = fn n => if n=0 then 1 else n*(f(n-1));

and "rec" appears within the language as a reserved word. It would be 
foolish to suggest that the Y operator is simple, or that the "manual" usage 
of Y is simple. However,it is mechanical and it does work. There are simple 
rules for its use, namely beta reduction and definition replacement.

At this point we have now implemented boolean algebra, conditionals,
addition over Church Numerals (the natural numbers), a test for zero, and
the predecessor function. We are therefore in a position to define 
all operations over the natural numbers. In addition, since we have
recursion, we also have iteration and sequential evaluation (we 
have already shown why this is so). However, in order to achieve this
we must exploit normal order beta reduction.