Show Question
Math and science::Theory of Computation::Lambda calculus

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

Source

Nederpelt, Type Theory and Formal Proof