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

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 $a 0 \to a 1 \to a 2 \to a 3 \to ...$ . 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 \to b$ and $a \to c$ , then there is an element d in A such that $b * \to d$ and $c * \to 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 * \to b$ and $a * \to c$ , there is an element d such that $b * \to d$ and $c * \to 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 * \to 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".

External links

This article is issued from Wikipedia - version of the Sunday, January 31, 2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.