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?

  • $\begingroup$ 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$. $\endgroup$
    – Git Gud
    Jun 16 '14 at 13:10
  • $\begingroup$ 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. $\endgroup$
    – Git Gud
    Jun 16 '14 at 13:11
  • $\begingroup$ @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. $\endgroup$ Jun 16 '14 at 13:15
  • $\begingroup$ @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$. $\endgroup$
    – Git Gud
    Jun 16 '14 at 13:21
  • $\begingroup$ It took me a few seconds, but then it hit me. Thanks! $\endgroup$
    – AnnieOK
    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.

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

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.