I'd like to learn the Newman's Lemma or Diamond Lemma (the one used in abstract rewriting system), can someone recommend me some books where I can read it? I'd appreciate self-contained books with examples. Thank you.
-
$\begingroup$ See also Chapter 1 in my book "Combinatorial Algebra: syntax and semantics" amazon.com/…. $\endgroup$– user6976Dec 26, 2017 at 16:12
-
$\begingroup$ @Mark Sapir : Thank you very much for the reference. $\endgroup$– John N.Dec 26, 2017 at 16:48
1 Answer
Franz Baader and Tobias Nipkow, Term Rewriting and All That is a book fully devoted to term rewriting; much of it is about applying the diamond lemma.
Vincent van Oostrom, Newman's proof of Newman's lemma proves the lemma itself on just 1 page. That's not the shortest proof.
Gert Smolka, Confluence and Normalization in Reduction Systems proves the diamond lemma in §15, after showing all sorts of related things. These notes are clearly written for computer scientists (the notations resemble Coq), but from what I've seen are fairly readable.
Kimmo Eriksson, Strong convergence and the polygon property of 1-player games, Discrete Mathematics, Volume 153, Issues 1--3, 1 June 1996, Pages 105--122 explores the "Polygon property theorem", which is similar to the diamond lemma. (It requires the play sequences to be of the same length, which makes it somewhat more restrictive, but its conclusion is accordingly stronger.)
George M. Bergman, The diamond lemma for ring theory, Advances in Mathematics, Volume 29, Issue 2, February 1978, Pages 178--218 (errata) applies the diamond lemma to the study of algebras.
As @MarkSapir pointed out, Mark Sapir, Combinatorial algebra: syntax and semantics, Springer 2014 has a section (§1.7) on confluence.
Marc Bezem, Thierry Coquand, Newman's Lemma -- a Case Study in Proof Automation and Geometric Logic proves a "bi-colored" analogue of Newman's lemma.
Lars Hellström, The Diamond Lemma for Power Series Algebras gives an analogue of the ring-theoretical diamond lemma for infinite-but-sort-of-convergent rewriting sequences (I am being deliberately vague here, since I've read only the motivating sections of this).
Self-containedness isn't really an issue in this subject; the proof of the lemma is usually less than a page long, and there are zero prerequisites. I once gave an expository talk about confluence that includes a proof of the diamond lemma.
-
$\begingroup$ I don’t know if it is a good place to learn about it, but a classical reference, in terms of establishing terminology and the proof techniques, is Gérard Huet, "Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems" $\endgroup$ Dec 26, 2017 at 18:23
-
$\begingroup$ Btw, I’m not 100% convinced about the self-contained was of the proof because the proof I know uses Noetherian induction, and the proof that Noetherian induction works is probably a subtle argument from logic or set-theory or something $\endgroup$ Dec 26, 2017 at 18:27
-
$\begingroup$ Oh, okay. I meant "self-contained up to the foundational questions", which are different from use to use anyway. The easiest case (apart from that when the system has only finitely many states) is when you assume an induction predicate over the term-rewriting relation; this is what Bezem and Coquand do, if I remember correctly. (See Definition 3.2 in their paper.) This might be annoyingly abstract to some, but it completely sidesteps constructivity issues, as far as I understand. $\endgroup$ Dec 26, 2017 at 19:29
-
$\begingroup$ @darijgrinberg: The transfinite induction is not needed. See the proof of 1.7.2 of my book. $\endgroup$– user6976Dec 27, 2017 at 0:00
-
$\begingroup$ @MarkSapir: Your proof of Theorem 1.7.10 (with its use of the termination condition) is not constructive either. The induction predicate in Bezem-Coquand is not really transfinite; for example, in the most commonly used case (when each rewriting step decreases some finite tuple with respect to lexicographic order), it boils down to a double (or triple? I forgot) induction. The resulting algorithm can be incredibly slow (Ackermann or worse), because it's not primitive recursive, but this is still allowed in constructivism. $\endgroup$ Dec 27, 2017 at 0:13