nLab Newman lemma

Contents

Contents

Idea

The Newman lemma is a useful result to prove good properties of a rewriting system. At the best, a rewriting system is strongly normalizing and confluent. The lemma allows to verify only the weaker property of local confluence, once we have first proved the strong normalization, in the case where the rewriting system possesses these two good 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 August 6, 2022 at 15:46:44. See the history of this page for a list of all contributions to it.