1. Fixed-points of Functions¶

In our endeavor to turn the \(\lambda\) calculus into a "real" programming language, we saw in the previous section that we could appropriately define Boolean constants (true, false), conditionals (if-then-else), logical operators (and, or, not), integers (0, 1, 2, 3, etc.), and arithmetic operators (\(+\), \(-\), etc.).

However, one thing is missing. We still need to be able to define recursive functions (factorial, etc.). But to recur, we need a "name" by which we can refer to the function we are creating within the function we are creating. And the \(\lambda\) calculus does not give us global names. Instead we only have a variable that represents the parameter in a function abstraction. So is there a way out of this dilemma? The answer is "yes", and it's called a fixed point combinator. We begin by defining the notion of a fixed point for a function.

For any function \(f\) and \(x\), if \(f(x) = x\) then \(x\) is called a fixed point of the function \(f\).

Here are some examples to consider when the functions are functions of real numbers:

1. Can you find one or more fixed points for the function \(f(t) = t^2\)?
2. Can you find one or more fixed points for the function \(f(t) = 1\)?
3. Can you find one or more fixed points for the function \(f(t) = t+1\)?

2. The Y Fixed-point Combinator¶

When we are dealing with functions of real numbers such as the examples above, the "algorithm" to find a fixed point is to solve the equation \(f(x) = x\). If a solution can be found, the function has a fixed point; otherwise it doesn't.

Is there a similar technique to find the fixed point of any \(\lambda\)-calculus function? Consider a function that we call \(Y\) for historical reasons. It is defined as follows:

\(Y\) will find the fixed point of any function F. That is, for any function F, \((F \; (Y \; F)) = (Y \; F)\). In other words, if we apply Y to F, the result is a value that, when given to F, will give us Y applied to F again.

To see this, note that the substitution needed to \(\beta\)-reduce \((Y \; F)\) leads us to:

Hence Y has the remarkable property that, once applied to any function F, it can keep generating applications of F to (Y F). That is,

If we use this property and define a function F in a way that makes it "almost recursive", Y applied to that almost-recursive function will result in the recursive function we want. In other words, Y turns almost-recursive functions into recursive functions.

3. Using Y to Implement Factorial¶

To illustrate, let's use the Church numerals, IF-THEN-ELSE, MULT, ISZERO, and PRED functions that were defined within the \(\lambda\) calculus in the previous section to define a new almost-recursive function:

This new function resembles what we would normally think of as a recursively defined factorial function except it uses a parameter \(g\) instead of a globally defined name \(g\). Hence it is a valid definition in the \(\lambda\) calculus. Although valid, it is also unfortunately not a recursive factorial function. The amazing thing, however, is that, if we apply \(Y\) to this function, that is:

we get the factorial function. It may take a while to convince yourself of this. Try carrying out the \(\beta\)-reductions that would come into play when evaluating

and you should see how the Church numeral \(SIX\) is eventually produced. To get started on this, you may want to abbreviate the \(\lambda g\) abstraction above as AFACT. Then note that:

β-reduce the leftmost redex in \(((AFACT \; (Y \; AFACT)) \; THREE)\), that is, substitute \((Y \; AFACT)\) for the g parameter in the definition of AFACT, and you will get ...

Note that \((Y \; AFACT)\) is re-introduced inside the ELSE. The combinator property allows us to replace this \((Y \; AFACT)\) with \((AFACT \; (Y \; AFACT)\), whence we can again replace the g parameter of the AFACT abstraction with \((Y \; AFACT)\). Continue from here and you will eventually reach SIX as the value that is returned.

Amazingly, while remaining entirely within the language defined by the Church Booleans and numerals, we have been able to produce a recursive version of the factorial function. This is of great theoretical importance because it demonstrates that Church's \(\lambda\) calculus can harness the full power of recursively defined functions.

4. Identifying Fixed Point Combinators¶

Although the function \(Y\) defined above is a famous fixed-point combinator, there are also many other fixed-point combinators, that is, functions \(Z\) with the property that:

for all functions \(F\). This section will give you practice with identifying other fixed-point combinators.

To reduce syntactic clutter in this problem, we will take some shortcuts in writing \(\lambda\) expressions. First, we will drop all but the first \(\lambda\) and all but the last dot for (curried) functions with two or more parameters. So, for example, we will use:

as an abbreviation for:

Second, to cut down on parentheses, we will use \((u\ v\ w\ x\ y\ z)\) as an abbreviation for \((((((u\ v)\ w)\ x)\ y)\ z)\). In essence, we are making function application left-associative. This notation is to be used only for the following practice problem. Do NOT use it for any assignments, exams, or other practice problems.