3.9.1. The Y Fixed-point Combinator¶

To turn the $\lambda$ calculus into a "real" programming language, we need to be able to manipulate, 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.

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

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$?

When we are dealing with functions of real numbers, the "algorithm" to find a fixed point to solve the equation $f(x) = x$. If a solution can be found, the function has a fixed point; otherwise it doesn't. fixed point of any numerical function?

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)$. To see this, note that the substitution dictated by $\beta$ reduction leads us to:

Now using the IF-THEN-ELSE, MULT, ISZERO, and PRED functions that were defined within the $\lambda$ calculus in the previous section, we can define a new 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 awhile to convince yourself of this. Try carrying out the $\beta$ reductions that would come into play when

is evaluated, and you should see how the Church numeral $SIX$ is eventually produced.

3.9.2. 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 problem 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 this review problem. Do NOT use it for any assignments, exams, or other review problems.