β-normal form
β-normal form
Let \( M \) be a lambda term.
- \( M \) is said to be in β-normal form iff \( M \) does not contain any redex.
- \( M \) is said to have a β-normal form iff \( M \betaEq U \) for some lambda term \( U \) that is in β-normal form.
The definition of redex is recalled on back side.
The notion of β-normal form captures a sense of the result of a lambda term; from a β-normal form, no further lambda computation is possible.
The following definition elaborates the concept by considering how many normal forms a term might have.
Weakly normalizing and strongly normalizing
Let \( M \) be a lambda term.
- \( M \) is said to be weakly normalizing iff it has a β-normal form.
- \( M \) is said to be strongly normalizing iff there are no infinite reduction paths starting from \( M \).
The two definitions below are referenced in the above material.
Redex and contractum
A subterm of a lambda expression is called a redex, from reducible expression, if it matches the left-hand side of the basis rule above. The subterm on the right-hand side, \( M[x:=U] \) is called the contractum of the redex.
Reduction path
Let \( M \) be a lambda term. A reduction path from \( M \) is a sequence of lambda terms \( (U_n)_{n=0}^{N} \) such that \( M \equiv N_0 \) and \( U_n \betaReduction U_{n+1} \) for every \( 0 \le n \le N \).
A reduction path with an infinite term sequence is called an infinite reduction path.
β-normal form: why \( M \betaEq U \) rather than \( M \multiBetaReduction U \)
It may seem like the multi-step reduction is more appropriate in the definition of the normal form. I think it is in fact true; however, to show it to be true, one must use the confluence theorem. I find this surprising, which suggests that I don't understand the flexibility of the \( \betaEq \) relation.
Finite computation guarantee
The below lemma follows from the definition of strongly normalizing:
A lambda terms is guaranteed to reduce to a β-normal form in finite steps iff it is strongly normalizing.
An interesting part of this lemma is that lambda terms that are not strongly normalizing might reduce to a β-normal form in finite steps or might get stuck in an infinite reduction loop.