Understanding η-conversion (Lambda Calculus)

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?

• I really don't know what I'm talking about, but using this link, to the first step take $\lambda y.My$ as $\lambda y\in B.(h(x))(y)$ and perform $\eta$-reduction to on this formula to get $$\lambda x\in A. \lambda y \in B.(h(x))(y) \underset{\eta}{\longrightarrow} \lambda x\in A.h(x)$$ (because $\lambda y\in B.(h(x))(y)\underset{\eta}{\longrightarrow} h(x)$). Similarly $\lambda x\in A.h(x) \underset{\eta}{\longrightarrow}h$. Jun 16 '14 at 13:10
• I repeat, I don't know what I'm talking about, but to me $$\lambda x\in A. \lambda y \in B.(h(x))(y) \underset{\eta}{\longrightarrow} \lambda y\in B.h(y)\underset{\eta}{\longrightarrow} h$$ feels better somehow. Jun 16 '14 at 13:11
• @GitGud Your first comment seems to be the right answer, but I can't understand your second comment. You seem to be $\eta$-converting a function with domain $A$ to a function with domain $B$ and then back to a function with domain $A$. Surely, $\eta$-conversion (or anything that deserves to be called "conversion") preserves types. Jun 16 '14 at 13:15
• @AndreasBlass Thank you for the input. I wasn't sure $h$ is a function, my motivation for the second comment was too look at $(h(x))(y)$ as a predicate - (I have no idea if predicate is a $\lambda$-calculus term or not) - first as a predicate depending on $x$, so I eliminate $x$ first. Then a predicate on $y$ remains and I eliminate $y$. Jun 16 '14 at 13:21
• It took me a few seconds, but then it hit me. Thanks! Jun 16 '14 at 13:23

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.

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.

• The $\alpha$-reduction point is subtle - thank you for clarifying this. Feb 26 '20 at 17:51