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.
If the above two conditions hold, then the lemma states that → 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
Franz Baader, Tobias Nipkow, (1998) Term Rewriting and All That, Cambridge University Press ISBN 0-521-77920-0
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.
Harrison, p. 260, Paterson(1990), p. 354.
Paul M. Cohn, (1980) Universal Algebra, D. Reidel Publishing, ISBN 90-277-1254-9 (See pp. 25-26)
References
M. H. A. Newman. On theories with a combinatorial definition of "equivalence". Annals of Mathematics, 43, Number 2, pages 223–243, 1942.
Paterson, Michael S. (1990). Automata, languages, and programming: 17th international colloquium. Lecture Notes in Computer Science. 443. Warwick University, England: Springer. ISBN 978-3-540-52826-5.
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".
Undergraduate Texts in Mathematics
Graduate Studies in Mathematics
Hellenica World - Scientific Library
Retrieved from "http://en.wikipedia.org/"
All text is available under the terms of the GNU Free Documentation License
