How can I prove a simple eta-conversion?

Question

I would like to prove the following:

$$\lambda x.\ \lambda y.\ f\ z\ x\ y \overset{\eta}{=} \lambda x.\ f\ z\ x$$

Definitions

Free variables

$x \in FV(f) :\Leftrightarrow$ $x$ is a variable used within a function $f$ and $x$ is neither a formal parameter of $f$ nor defined in the body of $f$.

$\alpha$-equivalence

Two terms $T_1, T_2$ are called $\alpha$-equivalent, if $T_1$ can be obtained from $T_2$ by consistant renaming.

$\beta$-equivalence

A $\beta$-reduction is function application on a redex:

$$(\lambda x. t_1)\ t_2 \Rightarrow t_1 [x \mapsto t_2]$$

$\eta$-equivalence

Two terms $\lambda x. f~x$ and $f$ are called $\eta$-equivalent, if $x \notin FV(f)$.

Some thoughts

I can make $\alpha$ conversions to get this:

$$\lambda y.\ \lambda x.\ g\ z\ y\ x \overset{\eta}{=} \lambda y.\ g\ z\ y$$

Then I could define $f := \lambda y.\ g\ z\ y$ so I had

$$\lambda y.\ \lambda x.\ g\ z\ y\ x \overset{\eta}{=} f$$

But now I have a problem. It seems as if I have to switch $\lambda y.\ \lambda x.\ \dots$ to $\lambda x.\ \lambda y.\ \dots$

May I do that? Is there a rule that tells me that this is a valid transformation?

Answer 1

First of all, you can simplify the equation like this:

\begin{align*} \lambda x.\ \lambda y.\ f\ z\ x\ y &\overset{!}{=} \lambda x.\ f\ z\ x\\ \overset{*}{\Leftrightarrow} \lambda y.\ f\ z\ x\ y &\overset{!}{=} f\ z\ x\\ \end{align*}

* is valid, because you may apply the rules to subterms. (Could somebody please go into detail here?)

Then you can make $\alpha$-conversions:

\begin{align*} \lambda y.\ f\ z\ x\ y &\overset{!}{=} f\ z\ x\\ \overset{\alpha}{\Leftrightarrow} \lambda x.\ g\ z\ y\ x &\overset{!}{=} g\ z\ y \end{align*}

Then you can define $f := g\ z\ y$:

\begin{align*} \lambda x.\ g\ z\ y\ x &\overset{!}{=} g\ z\ y\\ \overset{f}{\Leftrightarrow} \lambda x.\ f\ x &\overset{!}{=} f \end{align*}

The last line is true, because that's how $\eta$-conversion is defined. As we've used only equivalences, the other equations are true, too.

Answer 2

Let us consider $G=f\ z\ x$. Whence, $\lambda x.\lambda y. f\ z\ x\ y$ is syntactically the same as $\lambda x.\lambda y. G\ y$.

Now, $FV(G)=\{f,z,x\}$, so $y\notin FV(G)$. Therefore, $\lambda y. G\ y =_\eta G$. Therefore, $\lambda x.\lambda y. G\ y =_\eta \lambda x. G$.

If your trouble has to do with $G\ y$ being a subterm of $\lambda x. G\ y$, recall the definition of the $=_\eta$ relation:

• $(\lambda x. M\ x) =_\eta M$, if $x\notin FV(M)$
• $M=_\eta M$
• $N=_\eta M$, if $M=_\eta N$
• $M=_\eta P$, if $M=_\eta N$ and $N=_\eta P$
• $\lambda x. M =_\eta \lambda x.N$, if $M=_\eta N$
• $MN =_\eta M'N$, if $M=_\eta M'$
• $MN = _\eta MN'$, if $N=_\eta N'$

Answer 3

The main problem seems to be that your definition descriptions are too narrow. For example, every lambda term is $\eta$-equivalent to itself (by the axiom of reflexivity), but your definition of $\eta$-equivalence only takes the $\eta$-axiom into account. The same criticism applies to your definition of $\beta$-equivalence, but this is not relevant here.

There are really only two rules in $\lambda\eta$ you need to use here. First of all, by axiom $\eta$ we have:

$$(\lambda y.fzx y) = fzx \tag{1}$$

since $y \notin FV(fzx)$.

From both (1) and the rule of weak extensionality $\xi$ (a rule in $\lambda\eta$), defined as:

\begin{align} M &\;= M' \\ \hline (\lambda x.M) &\;= (\lambda x.M') \tag{$\xi$} \end{align}

we can then infer $(\lambda x.\lambda y.fzxy) = (\lambda x. fzx)$.