Alpha and eta conversions

In the previous chapter we ran into an important problem that arises during substitution. Here we look more closely at how to solve it.

α-conversion

The name of a bound variable is no more than a label: $\lambda x.\,x$ and $\lambda y.\,y$ are one and the same function.

The especially gifted folks skip the renaming hassle altogether and use de Bruijn indices: the lambdas themselves stay but become nameless, while every occurrence of a variable is written as a number — how many lambdas you must go up from it to reach its binder (counting from zero, $0$ being the nearest enclosing lambda). Then α-equivalent terms get one and the same representation, and α-conversion disappears as a concept.

• $\lambda x.\,x$ → $\lambda.\,0$ (the only variable points to its own lambda);
• $\lambda x.\,\lambda y.\,x\,y$ → $\lambda.\,\lambda.\,1\,0$ ($x$ became $1$, and $y$ became $0$).

η-conversion

This is really a small thing, but still worth a brief mention. η-conversion says that the “wrapper” $\lambda x.\,M\,x$ is no different from $M$ itself.

η-reduction collapses such a wrapper to the left, while η-expansion unfolds it to the right.

In Haskell this is the familiar point-free style:

sum xs = foldr (+) 0 xs
-- becomes
sum = foldr (+) 0