Eta conversion

Summary

Eta conversion identifies a term $M$ with the abstraction $\lambda x.\, M\, x$, when $x$ does not occur free in $M$. It expresses extensionality in the lambda calculus: two functions that give the same result on every argument are equal. Added to beta reduction, it gives the $\beta\eta$-calculus, whose convertibility is the extensional equality of terms.