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.