1
$\begingroup$

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?

$\endgroup$
  • 3
    $\begingroup$ Check the fix point property: $YV = V(YV) \neq V Y V$ $\endgroup$ – Euge Jan 17 '17 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$ – Andrej Bauer Jan 18 '17 at 14:37
1
$\begingroup$

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

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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