Structural normalization algorithm for the simply typed lambda calculus I would like to know if there is a (piecewise) structural normalization algorithm for the simply typed lambda calculus. By structural I mean a recursive function that only calls itself on subterms of its argument.
Suppose $T$ is an inductive type of terms, then it doesn't seem like there should be any way to define such a function $\text{nf} :T\to T$ directly, so what I want to know is whether one could define an intermediate inductive type $E$ and structural functions $p : T\to E$ and $r:E\to T$ so that $r\circ p:T\to T$ is the normalization function.
The motivation for this is that proving termination is immediate from the well-foundedness of the inductive types.
Are there any other references or implementations that address this question?
You can: define /hereditary substitution/ on already normalized STLC terms using structural induction (where the induction is (in part) on the type).
I couldn't find the reference I was thinking of right now, but a quick search for &quot;agda hereditary subtitutions STLC&quot; pointed to various relevant pages, such as https://github.com/ezyang/lr-agda/blob/master/STLC.agda