When are you supposed to eta-reduce? 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?
$\eta$ conversion is not a mean to reduce a term to $\beta$-normal form, but a tool to show equivalence regarding the (future) application; to express that 2 terms “are the same function”; that they will reduce to the same term when applied to arbitrary term(s).

If you want to also do $\eta$ conversions, you can do it anytime because you still have the same term (application-wise) after performing it. Having $\eta$ conversion in the theory will not enrich nor deplete the theory regarding existence of $\beta$($\eta$)-normal forms.