8
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ See also Chapter 1 in my book "Combinatorial Algebra: syntax and semantics" amazon.com/…. $\endgroup$
    – user6976
    Dec 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 1

16
$\begingroup$

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.

$\endgroup$
13
  • $\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$
    – user6976
    Dec 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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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