Proving that the Curry fixed point combinator y and the Turing fixed point combinator θ cannot be proved equal in λβ

Question

$y = λf.(λx.f(xx))(λx.f(xx))$

$θ = (λxy.y(xxy))(λxy.y(xxy))$

I'm trying to prove that $y \neq \theta$ in λβ.

My idea was to assume the contrary, then by Church - Rosser, there exists some $u$ s.t. both $y$ and $\theta$ beta reduce to $u$.

Now we know that both fixed point combinators have head normal forms - so I tried splitting it into 2 cases - the case where $u$ is in head normal form and $u$ is not in head normal form.

My idea was then to get both $y$ and $\theta$ into head normal form and compare their heads but this did not seem to work.

I'm not sure how else to solve it

Answer 1

The result, left as an exercise by Barendregt (Exercise 6.8.9), is proved by Klop in a 2007 paper (Proposition 1.2). Here is a slightly adapted version.

Recall the head-internal decomposition of β-reduction: a reduction $M \rightarrow_{\beta}^* N$ can always be decomposed into $M \rightarrow_h^* M' \rightarrow_i^* N$ (see Lemma 11.4.6 of Barendregt).

Write $y = \lambda f.\omega_f\omega_f$ and $\theta = \eta\eta$, then:

• $y \rightarrow_h \lambda f. f(\omega_f\omega_f)$, in hnf;
• $\theta \rightarrow_h \lambda f. f(\eta \eta f)$, in hnf.

Therefore the common reduct of $y$ and $\theta$, if it exists, must be some $u = \lambda f.fu'$ (because of the head-internal decompositions of the reductions $y \rightarrow_{\beta}^* u$ and $\theta \rightarrow_{\beta}^* u$), with $\omega_f\omega_f \rightarrow_{\beta}^* u'$ and $\eta\eta f \rightarrow_{\beta}^* u'$.

Let's do the same thing again:

• $\omega_f\omega_f \rightarrow_h f(\omega_f\omega_f)$, in hnf;
• $\eta\eta f \rightarrow_h (\lambda y.y(\eta\eta y))f \rightarrow_h f(\eta\eta f)$, in hnf.

The common reduct $u'$ must be some $fu''$, with $\omega_f\omega_f \rightarrow_{\beta}^* u''$ and $\eta\eta f \rightarrow_{\beta}^* u''$, which leads us to an infinite loop...

Two remarks:

1. This is a particular case of a more general result, also shown in Klop's paper (section 2), about the Böhm sequence $Y_n$ of fix-point combinators, with $Y_0 = y$ and $Y_1 = \theta$. The result states that there are no distinct $m$ and $n$ such that $Y_m =_{\beta} Y_n$.

2. In some sense, $y$ and $\theta$ are β-equivalent “at the infinity”. This intuition is formalised by the concept of Böhm tree: $\mathrm{BT}(y) = \mathrm{BT}(\theta) = \lambda f.fff\ldots$
   This can be turned into a “real” common reduct in an infinitary λ-calculus (in particular the “001-infinitary” one), where $y \rightarrow_\beta^\infty \lambda f.fff\ldots$, see for instance the original paper, the survey in Barendregt and Manzonetto's Satellite, or some recent presentations here or there.