Recursive Definition of Normal Form with explicit substitution

lambda-calculussubstitution

Context

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:

Neutral Form:

  • Every variable is in neutral form.
  • if $M$ is in neutral form and $N$ in normal form then $(M N)$ is in neutral form.

Normal 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.

Question

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?

Own Ideas

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.

Best Answer

Does the recursive definition make sense?

I'm guessing, this question in more formal terms would be "Are the two definitions equivalent?". To answer this, you can try to show that for every term $t$,

  1. if it has no more redexes, it is in II-normal form (short for "normal form by definition II")
  2. if it has at least one redex, then it is not in II-normal form* and it's also not neutral.

There we go:

  • If $t$ is a variable, it contains no more redexes and therefore we need to show (1). Trivially, a variable is in II-normal form.
  • If $t$ is a lambda $\lambda M$, then
    • if $M$ has no more redexes, then $\lambda M$ also has no more redexes, therefore we need to show (1). By the inductive hypothesis, $M$ is in II-normal form. Then by definition, $\lambda M$ is also in II-normal form.
    • if $M$ contains at least one more redex, then $\lambda M$ also contains at least one and therefore we need to show (2). We easily see that $\lambda M$ is not neutral. It remains to show that it is also not II-normal. According to the definition, $\lambda M$ can be in II-normal form if a) $M$ is also in II-normal form or b) if $\lambda M$ is neutral. However, regarding (a), by the induction hypothesis $M$ is not II-normal. Regarding (b), again $\lambda M$ can't be neutral because by definition lambda terms are not neutral. Point (2) has been shown.
  • If $t$ is an application $M\,N$, we separate cases again:
    • If $M$ and $N$ contain no more redexes, it is still possible for $M\,N$ to be a redex. It is a redex, if $M$ is a lambda term $\lambda M'$ and, therefore, $t$ is of the form $\lambda M'\, N$. We need to show that such a term is not in II-normal form. We will assume the opposite and arrive at a contradiction. Since $t$ is an application, the only way it can be in II-normal form is if it is neutral and, by definition, $\lambda M'\,N$ is neutral if $\lambda M'$ is neutral and $N$ is II-normal. However, lambdas are not neutral. We arrived at a contradiction. Therefore, $t = \lambda M'\, N$ is not in II-normal form.
    • If $N$ or $M$ contain at least one redex, then $M\,N$ also does, so we need to show (2). Again we will assume $M\,N$ is in II-normal form and reach a contradiction. Since $M\,N$ is in normal form, it must be the case that it is also neutral (by definition). This means that $M$ must be neutral and $N$ must be II-normal. From the induction hypothesis, if $N$ has redexes, then it is not in II-normal form and if $M$ has redexes then it is not neutral. Contradiction, hence $M\,N$ is not in II-normal form.

This proves that Definition II is equivalent to "is $\beta$-irreducible".

How to adapt Definition II to also account for substitution terms $t[s]$?

By the first definition, it is clear that $t[s]$ is in normal form when both $t$ and the term(s) in $s$ are. You need to append the above proof with one more inductive case for $t = M[N]$. How would you do that? How would you change Definition II so that the proof still holds?

*This is the contrapositive of saying, "if it is in II-normal form, it has no more redexes"

Related Question