Newman's lemma
In theoretical computer science, specifically in term rewriting, Newman's lemma, also commonly called the diamond lemma, is a criterion to prove that an abstract rewriting system is confluent. It states that local confluence is a sufficient condition for confluence, provided that the system is also terminating. This is useful since local confluence is usually easier to verify than confluence.
The lemma was originally proved by Max Newman in 1942. A considerably simpler proof was proposed by Gérard Huet. A number of other proofs exist.
Statement and proof
The lemma is purely combinatorial and applies to any relation. Owing to the context where it is commonly applied, it is stated below in the terminology of abstract rewriting systems.Newman's lemma: If an abstract rewriting system is terminating and locally confluent, then it is confluent. As a corollary, every term has a unique normal form.
Proof: We prove by well-founded induction on along that every diagram
[Image:Proof of Newman's lemma (1).svg|center|frameless|upright=0.8|Diagram with arrows (arrows are dotted to express that they represent sequences of arbitrarily many reduction steps)]
can be extended to a diagram
[Image:Proof of Newman's lemma (2).svg|center|frameless|upright=0.8|Diagram with arrows ]
where the dotted arrows represent sequences of arbitrarily many reductions by.
If or, this is trivial. Otherwise, we have at least one reduction on each side:
[Image:Proof of Newman's lemma (3).svg|center|frameless|upright=1.5|alt=Diagram with arrows ]
By local confluence, this diagram can be extended to:
[Image:Proof of Newman's lemma (4).svg|center|frameless|upright=1.5|alt=Diagram with arrows ]
then by induction hypothesis on :
[Image:Proof of Newman's lemma (5).svg|center|frameless|upright=1.5|alt=Diagram with arrows ]
and finally, by induction hypothesis on :
[Image:Proof of Newman's lemma (6).svg|center|frameless|upright=1.5|alt=Diagram with arrows ]
Eriksson's polygon property lemma
A related result was shown by Kimmo Eriksson in 1993. Recall that an abstract rewriting system is locally confluent if for any two reductions and, there exists such that and. If additionally it is required that the reduction chains and have the same length, then the system is said to have the polygon property. Examples of rewriting systems with the polygon property include bubble sort and the chip-firing game.Eriksson's polygon property lemma shows that if an abstract rewriting system is terminating and has the polygon property, then not only is it confluent, but additionally every terminating chain of reductions from a given state has the same length.