# β-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.