Let $h \in A\rightarrow (B\rightarrow C)$
I'm trying to understand the following reduction:
$$\lambda x\in A. \lambda y \in B.(h(x))(y) \\= \lambda x\in A.h(x) \\= h$$
Apparently, this is done by using "Eta-Reduction". Can you help me understand the use of this rule here?
Best Answer
Consider some function $F$. This function takes an argument $x$ and yields $F x$.
Now consider the following function $G$: $$\lambda y. F y$$ This function also takes an argument $x$ and yields $F x$.
$G$ and $F$ might be completely different lambda-terms, but it is the case that $Fx=Gx$ for every $x$, so the functions represented by $F$ and $G$ are equal.
For example, consider $$\begin{align} F & = \lambda x.x \\ G & = \lambda x.(\lambda y.y)x \\ \end{align}$$
$F$ is the identity function. $G$ is the function that takes an argument $x$ and applies the identity function to it. $F$ is not the same term as $G$: One is four symbols long, the other ten symbols. But the behavior of $F$ and $G$ is the same, in the sense that for every term $x$, $F x $ has a normal form if and only if $ G x$ does, and if so these normal forms are the same.
When this happens, we say that $F$ and $G$ are $\eta$-equivalent, or that $F$ is the $\eta$-reduction of $G$, or that $G$ is the $\eta$-expansion of $F$, or that $F$ and $G$ are $\eta$-conversions of one another.