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:
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$.
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.
