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"