EVALUATION REVISITED
--------------------
We have already seen that:

       (Y g) => (g (Y g))

and that:

       (Y g) -> (g (Y g))
             -> (g (g (Y g)))
             -> (g (g (g ... (Y g) ...)))

That is, in the above scenario, normal order terminates, and applicative
order does not. We also experience the same phenomenon over IF and cond.
This is because in the function application (((IF C) E1) E2),
using applicative order C, E1, and E2 are evaluated. A recursive function
that exploits IF and applicative order (call by value) is unlikely to
terminate.


Delaying Evaluation
-------------------
We can use applicative order and avoid the above phenomenon. We do this by
delaying the evaluation of E1 and E2 in the function application
(((IF C) E1) E2), and we do this by ABSTRACTION.

Consider the following:

   TRUE = Lx.Ly.x

   FALSE = Lx.Ly.y

   IF = Lc.Le1.Le2((c e1) e2)

  (((IF C) Ldummy.E1) Ldummy.E2)

Assume that the bound variable "dummy" does not occur within E1 or in E2.
We have added an extra layer of abstraction. If the condition C is TRUE 
(first, Lx.Ly.x) then we deliver Ldummy.E1, and if the condition C is FALSE
(second, Lx.Ly.y) we deliver Ldummy.E2  However, we must now explicitly
evaluate the result of the the IF, and we can do this via the function 
application:

     ((((IF C) Ldummy.E1) Ldummy.E2) anything)

     == ((((Lc.Le1.Le2.((c e1) e2) C) Ldummy.E1) Ldummy.E2) dummy)
     -> (((C Ldummy.E1) Ldummy.E2) anything)

If C is TRUE we get

     (((Lx.Ly.x Ldummy.E1) Ldummy.E2) anything)
     -> (Ldummy.E1 anything)
     -> E1

and if C is FALSE we get

     (((Lx.Ly.y Ldummy.E1) Ldummy.E2) anything)
     -> (Ldummy.E2 anything)
     -> E2


This technique is adopted in Algol 60 call-by-name, and is refered to as
a "thunk" (why, I don't know). A thunk is a parameterless procedure
which is produced by a call-by-value parameter, to delay evaluation
of that parameter until the parameter is encountered in the procedure's
body.


The Halting Problem
-------------------
Normal order may lead to repetitive argument evaluation, and applicative
order may not terminate. However, normal order might not terminate either:

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

and so on, for ever. In general there is no way of knowing, in advance,
if the evaluation of an expression will ever terminate.

Church (1903 - ) hypothesized that all descriptions of computing were
equivalent. Thus any result for one applies to the others. It has been shown
that for any Turing machine there exists an equivalent L expression.
Thus the undecidability of the halting problem applies equally to the 
lambda calculus.

Church and Rosser have shown that:

 (a) Every expression has a unique normal form.

Thus, if an expression is reduced using two different evaluation orders, and 
both reductions terminate, then both lead to the same normal form.

 (b) If an expression has a normal form, then it may be reached
     by normal order beta reduction.

Thus, if any evaluation order will terminate, then normal order will
terminate. There is a "flip side" to this. As we have already seen,
although an expression may reduce to normal form under a normal order 
reduction, applicative order might not terminate.



Historical Dates
----------------
Alonzo Church (1903-): Lambda Calculus
Kurt Godel (1906-78): theory of recursive function, brought about a complete
                      reassessment of the foundations of mathematics.
Allan Turing (1912-54): Turing machines

1924   Schonfinkel "Uber die Bausteine der mathematischen logik"
1930   Curry "Grundlagen der kombinatorischen Logik"
1931   Godel "Uber formal unenstcheibare Satze der Principia 
       Mathematica und verwandter Systeme"
1936   Church "An unsolvable problem of elementary number theory"
1936   Turing "On Computable Numbers, with an application to
       the Entscheidungsproblem"
1936   Church and Rosser "Some properties of conversion"
1937   Church and Turing independently showed that every computable
       operation can be achieved in lambda calculus and in Turing machines
1930's Kleene discovers subtraction in lambda calculus
1941   Church, "The Calculi of Lambda Conversion"
1965   Landin "A correspondence between Algol 60 and Church's lambda
       notation"
1967   Strachey "Fundamental concepts in programming languages"