<p>As usual, <a href="https://rads.stackoverflow.com/amzn/click/com/0444875085" rel="nofollow noreferrer" rel="nofollow noreferrer">the bible</a> knows all, and Lemma 3.3.8 (p 66) gives the detailed proof of commutativity of <span class="math-container">$\beta$</span> and <span class="math-container">$\eta$</span> reductions.</p>

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

<p><a href="https://i.sstatic.net/gfBPC.jpg" rel="nofollow noreferrer"><img src="https://i.sstatic.net/gfBPC.jpg" alt="enter image description here"></a></p>

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

CC BY-SA 4.0
2019-04-27T19:47:41.643Z
2019-04-27T19:47:41.643Z
cody
<p>In Sorensen and Urzyczyn's book there is a lemma (1.3.11) which I am having a hard time proving.</p>
<blockquote>
<p><strong>1.3.11 Lemma</strong>:</p>
<p>If there is an infinite <span class="math-container">$\beta \eta$</span>-reduction sequence starting with a term <span class="math-container">$M$</span> then there is an infinite <span class="math-container">$\beta$</span>-reduction seqeunce from <span class="math-container">$M$</span>.</p>
</blockquote>
<p>Now the proof is sketched in the book but I am having trouble realising it:</p>
<blockquote>
<p>Proof.
First observe that in an infinite <span class="math-container">$\beta\eta$</span>-reduction sequence there must be infinitely many <span class="math-container">$\beta$</span>-reduction steps (cf. Exercise 1.6). These <span class="math-container">$\beta$</span>-reduction steps can be &quot;permuted forward&quot;, yielding an infinite <span class="math-container">$\beta$</span>-reduction. Indeed, by induction with respect to <span class="math-container">$M \to_{\eta} N$</span>, one can show that <span class="math-container">$M \to_{\eta}N \to_{\beta}L$</span> implies <span class="math-container">$M \to_\beta P \twoheadrightarrow_{\beta \eta} L$</span>, for some <span class="math-container">$P$</span>.</p>
</blockquote>
<p>So <span class="math-container">$\to_\eta$</span> is defined as the least compatible relation satisfying <span class="math-container">$\lambda x . f x \to_\eta f$</span>. Where compatible means works with the syntax, i.e. <span class="math-container">$A \to B$</span> imples <span class="math-container">$M A \to M B$</span>, <span class="math-container">$A M \to B M$</span> and <span class="math-container">$\lambda x . A \to \lambda x .B$</span>.</p>
<p>The definition is similar for <span class="math-container">$\beta$</span> with the obvious reduction. The relation <span class="math-container">$\to_{\beta \eta}$</span> is the union of both. And <span class="math-container">$\twoheadrightarrow$</span> is the transitive-relfexive closure of said relation.</p>
<p>Exercise 1.6 was to prove that <span class="math-container">$\to_\eta$</span> is strongly normalising, which can be shown by considering a &quot;depth&quot; function on terms, and showing that this strictly decreases on <span class="math-container">$\eta$</span>-reduction.</p>
<p>The problem I am having is I can't seem to understand how <span class="math-container">$\beta$</span> and <span class="math-container">$\eta$</span> interact.</p>
<p>Take for example <span class="math-container">$\lambda t. (\lambda  x . y) t$</span>. Clearly we can <span class="math-container">$\beta$</span>-reduce this to get <span class="math-container">$\lambda t . y$</span> or <span class="math-container">$\eta$</span>-reduce it to get <span class="math-container">$\lambda x . y$</span> which are clearly equal but its not obvious to me in general.</p>
<blockquote>
<p>How can this be proven? And better yet, are there any references for this? I can't seem to find much on <span class="math-container">$\eta$</span>-reduction in lambda calculus.</p>
</blockquote>

CC BY-SA 4.0
2019-04-27T07:11:05.823Z
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
CC BY-SA 4.0
2019-04-27T08:40:04.493Z
@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
CC BY-SA 4.0
2019-04-27T10:26:43.007Z
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
CC BY-SA 4.0
2019-04-27T10:35:56.920Z
@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
CC BY-SA 4.0
2019-04-27T11:10:12.307Z
@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
CC BY-SA 4.0
2019-04-27T11:25:36.237Z
@EmilJeřábek I don't know what the original poster meant, that's why I qualified my initial comment with "provided  [...] ranges over variables rather than terms". If  ranges over terms, the original question forgets to mention the side condition on variables. I wanted to alert the original poster, that  the question is a bit unclear.
Martin Berger
<lambda-calculus><normalization>
Infinite $\beta \eta$-reduction sequence implies infinite $\beta$-reduction sequence
DontMockMeBird
# Infinite $\beta \eta$-reduction sequence implies infinite $\beta$-reduction sequence

(Asked by: username_0 on 2019-04-26)

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.

**Tags:** lambda-calculus, normalization

> **Comments:**
> **username_1**: 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.  
> **username_2**: @MartinBerger If you restrict $\eta$-reduction to variables, how do you reduce $\lambda x.(yz)x$ to the $\beta\eta$-equivalent term $(yz)$?  
> **username_1**: 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.  
> **username_1**: @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.  
> **username_2**: @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.  
> **username_1**: @EmilJeřábek I don't know what the original poster meant, that's why I qualified my initial comment with "provided  [...] ranges over variables rather than terms". If  ranges over terms, the original question forgets to mention the side condition on variables. I wanted to alert the original poster, that  the question is a bit unclear.  

---

## 1 answers

### Answer by username_3 on 2019-04-27. Score: 2

As usual, [the bible](https://rads.stackoverflow.com/amzn/click/com/0444875085) 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](https://i.sstatic.net/gfBPC.jpg)](https://i.sstatic.net/gfBPC.jpg)

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


---

