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?

  • 3
    $\begingroup$ Check the fix point property: $YV = V(YV) \neq V Y V$ $\endgroup$
    – Euge
    Jan 17, 2017 at 16:07
  • $\begingroup$ 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))$. $\endgroup$ Jan 18, 2017 at 14:37

1 Answer 1



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*}

  • $\begingroup$ Excellent. Indeed -- all of my confusion has come from conflating $XYZ \equiv ((XY)Z)$ with $X(YZ)$. $\endgroup$
    – George
    Jan 18, 2017 at 16:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.