# 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 (*A*,→) 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*,*y*)→*x*, the term *g*(*g*(4,2),*g*(3,1)) can be rewritten as follows, applying the rule to the outermost occurrence ^{[note 1]} of *g*:

(**g***g*(4,2),*g*(3,1)) →(4,2) → 4.**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*(4,2),*g*(3,1)) 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 { *g*(*x*,*y*)→*x*, *g*(*x*,*x*)→*g*(3,*x*) } is weakly,
^{[note 2]}
but not strongly
^{[note 3]}
normalizing, although each term not containing *g*(3,3) is strongly normalizing.
^{[note 4]}
The term *g*(4,4) has two normal forms in this system, viz. *g*(4,4) → 4 and *g*(4,4) → *g*(3,4) → 3, hence the system is not confluent.

Another example: The single-rule system { *r*(*x*,*y*)→*r*(*y*,*x*) } has no normalizing properties (not weakly or strongly), since from any term, e.g. *r*(4,2) a single rewrite sequence starts, viz. *r*(4,2)→*r*(2,4)→*r*(4,2)→*r*(2,4)→..., which is infinitely long.

## Normalization and Confluency

Newman's lemma states that if an abstract rewriting system *A* is strongly normalizing and is weakly confluent, then *A* is confluent.

The result enables us to further generalize the critical pair lemma.

## Notes

- ↑ each occurrence of
*g*where the rule is applied is highlighted in**boldface** - ↑ since every term containing
*g*can be rewritten by a finite number of applications of the first rule to a term without any*g*, which is in normal form - ↑ since to the term
*g*(3,3), the second rule can be applied over and over again, without reaching any normal form - ↑ For a given term, let
*m*and*n*denote the total number of*g*and of*g*applied to identical arguments, respectively. Application of any rule properly decreases the value of*m*+*n*, which is possible only finitely many times.

## References

- Baader, Franz; Nipkow, Tobias (1998).
*Term Rewriting and All That*. Cambridge University Press.