# What's the point of eta-conversion in lambda calculus?

I think I'm not understanding it, but eta-conversion looks to me as a beta-conversion that does nothing, a special case of beta-conversion where the result is just the term in the lambda abstraction because there is nothing to do, kind of a pointless beta-conversion.

So maybe eta-conversion is something really deep and different from this, but, if it is, I don't get it, and I hope you can help me with it.

Thank you.

(And sorry, I know this is part of the very basics in lambda calculus)

• – MJD
Jun 27 '15 at 17:44
• It is funny because $\eta$-conversion seems to me like currying which let's you omit whole but one parameter. This way, your program is like chain of combinators and this representation is called point-free, aka. pointless :) Apr 2 '18 at 17:46
• Tangentially related: What is Eta abstraction in lambda calculus used for? Feb 15 at 20:32

Beta conversion is the familiar $(\lambda x.M)N \rightsquigarrow M[x:=N]$.

Eta conversion is $\lambda x.M x \rightsquigarrow M$ when $M$ does not contain $x$ free.

Eta is not a special case of beta, because there is no beta redex anywhere yet. You could say that it anticipates the beta redex that will arise if and when the left-hand side is applied to something. At that point the reduction $$(\lambda x.M x) N \rightsquigarrow M N$$ can be justified either as a beta or an eta reduction, but the eta reduction could happen before there's even an $N$ there. The eta conversion is intuitively justified by the fact that in the end the only thing you can really do with a lambda term is to apply it to something, so at that point it's not going to matter whether you've already eta reduced or not. So in that sense, eta equivalence does not add anything fundamentally new to the calculus. The availability of eta-reduction does not change whether a term has a normal form, for example.

Eta is, however, sometimes useful as an auxiliary reasoning concept. For example, the combinators $(\lambda y.\lambda x.y x)$ and $(\lambda y.y)$ are observationally equivalent -- but how can we show that? Simply noting that they are $\eta$-equivalent packs a somewhat subtle and long-winded argument into an easily reusable concept.

• What do you mean by "observationally equivalent". Could you clarify this? Oct 14 '13 at 7:51
• I think the difference between $\beta$ and $\eta$ becomes more obvious if you consider some model of $\lambda$. Then $\beta$ is simply the statement that we can evaluate a pointwise-defined function at any point in a natural manner, while $\eta$ is a much less trivial statement that a function is uniquely determined by its value at each point. Clearly not any function contains only pointwise information. E.g. in algebraic geometry the ring of functions can have nilpotent elements (although AG isn't formally a model of $\lambda$), and there are similarly nilpotent models of real analysis/ Dec 15 '13 at 17:37
• @Trismegistos $A$ and $B$ are “observationally equivalent” if they “do” the same thing: that is, if $A x\equiv B x$ for every $x$. This is obviously no stronger than regular equivalence, and Henning Makholm's example shows that it is strictly weaker.
– MJD
Jun 27 '15 at 17:46
• I think the point is yx means apply y to x, so y is eta equivalent to (λx.yx) and y here is the M in the definition of Eta conversion. And further, (λy.y) is apply ident to y and so ident is the M here. So (λy.λx.yx) eta equivalent to (λy.y) and then eta equivalent to ident.
– cmal
Jul 3 '18 at 5:20

Yet another way to answer this question is to provide the following quotation from “Lambda Calculus. Its Syntax and Semantics“ (Barendregt, 1981). However, since I have access only to its Russian translation at the moment, I have to translate it back to English. The following is from Section 3.3.

The point of introducing of $\beta\eta$-reduction is to provide an axiom for provable statements in extensional $\lambda$-calculus [the $\lambda + \text{ext}$ theory, where $\text{ext}$ stands for the rule $M x = N x \Rightarrow M = N$] such that it would have Church–Rosser property.

Proposition. $M =_{\beta\eta} N \Leftrightarrow \lambda\eta \vdash M = N \Leftrightarrow \lambda + \text{ext} \vdash M = N$.

[Its proof is based on the following theorem.]

Theorem (by Curry). The theories $\lambda + \text{ext}$ and $\lambda\eta$ are equivalent… [Its proof consists of two parts: $(\text{ext}) \Rightarrow (\eta)$ and vice versa.]

One of the reasons to consider the system $\lambda\eta$ is that it has a certain property of completeness… [Namely, in the sense of the following theorem.]

Theorem. Let $M$ and $N$ both have a normal form. Then, either $\lambda\eta \vdash M = N$, or $\lambda\eta + M = N$ is inconsistent…

HP-complete [after Hilbert–Post] theories correspond to maximum consistent theories in theory of models for the first-order logic.

The $$\eta$$-equivalence does not just imply $$(\lambda x . e_0) x \to e_0$$ under the side-condition (which I believe could be argued using $$\beta$$ instead, noting that $$e_0[x/x] = e_0$$); it also implies the opposite direction. IE, it is an equivalence $$(\equiv_{\eta})$$, not just a reduction $$(\to_{\eta})$$. I am not sure why anyone worries much about $$\eta$$-reduction in the left-to-right sense, but viewed as an equivalence, it gives rise to "expansion" in the right-to-left sense, which is useful in writing more succinct proofs at least. Here is some justification of my argument [Ramsey19]:

That said, the immediate, practical reason to know about Eta is that the rule can used backwards. This transformation, from M to λx.Mx, is known as “eta-expansion.”

This direction allowes us to capture the notion that two functions $$f$$ and $$g$$ are equal/equivalent iff they evaluate the same way on all possible arguments.