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 selfcontained books with examples. Thank you.

$\begingroup$ See also Chapter 1 in my book "Combinatorial Algebra: syntax and semantics" amazon.com/…. $\endgroup$ – Mark Sapir Dec 26 '17 at 16:12

$\begingroup$ @Mark Sapir : Thank you very much for the reference. $\endgroup$ – John N. Dec 26 '17 at 16:48
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 1player games, Discrete Mathematics, Volume 153, Issues 13, 1 June 1996, Pages 105122 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 178218 (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 "bicolored" analogue of Newman's lemma.
Lars Hellström, The Diamond Lemma for Power Series Algebras gives an analogue of the ringtheoretical diamond lemma for infinitebutsortofconvergent rewriting sequences (I am being deliberately vague here, since I've read only the motivating sections of this).
Selfcontainedness 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$ – Sam Hopkins Dec 26 '17 at 18:23

$\begingroup$ Btw, I’m not 100% convinced about the selfcontained 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 settheory or something $\endgroup$ – Sam Hopkins Dec 26 '17 at 18:27

$\begingroup$ Oh, okay. I meant "selfcontained 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 termrewriting 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$ – darij grinberg Dec 26 '17 at 19:29

$\begingroup$ @darijgrinberg: The transfinite induction is not needed. See the proof of 1.7.2 of my book. $\endgroup$ – Mark Sapir Dec 27 '17 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 BezemCoquand 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$ – darij grinberg Dec 27 '17 at 0:13