Can F be diverging in "forall M FM = F"?

119 Views Asked by At

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?

1

There are 1 best solutions below

1
On BEST ANSWER

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.