3
$\begingroup$

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?

$\endgroup$
1
$\begingroup$

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.

$\endgroup$
1
$\begingroup$

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'$
$\endgroup$
0
$\begingroup$

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)$.

$\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.