7
$\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$
3
  • 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, 2015 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$ Jan 3, 2016 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$ Jan 3, 2016 at 21:18

1 Answer 1

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$
3
  • $\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$ Jan 4, 2016 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, 2016 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$ Jan 6, 2016 at 16:32

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .