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)) → g(4,2) → 4.

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

  1. ↑ each occurrence of g where the rule is applied is highlighted in boldface
  2. ↑ 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
  3. ↑ since to the term g(3,3), the second rule can be applied over and over again, without reaching any normal form
  4. ↑ 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