Normal form (abstract rewriting)


In abstract rewriting, an object is in normal form if it cannot be rewritten any further. Depending on the rewriting system and the object, several normal forms may exist, or none at all.

Definition

Stated formally, if is an abstract rewriting system, some x∈A is in normal form if no y∈A exists such that x→y.
For example, using the term rewriting system with a single rule g→x, the term g,g) can be rewritten as follows, applying the rule to the outermost occurrence of g:
Since no rule applies to the last term, 4, it cannot be rewritten any further, and hence is a normal form of the term g,g) with respect to this term rewriting system.

Normalization properties

Related concepts refer to the possibility of rewriting an element into normal form.
An object of an abstract rewrite system is said to be weakly normalizing if it can be rewritten somehow into a normal form, that is, if some rewrite sequence starting from it cannot be extended any further.
An object is said to be strongly normalizing if it can be rewritten in any way into a normal form, that is, if every rewrite sequence starting from it eventually cannot be extended any further.
An abstract rewrite system is said to be weakly and strongly normalizing, or to have the weak and the strong normalization property, if each of its objects is weakly and strongly normalizing, respectively.
For example, the above single-rule system is strongly normalizing, since each rule application properly decreases term size and hence there cannot be an infinite rewrite sequence starting from any term.
In contrast, the two-rule system is weakly,
but not strongly
normalizing, although each term not containing g is strongly normalizing.
The term g has two normal forms in this system, viz. g → 4 and g → g → 3, hence the system is not confluent.
Another example: The single-rule system has no normalizing properties, since from any term, e.g. r a single rewrite sequence starts, viz. r→r→r→r→..., which is infinitely long.

Normalization and confluency

states that if an abstract rewriting system A is strongly normalizing and is weakly confluent, then A is confluent.
The result enables to further generalize the critical pair lemma.