<p>You can: define /hereditary substitution/ on already normalized STLC terms using structural induction (where the induction is (in part) on the type).</p>
<p>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 <a href="https://github.com/ezyang/lr-agda/blob/master/STLC.agda" rel="nofollow noreferrer">https://github.com/ezyang/lr-agda/blob/master/STLC.agda</a></p>

CC BY-SA 4.0
2021-01-30T14:36:51.813Z
2021-01-30T14:36:51.813Z
Stefan
<p>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.</p>
<p>Suppose <span class="math-container">$T$</span> is an inductive type of terms, then it doesn't seem like there should be any way to define such a function <span class="math-container">$\text{nf} :T\to T$</span> directly, so what I want to know is whether one could define an intermediate inductive type <span class="math-container">$E$</span> and structural functions <span class="math-container">$p : T\to E$</span> and <span class="math-container">$r:E\to T$</span> so that <span class="math-container">$r\circ p:T\to T$</span> is the normalization function.</p>
<p>The motivation for this is that proving termination is immediate from the well-foundedness of the inductive types.</p>
<p>Are there any other references or implementations that address this question?</p>

CC BY-SA 4.0
2021-01-29T20:37:16.780Z
Do you consider $M[N/x]$ to be a subterm of $(\lambda x.M)N$?
Martin Berger
CC BY-SA 4.0
2021-01-29T20:45:40.367Z
@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
CC BY-SA 4.0
2021-01-29T21:04:06.427Z
This is a core feature of "normalization by evaluation" (nbe). There are lots of references for nbe.
András Kovács
<reference-request><type-theory><lambda-calculus>
Structural normalization algorithm for the simply typed lambda calculus
Couchy
# Structural normalization algorithm for the simply typed lambda calculus

(Asked by: username_0 on 2021-01-29)

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?

**Tags:** reference-request, type-theory, lambda-calculus
> **Comments:**
> **username_1**: Do you consider $M[N/x]$ to be a subterm of $(\lambda x.M)N$?  
> **username_0**: @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.  
> **username_2**: This is a core feature of "normalization by evaluation" (nbe). There are lots of references for nbe.  

---

## 1 answers

### Answer by username_3 on 2021-01-30. Score: 1

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>


---

