Understanding η-conversion (Lambda Calculus)

Question

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?

Answer 1

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.

Answer 2

For Eta reduction, see Hendrik Pieter Barendregt, The Lambda Calculus Its Syntax and Semantics (rev ed - 1984), page 63 :

3.3.1. Definition : (i) $\eta:\lambda x.Mx \rightarrow M$ provided $x \notin FV(M)$.

The point of $\beta \eta$-reduction is that it axiomatizes provable equality in the extensional $\lambda$-calculus.

This amount to saying that, whenever the function $M$ is to be used, any argument will simply be passed to $M$. Hence, this function is, in essence, equal to $M$. One caveat of $\eta$-abstraction is that a name conflict must be avoided. What this means is if $x$ is a free variable (i.e., not scoped in a function abstraction) in $M$ itself, then this $\eta$-reduction is not valid, as it would be changing the scope of $x$. In order to avoid this, an $\alpha$-reduction must be performed before the $\eta$-reduction.