[Math] What’s the point of eta-conversion in lambda calculus

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.

Best Answer

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.

Related Question