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?

  • $\begingroup$ Do you consider $M[N/x]$ to be a subterm of $(\lambda x.M)N$? $\endgroup$ – Martin Berger Jan 29 at 20:37
  • $\begingroup$ @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. $\endgroup$ – Couchy Jan 29 at 20:45
  • 2
    $\begingroup$ This is a core feature of "normalization by evaluation" (nbe). There are lots of references for nbe. $\endgroup$ – András Kovács Jan 29 at 21:04

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 "agda hereditary subtitutions STLC" pointed to various relevant pages, such as https://github.com/ezyang/lr-agda/blob/master/STLC.agda


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.