# Infinite $\beta \eta$-reduction sequence implies infinite $\beta$-reduction sequence

In Sorensen and Urzyczyn's book there is a lemma (1.3.11) which I am having a hard time proving.

1.3.11 Lemma:

If there is an infinite $$\beta \eta$$-reduction sequence starting with a term $$M$$ then there is an infinite $$\beta$$-reduction seqeunce from $$M$$.

Now the proof is sketched in the book but I am having trouble realising it:

Proof. First observe that in an infinite $$\beta\eta$$-reduction sequence there must be infinitely many $$\beta$$-reduction steps (cf. Exercise 1.6). These $$\beta$$-reduction steps can be "permuted forward", yielding an infinite $$\beta$$-reduction. Indeed, by induction with respect to $$M \to_{\eta} N$$, one can show that $$M \to_{\eta}N \to_{\beta}L$$ implies $$M \to_\beta P \twoheadrightarrow_{\beta \eta} L$$, for some $$P$$.

So $$\to_\eta$$ is defined as the least compatible relation satisfying $$\lambda x . f x \to_\eta f$$. Where compatible means works with the syntax, i.e. $$A \to B$$ imples $$M A \to M B$$, $$A M \to B M$$ and $$\lambda x . A \to \lambda x .B$$.

The definition is similar for $$\beta$$ with the obvious reduction. The relation $$\to_{\beta \eta}$$ is the union of both. And $$\twoheadrightarrow$$ is the transitive-relfexive closure of said relation.

Exercise 1.6 was to prove that $$\to_\eta$$ is strongly normalising, which can be shown by considering a "depth" function on terms, and showing that this strictly decreases on $$\eta$$-reduction.

The problem I am having is I can't seem to understand how $$\beta$$ and $$\eta$$ interact.

Take for example $$\lambda t. (\lambda x . y) t$$. Clearly we can $$\beta$$-reduce this to get $$\lambda t . y$$ or $$\eta$$-reduce it to get $$\lambda x . y$$ which are clearly equal but its not obvious to me in general.

How can this be proven? And better yet, are there any references for this? I can't seem to find much on $$\eta$$-reduction in lambda calculus.

• Your example $\lambda t. (\lambda x . y) t$ does not $\eta$-reduce to $\lambda x . y$, provided $f$, in your rendition $\lambda x . f x \to_\eta f$ of the $\eta$-axiom, ranges over variables rather than terms. – Martin Berger Apr 27 at 7:11
• @MartinBerger If you restrict $\eta$-reduction to variables, how do you reduce $\lambda x.(yz)x$ to the $\beta\eta$-equivalent term $(yz)$? – Emil Jeřábek supports Monica Apr 27 at 8:40
• Regarding the orginal question: the key insight is that $\eta$-reduction never removes any (interesting) $\beta$-redexes, so any $\beta$-redex that exists in term $N$ after an $\eta$-reduction $M \rightarrow_{\eta} N$, existed already in $M$. Hence $M$ has a $\beta$-reduction. Then you appeal to something like Church-Rosser. – Martin Berger Apr 27 at 10:26
• @EmilJeřábek Note that the standard presentation of the $\eta$ axiom (e.g. in Barendregt's The Lambda Calculus, or Hindley/Seldin's Lambda-Calculus and Combinators) is: $\lambda x.Mx =_{\eta} M$ provided $x$ isn't free in $M$. The two forms of $\eta$ are equivalent when considered as axioms for an equational theory. Why? Because clearly: $(\lambda x.Mx) =_{\beta} (\lambda fx.fx)M$ $=_{\eta} (\lambda f.f)M =_{\beta} M$. In this derivation, the second step uses $=_{\eta}$ with variables only. The side-condition that $x$ not be free in $M$ is used in the first step. – Martin Berger Apr 27 at 10:35
• @MartinBerger I know all that. However, the whole point of reductions (as opposed to equations) is that you can apply them only in one direction. The $\beta\eta$-reduction calculus will fail to have the Church–Rosser property and fail to be equivalent to the $\beta\eta$-equational theory if you restrict the $\eta$-rule to variables. – Emil Jeřábek supports Monica Apr 27 at 11:10

As usual, the bible knows all, and Lemma 3.3.8 (p 66) gives the detailed proof of commutativity of $$\beta$$ and $$\eta$$ reductions.