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.[1][2] A considerably simpler proof (given below) was proposed by Gérard Huet.[3] A number of other proofs exist.[4]

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 (this is simply a set whose elements are called terms, equipped with a relation called reduction, and see the corresponding article for definitions of termination, confluence, local confluence and normal forms).

Newman's lemma:[5][6][7][8] 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

Diagram with arrows '"`UNIQ--postMath-00000004-QINU`"' (arrows are dotted to express that they represent sequences of arbitrarily many reduction steps)
Diagram with arrows (arrows are dotted to express that they represent sequences of arbitrarily many reduction steps)

can be extended to a diagram

Diagram with arrows '"`UNIQ--postMath-00000005-QINU`"'
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:

Diagram with arrows '"`UNIQ--postMath-00000009-QINU`"'

By local confluence, this diagram can be extended to:

Diagram with arrows '"`UNIQ--postMath-0000000A-QINU`"'

then by induction hypothesis on :

Diagram with arrows '"`UNIQ--postMath-0000000C-QINU`"'

and finally, by induction hypothesis on :

Diagram with arrows '"`UNIQ--postMath-0000000E-QINU`"'

References

  1. ^ Newman, Max (1942). "On theories with a combinatorial definition of "equivalence"". Annals of Mathematics. 43 (2): 223–243.
  2. ^ van Oostrom, Vincent. "Newman's Proof of Newman's Lemma" (PDF). Archived from the original (PDF) on April 15, 2024.
  3. ^ Huet, Gérard (1980). "Confluent reductions: Abstract properties and applications to term rewriting systems". Journal of the ACM. 27 (4): 797–821. doi:10.1145/322217.322230.
  4. ^ Klop, Jan Willem (1990). "Term rewriting systems: From Church-Rosser to Knuth-Bendix and Beyond". Automata, languages, and programming: 17th international colloquium. Lecture Notes in Computer Science. Vol. 443. Warwick University, England: Springer. pp. 350–369. doi:10.1007/BFb0032044. ISBN 978-3-540-52826-5.
  5. ^ Baader, Franz; Nipkow, Tobias (1998). Term Rewriting and All That. Cambridge University Press. doi:10.1017/CBO9781139172752. ISBN 0-521-77920-0.
  6. ^ Terese (2003). Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press.
  7. ^ Harrison, John (2009). Handbook of Practical Logic and Automated Reasoning. Cambridge University Press. p. 260. ISBN 978-0-521-89957-4.
  8. ^ Cohn, Paul Moritz (1980). Universal Algebra. D. Reidel Publishing. p. 25–26. ISBN 90-277-1254-9.
Allikas: http://en.wikipedia.org/wiki/Newman%27s_lemma
No tags for this post.