I assume a simply typed lambda calculus, probably written with de-bruijn indexes. With $\to_\beta$ I denote the $\beta$-reduction as a relation.
Also, my question eventually will use this $\lambda$-calculus with explicit substitution (originally called $\lambda\sigma$-calculus), where substitution is introduced on term level via closures $M[s]$ with $\lambda$-term M and substitution $s$.
A few definitions are needed.
Definition: Normal Form
A $\lambda$-term $M$ is in normal form, if there is no $\lambda$-term $N$ such that $M\to_\beta N$.
Besides this defintion, there is also another definition I'm ultimately interested in: defining normal form recursively:
Definition II: Neutral and Normal Form
Mutually defining neutral and normal forms:
- Every variable is in neutral form.
- if $M$ is in neutral form and $N$ in normal form then $(M N)$ is in neutral form.
- If $M$ is in neutral form, then $M$ is in normal form.
- If $M$ is in normal form, then $\lambda M$ is in normal form.
So far, this deals with the classical simply typed lambda calculus, where substitution is defined as a (meta-) function over terms. First: does this definition of normal forms make sense?
Then: Putting substitution into the term level, the question arises how to define normal forms then recursively as above?
My first go to was to add the following case to the definition of a normal form:
- If every term in $s$ is in neutral form and $t$ is in normal form, then $t[s]$ is in normal form.
Since neutral forms don't allow abstractions, even when dealing with closures like $(x y)[s]$, this should not introduce new $\beta$-redexes. But somehow, I'm unsure. Does this still resemble what NF means? After searching for information, there seems to be nothing like this.