Can strong normalization of the typed lambda calculus be proved by a reasonably straightforward mapping from typed terms to a well-founded ordering?

The source page states the original problem together with its recorded qualifications and progress updates as follows.

Can strong normalization (termination) of the typed lambda calculus be proved by a reasonably straightforward mapping from typed terms to a well-founded ordering? Note that the type structure can remain unchanged by $\beta$-reduction. The same question arises with polymorphic (second-order) lambda calculus.