nLab Newman lemma




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.


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


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


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.