4
$\begingroup$

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?

Improve this question
$\endgroup$
3
  • $\begingroup$ Do you consider $M[N/x]$ to be a subterm of $(\lambda x.M)N$? $\endgroup$
    – Martin Berger
    Jan 29, 2021 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, 2021 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, 2021 at 21:04

1 Answer 1

Reset to default
1
$\begingroup$

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

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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