6
$\begingroup$

In Hindley (Lambda-Calculus and Combinators, an Introduction), Corollary 3.3.1 to the fixed-point theorem states:

In $\lambda$ and CL: for every $Z$ and $n \ge 0$ the equation $$xy_1..y_n = Z$$ can be solved for $x$. That is, there is a term $X$ such that $$Xy_1..y_n =_{\beta,w} [X/x]Z$$

I dont understand how to even think about it. I was thinking that $y_1...y_n$ could be thought of as a function on which $X$ acts so $X$ is the fixed point I would like to find. Is that right?

And I dont even understand the proof a little bit, which is - Choose $X = \mathbf{Y}(\lambda x y_1...y_n.Z)$ What does it mean? How is it a solution? Can someone explain?

Note that $\mathbf{Y}$ here means any fixed-point combinator, i.e. $\mathbf{Y}X =_{\beta, w}X$ for any expression $X$.

$\endgroup$
  • 1
    $\begingroup$ You might want to try posting (moving?) this to computer science stackexchange at cs.stackexchange.com if you don't have any luck here. $\endgroup$ – joeA Jan 26 '15 at 20:09
  • $\begingroup$ Did you ever get any intuition about this? I just got to this part of the text and was considering asking about it here. $\endgroup$ – Kyle Strand Jan 3 '16 at 21:00
  • $\begingroup$ I don't really understand your comment about the relationship between $y_1\dots y_n$ being a function and $X$ being the "fixed point [we] would like to find", but it is certainly true that $X$ is a fixed point, since it is of the form $\mathbf{Y}x$. But note that the particular expression for which it is a fixed point, i.e. the expression $x$ in $\mathbf{Y}x = x(\mathbf{Y}x)$, is $\lambda xy_1 \dots y_n.Z)$. I'm still not sure how that solves the problem, though. $\endgroup$ – Kyle Strand Jan 3 '16 at 21:18
6
+100
$\begingroup$

Just apply equational reasoning starting from the provided solution $$ X = \mathbf{Y}(\lambda x y_1 \ldots y_n.Z ) $$ Recall that $\mathbf{Y}F = F(\mathbf{Y}F)$ for any $\lambda$-term $F$, since $\mathbf{Y}$ is a fixed point combinator. In particular $$ \mathbf{Y}(\lambda x y_1 \ldots y_n.Z ) = (\lambda x y_1 \ldots y_n.Z ) (\mathbf{Y}(\lambda x y_1 \ldots y_n.Z )) $$ Then we just compute:

$$ \begin{array}{ll} & X y_1 \ldots y_n \\ = & \mbox{\{definition of $X$\}} \\ & \mathbf{Y}(\lambda x y_1 \ldots y_n.Z ) y_1 \ldots y_n \\ = & \mbox{\{fixed point property\}} \\ & (\lambda x y_1 \ldots y_n.Z ) (\mathbf{Y}(\lambda x y_1 \ldots y_n.Z )) y_1 \ldots y_n \\ = & \mbox{\{definition of $X$\}} \\ & (\lambda x y_1 \ldots y_n.Z ) X y_1 \ldots y_n \\ = & \mbox{\{$\beta$ reduction, applied $n+1$ times\}} \\ & [y_n / y_n] \ldots [ y_1 / y_1 ] [X/x] Z \\ = & \mbox{\{substituting a variable for itself has no effect\}} \\ & [X/x] Z \\ \end{array} $$ Q.E.D.

Let me add some intuition about how one can find the proposed solution. Recall the equation $$ x y_1 \ldots y_n = Z $$ and consider the easy case where $x \notin {\sf free}(Z)$. In this case there's a trivial solution: $x$ can just take $n$ arguments $y_1 \ldots y_n$ and output $Z$: $$ x = \lambda y_1 \ldots y_n. Z $$ Hence, the above solves the easy case. What about the general one? There, the above equation does not provide a solution, since $x$ is present in the right hand side. However, we can apply a "reverse $\beta$ reduction step" to isolate such $x$: $$ x = (\lambda x y_1 \ldots y_n. Z) x $$ We can rewrite the above as $$ x = F x \qquad\mbox{where } F = (\lambda x y_1 \ldots y_n. Z) $$ Now, $F$ is a well-defined $\lambda$-term not involving $x$ as a free variable. All that is left is to solve the equation $x = F x$, but this is a fixed point equation so we can simply take $x = \mathbf{Y} F$ for this. Hence, we obtain the proposed solution.

$\endgroup$
  • $\begingroup$ Thanks for showing how the definition of $X$ satisfies the second equation, which is certainly part of OP's question. The part I am more confused about, though (and perhaps I should have simply opened a new question), is what that definition of "solve for $x$" even means. Typically "solve for $x$" means something like "isolate $x$ on one side of the equation," but in lambda calculus $x$ is just an atom (so what good is "solving for" it?), and the second equation doesn't seem to isolate $x$ at all; it just binds it on the left-hand side. $\endgroup$ – Kyle Strand Jan 4 '16 at 17:58
  • $\begingroup$ @KyleStrand It means to find some term $X$ (not involving $x$) such that replacing $x$ with $X$ satifies the equation according to the $\lambda$-calculus axioms. The second equation $x = \lambda y_1 \ldots$ simply defines a solution. $\endgroup$ – chi Jan 4 '16 at 18:05
  • 1
    $\begingroup$ Okay, the other part of my confusion (which was mostly clarified by reading further in the book) is that the first equation, $xy_1y_2\dots y_n = Z$, is any arbitrary equation (i.e. not a formula already known to be satisfied by $=_{\beta, w}$) where one side starts with $x$. This makes the "solve for $x$" definition make a lot more sense. $\endgroup$ – Kyle Strand Jan 6 '16 at 16:32

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.