nLab Newman's lemma

Contents

Contents

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,)(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.

References

The original article:

See also:

Last revised on April 17, 2023 at 14:44:04. See the history of this page for a list of all contributions to it.