Wikipedia lists the following algorithm for normalizing a lambda calculus term $t$:
- If $t$ is not in head normal form, beta reduce the beta redex in the head position to get $t'$. Then normalize $t'$ to get $t''$. $t''$ is the normal form of $t$.
- If $t$ is in head normal form, normalize each of its subterms to get $t'$. $t'$ is the normal form of $t$.
The implied base case is if $t$ is in head normal form but has no subterms, in which case it is in normal form already. If $t$ has a normal form, the above algorithm is guaranteed to find it.
The problem I'm having is that it does not seem that the algorithm ever eta-reduces.
For example given the algorithm normalizes $\lambda y.\lambda x.y x$ to itself (since it is already in head normal form, and $x$ is also in head normal form). It should normalize to $\lambda y. y$ though.
It seems apparent that you need to add eta-reduction steps at some point. The problem is I'm not sure where to put them and preserve the property that the algorithm is guaranteed to find the normal form.
When and where do you eta-reduce to achieve this?