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.
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. Newman's original proof was considerably more complicated.
Diamond lemma
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.
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. https://doi.org/10.1145/322217.322230
- 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. Vol. 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".
External links
- Diamond lemma at PlanetMath.
- "Newman's Proof of Newman's Lemma", a PDF on the original proof, Archived July 6, 2017, at the Wayback Machine