Trouble Replicating Proof of The Lambda Calculus Fixed Point Theorem

Question

From pg. 35 of Lambda Calculus and Combinators An Introduction:

Corollary 3.3.1 in $\lambda$ and $CL$: for every $Z$ and $n \ge 0,ドル the equation

$$ xy_1 \ldots y_n = Z $$

can be solved for $x$. That is, there is a term $X$ such that

$$ Xy_1 \ldots y_n =_{\beta, w} [X/x]Z. $$

Proof: Choose $X \equiv \mathsf{Y} (\lambda x y_1 \ldots y_n.Z)$.

Note: In the book, we assume that $\mathsf{Y} \equiv (\lambda ux. xuux)(\lambda ux. xuux)$. Further, for ease of notation, let $V \equiv (\lambda x y_1 \ldots y_n.Z)$.

The problem is that when I check this with my own examples, I'm not getting this result.

For example, suppose that neither $x$ nor any of $y_1, \ldots , y_n$ is in the free variables of $Z$ (to make it easy). Then this theorem asserts that if $X \equiv \mathsf{Y}(\lambda x y_1 \ldots y_n . Z),ドル then

$$ Xy_1 \ldots y_n =_{\beta, w} Z $$

When I check whether this true, I get

$$ (\mathsf{Y}(\lambda x y_1 \ldots y_n . Z))y_1 \ldots y_n = (\mathsf{Y}V)y_1 \ldots y_n = (V\mathsf{Y}V)y_1 \ldots y_n =_{\beta, w} Zy_n $$

Am I doing something wrong?

• Euge: Check the fix point property: $YV = V(YV) \neq V Y V$
• Andrej Bauer: There seems to be some confusion here on the difference between $A (B C)$ and $(A B) C$. Your combinator $Y$ is broken is it not? It should be $(\lambda u x. x (u u x)) ((\lambda u x. x (u u x))$.

Answer 1

$\newcommand{\Y}{\mathsf{Y}}$

Did you leave out any parentheses by any chance? We should take $\Y = (\lambda u x . x (u u x)) (\lambda u x . x (u u x))$. Note that $x u u x$ is the same as $(x u u) x,ドル which is not the same as $x (u u x)$.

We use the abbreviations $V = (\lambda x y_1 \ldots y_n . Z)$ and $X = \Y V,ドル as in your question. Then we calculate: \begin{align*} \Y V &= (\lambda u x . x (u u x)) (\lambda u x . x (u u x)) V \\ &= (\lambda x . x ((\lambda u x . x (u u x)) (\lambda u x . x (u u x)) x)) V \\ &= V ((\lambda u x . x (u u x)) (\lambda u x . x (u u x)) V) \\ &= V (\Y V) \end{align*} and hence \begin{align*} X y_1 \ldots y_n &= \Y V y_1 \ldots y_n \\ &= V (\Y V) y_1 \ldots y_n \\ &= (\lambda x y_1 \ldots y_n . Z) (\Y V) y_1 \ldots y_n \\ &= (\lambda x y_1 \ldots y_n . Z) X y_1 \ldots y_n \\ &= [X/x, y_1/y_1, \ldots, y_n/y_n] Z \\ &= [X/x] Z. \end{align*}

• George: Excellent. Indeed -- all of my confusion has come from conflating $XYZ \equiv ((XY)Z)$ with $X(YZ)$.