New Syntax
----------

 (<name> <argument>) == (<function> <argument>)

 Where == indicates the replacement of <name> by its associated <function>

 (<function> <argument>) => <expression>

 Where => means that in the function application, the bound variable in 
 <function> is replaced with the "unevaluated" <argument>.
 This is "normal order beta reduction". This is the same as "call-by-name".

 (<function> <argument>) -> <expression>

 Where -> means that in the function application, the bound variable in 
 <function> is replaced with the "evaluated" <argument>.
 This is "applicative order beta reduction". This is the same as "call-by-value".


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!
 

 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?). 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))))

 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))))  |
  |                                                                           |
  -----------------------------------------------------------------------------

 (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)))
      -> ((times three)
          ((fact1 (Ls.(fact1 (s s)) Ls.(fact1 (s s)))) (pred three)))
      -> ((times three)
          ((Lf.Ln.(((IF (iszero n)) one) ((times n) (f (pred n))))
            (Ls.(fact1 (s s)) Ls.(fact1 (s s)))) (pred three)))
      => ((times three)
          (((IF (iszero (pred three))) one) ((times (pred three))
              ((Ls.(fact1 (s s)) Ls.(fact1 (s s))) (pred (pred three))))))