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

lambda-calculus

$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

Best Answer

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.

Related Question