3
$\begingroup$

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.

Improve this question
$\endgroup$
6
  • $\begingroup$ 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. $\endgroup$ – Martin Berger Apr 27 '19 at 7:11
  • $\begingroup$ @MartinBerger If you restrict $\eta$-reduction to variables, how do you reduce $\lambda x.(yz)x$ to the $\beta\eta$-equivalent term $(yz)$? $\endgroup$ – Emil Jeřábek Apr 27 '19 at 8:40
  • $\begingroup$ 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. $\endgroup$ – Martin Berger Apr 27 '19 at 10:26
  • $\begingroup$ @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. $\endgroup$ – Martin Berger Apr 27 '19 at 10:35
  • $\begingroup$ @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. $\endgroup$ – Emil Jeřábek Apr 27 '19 at 11:10
2
$\begingroup$

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

Trying to reproduce it here would be tedious and wouldn't do it justice, so I'll include a picture:

enter image description here

You had the main idea right, it just takes a bit of practice to generalize from the specific examples.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.