Normal form (abstract rewriting)

In abstract rewriting,[1] an object is in normal form if it cannot be rewritten any further, i.e. it is irreducible.

Many properties of rewriting systems relate to normal forms.

Stated formally, if (A,→) is an abstract rewriting system, x∈A is in normal form if no y∈A exists such that x→y, i.e. x is an irreducible term.

A rewriting system has the unique normal form property with respect to reduction (UN→) if for every term reducing to normal forms a and b, a is equal to b.

{a→b,a→c,b→b} is UN but not NF as b=c, c is a normal form, and b does not reduce to c. {a→b,a→c,b→b,c→c} is NF as there are no normal forms, but not CR as a reduces to b and c, and b,c have no common reduct.

Hence CR, NF, UN, and UN→ coincide if WN holds.

A remarkable fact is that all arithmetic expressions have a unique value, so the rewriting system is strongly normalizing and confluent:[6] Examples of non-normalizing systems (not weakly or strongly) include counting to infinity (1 ⇒ 2 ⇒ 3 ⇒ ...) and loops such as the transformation function of the Collatz conjecture (1 ⇒ 2 ⇒ 4 ⇒ 1 ⇒ ..., it is an open problem if there are any other loops of the Collatz transformation).

[7] Another example is the single-rule system { r(x,y) → r(y,x) }, which has no normalizing properties since from any term, e.g. r(4,2) a single rewrite sequence starts, viz.

Although this is a very useful property, it has a drawback: a programming language with the normalization property cannot be Turing complete, otherwise one could solve the halting problem by seeing if the program type checks.

This means that there are computable functions that cannot be defined in the simply typed lambda calculus, and similarly for the calculus of constructions and System F. A typical example is that of a self-interpreter in a total programming language.