Introduction: Recursion is a topic central to computer science. Lambda calculus offers us a very elegant (and fundamental) way to model and study recursion. In a book on computability and automata, such a study also serves another purpose; to concretely demonstrate that Lambda calculus provides a universal mechanism to model computations, similar to the role played by Turing machines. While this chapter can be skimmed, or even skipped, we have taken sufficient pains to make this chapter as “friendly” and intuitive as possible, permitting it to be covered without spending too much time. Covering this chapter will permit fixed-point theory to be used as a conceptual “glue” in covering much important material, including studying context-free grammars, state-space reachability methods, etc.
Recursive Definitions: Let’s get back to the discussion of function ‘Fred’ introduced in Chapter 2, Section 2.6. Now consider a recursively defined function, also called ‘Fred.’ We fear that this will make it impossible to ‘de-Fred:’ function Fred x = if (x=0) then 0 else x Fred(x-1) It is quite tempting to arrive at the following de-Freded form: function(x) = if (x=0) then 0 else x self(x-1)
However, it would really be nice if we can avoid using such ad hoc conventions, and stay within the confines of the Lambda notation as introduced earlier. We shall soon demonstrate how to achieve this; it is, however, instructive to examine one more recursive definition, now involving a function called Bob:
function Bob(x) = Bob(x 1).
One would take very little time to conclude that this recursive definition is “plain nonsense,” from the point of view of recursive programming. For example, a function call Bob(3) would never terminate. However, unless we can pin down exactly why the above definition is “nonsense,” we will have a very ad hoc and non-automatable method for detecting nonsensical recursive definitions - relying on human visual inspection alone. Certainly we do not expect humans to be poring over millions of lines of code manually detecting nonsensical recursion. Here, then, is how we will proceed to “de-Fred” recursive definitions (i.e., create irredundant names for them):
Recursion viewed as solving for a function: Let us write our Fred function as an equation:
Fred=lambda x. if (x=0) then 0 else x Fred(x-1).
The above equation can be rewritten as
Fred=(lambda Fred’ .lambda x. if(x=0) then 0 else x Fred’(x-1)) Fred The fact that this equation is equivalent to the previous one can easily be verified. We can apply the Beta rule, plugging in Fred in place of Fred’, to get back the original form. We can now apply the Alpha rule, and change Fred’ to y, to obtain
the following:
Fred = (lambda y . lambda x . if(x=0) then 0 else x y(x-1)) Fred. Well, we are almost done eliminating the redundant name “Fred.” What we have achieved is that we have expressed Fred using an equation of the form
Fred = H Fred
where H is the Lambda expression (lambda y . lambda x . if(x=0) then 0 else y(x-1)). Note that H contains no trace of Fred.
Fixed-point equations: We now make a crucial observation about the nature of the equation Fred = H Fred. Recall that juxtaposing H and Fred is, in Lambda calculus, equivalent to applying H to Fred. If we wish, we can rewrite the above equation as Fred = H(Fred) to express it in the more familiar syntax of “f(x)”—for f applied to x. Note that there is something peculiar going on; when we feed Fred to H, it spits out Fred. The application of H seems to be “stuck” at Fred. In mathematics, an equation of the form x = f(x) is called a fixedpoint equation. Think of a fixed-point as a fixed point, i.e., an “immovable point.” It appears that things are “stuck” at x; even if we apply f to x, the result is stuck at x. Can we find such “stuck function applications?” Surely!
Here is another way to get a “fixed-point out of a photocopying machine.” More specifically, we can get the fixed-point of the image transformation function of a photocopying machine. Go photocopy your face; then photocopy the photocopy, photocopy the photocopy of the photocopy, etc. In most photocopying machines, the image stabilizes, by turning all gray regions to black or (sometimes) white. Such a stable image is then one fixed-point of the image transformation function of
the photocopying machine.
Coming back to our example, we want a fixed-point, namely a function Fred, that solves the fixed-point equation Fred = H(Fred). Ideally, we would like this fixed-point to be unique, but if that’s not possible, we would like some way to pick out the fixed-point that corresponds to what computers would compute should they handle the recursive program.
The beauty of Lambda calculus is that it does not fundamentally distinguish between functions and “values,” and so the principles of obtaining fixed-points remain the same, independent of whether the fixed-points in question are functions, numbers, or images. For the example at hand, if Fred is a fixed-point of H, we must
We shall resolve these issues in what follows.
