# 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?

• Do you consider $M[N/x]$ to be a subterm of $(\lambda x.M)N$? – Martin Berger Jan 29 at 20:37
• @MartinBerger If you choose a tree representation for terms, then a subterm is a subtree, so I would not consider this a subterm unless you have some very clever encoding of terms. – Couchy Jan 29 at 20:45
• This is a core feature of "normalization by evaluation" (nbe). There are lots of references for nbe. – András Kovács Jan 29 at 21:04