====================================================================== Review of "Term Rewriting Systems" by Terese Jean-Pierre Jouannaud (The Computer Journal, Volume 47(1), January 2004, p. 135) ====================================================================== This book, written by Terese, a group of close colleagues, collaborators, and former students of Jan Willem Klop from Amsterdam, covers a rather large part of what is nowadays known as the field of term rewriting systems. Contrary to most books and surveys in this field, this book covers first-order as well as higher-order rewriting systems in depth, with some emphasis on the properties that rewriting and lambda calculus share. This work is actually a collection of articles written by several authors who tried, sometimes with great success, to write their chapters in a similar, fluent style, with limited redundancy, detailed proofs, many examples, nice looking diagrams, and lots of exercises of various difficulty. As of today, there no such ambitious book on the market. It will help, and sometimes please those interested in \emph{almost all aspects} of rewriting systems, whether first- or higher-order, and in the relationships between rewriting systems and lambda calculi. I would not recommend it to beginners, however, it is a book for teaching graduate courses on these topics, or for the researcher who needs to refresh his memory about all possible ways to track down some complex confluence-like property of rewriting systems. At first sight the organization of the book seems dificult to follow. The two subjects terminating rewrite systems and orthogonal rewrite systems are intermixed, making two books in one. However, orthogonal rewrite systems form the core of the book: they are covered in a great depth to the point that several important theorems are stated and proved several times, with different perspectives and proof techniques. In contrast, some aspects of terminating rewriting systems have a sometimes limited and even poor coverage. Very few improvements are needed to make this book into a very good book: more uniformity in the writing of chapters, a better account of plain and AC terminating rewriting systems, improving the two weak Chapters 6 and 7, and perhaps a slightly better structuring. However, already in its present form, this book is a pleasure to read, and should be very useful, and a good companion to Baader and Nipkow's book "Term Rewriting and all that" whose weaknesses meet the present one strong parts. Both books will stand side by side on my bookshelf. Rather than giving a detailed account of all the chapters, I will now illustrate my general opinion by picking up some topics that I liked or disliked in each of them. The introduction is useful, with three interesting examples, among which the one on knot transformations is -as far as I can tell- original. Chapters 1 and 2 are well written and very useful : the goal here is to give the setting (both abstract and concrete) and present the fundamental concept of rewriting when used as a language for describing computations. Chapter 3 follows, like a second introduction, once the basics are known. This was a good idea to give many more examples and motivations at this stage. Chapter 4 discusses a concept central to non-terminating computations, orthogonality, which applies to both lambda calculus, first-order and higher-order rewriting, although only the first-order rewriting case is carried out at this stage. It is as expected very well written considering the considerable amount of work done in this area by the authors of the chapter, who gave in particular the first understandable proof of decidability of strong sequentiality for non-linear, non-ambiguous term rewriting systems. I don't like the idea of making this Chapter 5. The first half of the material would fit better in Chapter 3. The second part would merit a chapter of its own. I do not like Chapter 6. My opinion may of course be biased, since this is a topic which I know extremely well. Many interesting proofs are missing, such as the correctness of the dependency pairs method. By the way, it should be stressed that this method is important for pratice, as are all those that transform a termination problem into a constraint satisfaction problem, because of their potential for automation. The "syntactical methods" are poorly presented, with extremely complex "justifications" for the recursive path order which point out a wrong understanding of multiset and lexicographic extensions of (arbitrary) relations. It would have been far more useful to cover AC-termination than to spend so much effort on total and simple termination, even if the latter is an important concept. "Divide and conquer" methods based either on commutation criteria or on disjoint signatures are not very well covered either. It would have been important to say a bit about the tools aiming at supporting termination proofs. For example, the explicit substitution calculus can be proved terminating by CiME, using polynomial interpretations on finite domains which can be computed automatically. References are not always accurate : the relationship between termination of TRS and reduction orders appears in an early paper of Manna and Ness (instead of Lankford 79). More important, this chapter is overflooded with useless references to the work of the author or to other minor results, while many important ones are missing. Such a bias should not occur in a textbook like this. I hope that future editions will include an improved reference section. Chapter 7 is is in the same vein. Metivier's Theorem 7.4.9 was suggested earlier by Lankford, without a proof, and proved independently by Dershowitz (in unpublished notes written for a series of seminars at NASA, as far as I remember). It should be mentioned that the first proof of Knuth-Bendix completion (acting as semi-decision procedure when it diverges) was given by Huet in a paper which is not cited here. This paper was important by introducing the concept of fairness and showing its necessity. Section 7.6 does not cite Musser's paper who initiated the idea of proof by consistency, nor what I consider the 4 most important works in this area by: Huet-Hullot (CADE80?), Jouannaud-Kounalis (LICS85, containing Definition 7.6.4 and Theorem 7.6.5), Fribourg (ICALP85), and Comon (2000 approximately). I would also recommend a more recent reference than Siekmann (84,89) to refer to the area of unification and E-unification. As far as I recall, the so-called "Martelli-Montanari" rules for unification displayed in Table 7.9 are not due to these authors who actually used transformation rules operating on "multiequations" in their (unpublished, I think) 78 paper. The rule presentation with equations appeared first in a paper by Colmerauer in 82 (it did not appear so clearly in Herbrand, although Herbrand's presentation -I think- inspired Colmerauer and was closer to Table 7.9 than Martelli-Montanari's). Besides, the major innovation of Martelli-Montanari was the so-called "merge rule" which is not even in the table, and leads to a clear understanding of why unification is indeed linear. See the chapter "Rewriting Rules" in the Handbook of Theoretical Computer Science, where these aspects are covered correctly, or the chapter "Solving equations in abstract algebras" in the anniversary book for Alan Robinson edited by Lassez and Plotkin. I hope again that future editions will include an improved chapter. Chapters 8 and 9 are extremely interesting, they present a lot of recent and even novel material, but must be read in detail for a good understanding. I was impressed by the excellent grasp of the complex literature on the subject by the authors of this chapter, and by the amount of research work done here. Minor suggestions for future elaboration are the following: it has been noted that the optimal strategy had a very strong link with linear logic (see Abadi-Gonthier-Levy and others who succeeded to reformulate in this setting Lamping's work); I was therefore surprised to see that the ideas originating from linear logic that finally lead to the solution of Levy's problem were not described in this chapter, where only sharing graphs are used -which seem quite close to Girard's visual representation of linear logic proofs!-; what is the precise link between both? The recent work by Fernandez and Mackie along these lines is relevant as well, I think. Chapter 10 is interesting as well, covering various confluent/non-confluent extensions of lambda calculus here is a good idea. The coverage of typed lambda calculi is extremely brief -an entire chapter would have been needed for a good understanding- and can hardly compete with the illuminating chapter "Typed Lambda Calculi" by Henk Barendregt in the Handbook of Logic in Computer Science. Indeed, why should it be included at all in a book which is entirely about untyped computations ? Chapter 11 introduces the reader to a quite recent and important research area that will probably have moved on by the time the book is revised: it introduces and compares different formats for higher-order rewriting, an area still under active development. Chapter 12 is about infinitary rewriting. Chapter 13 is about graph rewriting, which is an important subject of its own and would merit an entire book, but I understand the desire to give a quick overview, since graph rewriting is present in all reasonable implementations of functional languages. Chapter 14 is a very nice abstract presentation of confluence proofs which I had the opportunity to review in the past for a journal publication. It could have been presented at an earlier stage. Chapter 15 is very interesting and useful, but needs to be a bit more complete. For example, the CiME system should be included in the list as one of the most powerful system for automating termination proofs. In retrospect, one can even say that this book was not ambitious enough to give the mathematics needed to understand all these systems. For example, how could the book's presentation of simply typed lambda-calculus help understanding ACL2, Automath or Coq ?