Newman's lemma

In mathematics, in the theory of rewriting systems, Newman's lemma, also commonly called the diamond lemma, states that a terminating (or strongly normalizing) abstract rewriting system (ARS), that is, one in which there are no infinite reduction sequences, is confluent if it is locally confluent. In fact a terminating ARS is confluent precisely when it is locally confluent.[1]

Equivalently, for every binary relation with no decreasing infinite chains and satisfying a weak version of the diamond property, there is a unique minimal element in every connected component of the relation considered as a graph.

Today, this is seen as a purely combinatorial result based on well-foundedness due to a proof of Gérard Huet in 1980.[2] Newman's original proof was considerably more complicated.[3]

Diamond lemma
Proof idea (straight and wavy lines denoting → and ∗→, respectively):
Given t1 ∗←t∗→t2, perform an induction on the derivation length. Obtain t′ from local confluence, and t′′ from the induction hypothesis; similar for t′′′.

In general, Newman's lemma can be seen as a combinatorial result about binary relations → on a set A (written backwards, so that a → b means that b is below a) with the following two properties:

  • → is a well-founded relation: every non-empty subset X of A has a minimal element (an element a of X such that a → b for no b in X). Equivalently, there is no infinite chain a0 → a1 → a2 → a3 → .... In the terminology of rewriting systems, → is terminating.
  • Every covering is bounded below. That is, if an element a in A covers elements b and c in A in the sense that a → b and a → c, then there is an element d in A such that b ∗→ d and c ∗→ d, where ∗→ denotes the reflexive transitive closure of →. In the terminology of rewriting systems, → is locally confluent.

The lemma states that if the above two conditions hold, then → is confluent: whenever a ∗→ b and a ∗→ c, there is an element d such that b ∗→ d and c ∗→ d. In view of the termination of →, this implies that every connected component of → as a graph contains a unique minimal element a, moreover b ∗→ a for every element b of the component.[4]

Notes
  1. Franz Baader, Tobias Nipkow, (1998) Term Rewriting and All That, Cambridge University Press ISBN 0-521-77920-0
  2. Gérard Huet, "Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems", Journal of the ACM (JACM), October 1980, Volume 27, Issue 4, pp. 797–821.
  3. Harrison, p. 260, Paterson (1990), p. 354.
  4. Paul M. Cohn, (1980) Universal Algebra, D. Reidel Publishing, ISBN 90-277-1254-9 (See pp. 25–26)

References

Textbooks
  • Term Rewriting Systems, Terese, Cambridge Tracts in Theoretical Computer Science, 2003. (book weblink)
  • Term Rewriting and All That, Franz Baader and Tobias Nipkow, Cambridge University Press, 1998 (book weblink)
  • John Harrison, Handbook of Practical Logic and Automated Reasoning, Cambridge University Press, 2009, ISBN 978-0-521-89957-4, chapter 4 "Equality".
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.