1
$\begingroup$

Using the $Y$ combinator I got $F (Y F) = Y F = F \Rightarrow F = YY$. The problem is $YY$ diverges.

Is it correct to state that $\forall M\;YYM = YY$, because both statements diverge?

$\endgroup$
  • $\begingroup$ The fixed point combinator is a term such that $YF = F(YF)$ for every term $F$. Why do you say that $YF = F$? Anyway, the fact that two terms diverge does not mean they are $\beta$-equivalent. $\endgroup$ – Taroccoesbrocco Feb 10 '18 at 21:25
  • $\begingroup$ I say that because $F(YF) = F$. But ok, the "solution" is invalid $\endgroup$ – Alex Feb 10 '18 at 21:29
  • $\begingroup$ Well, then I am missing something. If $\forall M\: FM = F$ and $YF = F(YF)$, why does not it mean that $F$ is the fixed point of $Y$? At least it should not be, as this does not make sense $\endgroup$ – Alex Feb 10 '18 at 21:37
  • $\begingroup$ I don't understand how you can derive $F = YY$ from $YF = F$. $\endgroup$ – Taroccoesbrocco Feb 11 '18 at 7:56
  • $\begingroup$ Oh. For some reason I thought that any term has a unique fixed point, so $F$ would be equivalent to $Y$'s fixed point which is $YY$. This is obviously wrong, because any term is a fixed point of $I$, for instance $\endgroup$ – Alex Feb 11 '18 at 9:28
1
$\begingroup$

I think that behind your questions there is some confusion about the terminology. I try to clarify it.

In mathematics, an element $x$ of the domain of a function $f$ is a fixed point of $f$ if $f(x) = x$. For instance, $0$ is a fixed point of the function $f(x) = x^2$; the function $f(x) = x +1$ has no fixed points.

In the context of $\lambda$-calculus (where every term is a function), a fixed point of a term $F$ is a term $M$ such that $FM = M$ (where $=$ stands for the $\beta$-equivalence). Do you see the analogy with mathematics?

A key feature of the $\lambda$-calculus is that every term $F$ has a fixed point; such a fixed point of $F$ is $YF$, where $Y$ is the fixed point combinator $\lambda f. \! (\lambda x. \! f(x\,x))\ (\lambda x.\! f(x\,x))$. Indeed, it is easy to prove that $F(YF) = YF$ for every term $F$.


  1. To answer the question in your last comment, if $F$ is a term such that $FM = F$ for every term $M$ (the hypothesis $F(YF) = YF$ is superfluous because it always holds), then $F$ is a fixed point of $Y$. Indeed, \begin{align} YF = F(YF) = F \end{align} where the first $\beta$-equivalence holds by definition of $Y$, the second $\beta$-equivalence holds by hypothesis (take $M = YF$).

  2. But is there a term $F$ such that $FM = F$ for every term $M$? To give a positive answer to such a question it is sufficient to find a term $F$ that satisfies the $\beta$-equivalence \begin{align}\tag{1} F = \lambda x.\! F \end{align} where $x$ is not a free variable of $F$: indeed, this implies that $FM = (\lambda x.\! F)M = F$ for every term $M$. A term $F$ that satisfies $(1)$ must be a fixed point of $K := \lambda y.\! \lambda x.\! y$, because $KF = \lambda x.\! F = F$ (the first $\beta$-equivalence holds by definition of $K$). Therefore, since $YK$ is a fixed point of $K$, you can define \begin{align} F := YK. \end{align} Let us check that, with this definition of $F$, really $FM = F$ for every term $M$: $FM = (YK)M = K(YK)M = (\lambda x .\! YK)M = YK = F$. Note that $F$ diverges (this answers your question in the title of the OP), because (remember that $Y := \lambda f. \! (\lambda x. \! f(x\,x))\ (\lambda x.\! f(x\,x))$, see above) \begin{align} F := YK &\to_\beta (\lambda x. \! K(x\,x))\ (\lambda x.\! K(x\,x)) \to_\beta K \big( (\lambda x. \! K(x\,x))\ (\lambda x.\! K(x\,x)) \big) \\ &\to_\beta K \big(K\big( (\lambda x. \! K(x\,x))\ (\lambda x.\! K(x\,x)) \big)\big) \to_\beta \dots \end{align}

  3. To answer your question in the OP, the fact that two terms diverge does not mean they are $\beta$-equivalent. For instance, consider the terms $\delta = \lambda x.xx$ and $\Delta = \lambda x.xxx$; then, the terms $\delta\delta$ and $\Delta\Delta$ diverge but are not $\beta$-equivalent, because all the reductions from $\delta\delta$ and $\Delta\Delta$ have the form: \begin{align} \delta\delta &\to_\beta \delta\delta \to_\beta \dots & \Delta\Delta \to_\beta \Delta\Delta\Delta \to_\beta \Delta\Delta\Delta\Delta \to_\beta \dots \end{align} and so $\delta\delta$ and $\Delta\Delta$ do not have a common reduct.

  4. In general, proving that two terms are not $\beta$-equivalent is a hard task: you have to prove that all the reduction sequences starting from these two terms do not have a common reduct.

$\endgroup$
  • $\begingroup$ Just to let you know, I skimmed the PDF you mentioned in the Logic room. It was as interesting as it was vague. An incredible number of issues raised in it shows up in some way in my type theory! But anyone who does not know anything about type theory will learn nothing from the PDF... It seems though that my type theory escapes the issues in the PDF in interesting ways, which I'd be glad to discuss with you in the Logic room when you're free. For example, I have a universal type and hence a true fixed-point combinator, unlike ZFC or System F. =) $\endgroup$ – user21820 Feb 17 '18 at 16:54

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.