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$ – 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

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$ – Sam Hopkins Dec 26 '17 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$ – Sam Hopkins Dec 26 '17 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$ – 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 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$ – darij grinberg Dec 27 '17 at 0:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.