nLab Newman's lemma

Idea

Newman’s lemma implies good properties (confluence) of a rewriting system based on satisfaction of a “diamond condition” on generating moves:

With the lemma it is sufficient to verify the weaker property of local confluence, once strong normalization is established (assuming that the rewriting system does possess these two properties).

Statement

Let $(X,\rightarrow)$ be an abstract rewriting system ie. a set equipped with a binary relation $\rightarrow$. The Newman lemma asserts that:

Proposition

If $\rightarrow$ is strongly normalizing and locally confluent then it is confluent.

Related concepts

• rewriting

• diamond

• confluence

• Church-Rosser theorem,

References

The original article:

• Maxwell H. A. Newman, On theories with a combinatorial definition of “equivalence”, Annals of Mathematics 43 2 (1942) 223–243 [doi:10.2307/2269299]

See also:

• Wikipedia article

• (Širšov-Bergman) diamond lemma (zoranskoda lab)