Book review

Advanced Topics in Term Rewriting by Enno Ohlebusch, Springer-Verlag, 2002, hard cover: ISBN 0-387-95250-0, xi + 414 pages.

Term rewriting techniques play a role in many areas in computer science, for instance automated deduction, functional and functional-logic programming, and computer algebra. The book presents, besides the basics of term rewriting, contributions to the theory of term rewriting, in particular to the themes conditional rewriting and modularity. Especially for those subjects, the book provides a well-written overview of recent research with many references to the literature, and hence has clearly an added value over a collection of papers. Also the advanced part of the chapter on termination has this property. Moreover, the book contains a pleasant surprise in the form of a chapter on termination of logic programs.

The book is very useful for researchers interested in term rewriting, and in particular in conditional rewriting and modularity. As the title of the book already indicates, it is not very suitable for teaching a basic term rewriting course. However, it can be very well used for a seminar for advanced students who already know the basics of term rewriting.

The book consists of 10 chapters and an appendix.

1. Motivation

2. Abstract Reduction Systems

3. Term Rewriting Systems

4. Confluence

5. Termination

6. Relative Undecidability

7. Conditional Rewrite Systems

8. Modularity

9. Graph Rewriting

10. Proving Termination of Logic Programs

Appendix A: Kruskal's Theorem

The basics of term rewriting are presented in the Chapters 1-5. This part is mainly included to make the book self-contained and fix notation and terminology, as it is claimed both by the title and in the preface that the book is not an introductory textbook. Like the remainder of the book, it is written in a clear and rigorous way.

The chapter on abstract rewriting also contains two more advanced subjects: rewriting modulo an equivalence and decreasing diagrams which is a general method to prove confluence.

A large part of the chapter on termination is concerned with more advanced material such as the termination hierarchy, dependency pairs, transformational methods, and innermost termination.

Chapter 6 is devoted to relative undecidability results and is based on two papers by Geser, Middeldorp, Ohlebusch and Zantema. The issue of relative undecidability is the following one: consider for example the statement `termination implies that there are no loops'. It is shown that for systems with no loops, termination is still undecidable. For 6 implications concerning termination relative undecidability is shown for one-rule systems. Further, for 12 implications concerning termination or confluence, relative termination is shown (for many-rule systems).

Chapter 7 contains a wealth of material on conditional term rewriting, a subject that is very important for functional-logic programming, and forms in my opinion together with Chapter 8 on modularity the core of the book. The author has contributed a lot to the study of conditional rewriting, but the chapter is more than a collection of his results, since it also provides a nice overview of conditional rewriting and hence forms a good starting point for a study of the subject.

Chapter 8 is concerned with modularity. The issue here is the following: if we combine two term rewriting systems with property $P$, does the combination also have property $P$? This line of research was initiated by Toyama who showed in 1987 that confluence is a modular property, and termination is not. Since then modularity has been studied for many properties. Moreover, many different ways of combining systems have been considered: for instance systems with no function symbols in common, systems that share only constructor symbols but no defined symbols, and hierarchical combinations. The author has contributed many results to the study of modularity, but as is the case for Chapter 7, also this chapter is more than a collection of his results. A large selection of results on modularity is presented, without claiming completeness.

Chapter 9 is concerned with a special presentation of directed acyclic graphs using marked terms. Modularity of termination for graph rewriting is shown in this setting, and in addition conditional graph rewriting is studied.

Finally, Chapter 10 presents a method to show termination of well-moded logic programs by a transformation into conditional term rewriting systems. The system TALP (termination analysis of logic programs) is an implementation of this method. TALP uses the system CiME which is developed at the University of Orsay.

The book is based on the author's `Habilitationsschrift' and hence is mainly concerned with the contributions of the author to the theory of rewriting. In addition, the basics of term rewriting are presented to make the book self-contained. I find in particular the more advanced part of Chapter 5 on termination, Chapter 7 on conditional rewriting, and Chapter 8 on modularity more than a collection of the results obtained by the author; they form an excellent starting point to study these subjects. However, I don't really see what Chapter 9 on graph rewriting, no matter how interesting, adds to the two journal papers on which it is based. The same holds to a slightly lesser extent for Chapter 6 on relative undecidability, which is also based on two journal papers. This makes the book maybe slightly unbalanced: on the one hand there are chapters (7, 8, and the advanced part of 5) which present well-organised selections of recent results, and on the other hand there are chapters (6 and 9) which really have a `third thesis character' in the sense that they mainly report what is already in the journal papers.

Nevertheless, my opinion on this book is very positive, mainly because of my three favorite chapters. Also, I find the presentation in general very good. The style of writing is rigorous and clear, and the material is well organized. There are not so many figures, but there are nice tables with overviews of results. It is easy to find something and it is also not very difficult to conclude that a certain issue is not treated in the book - this is also very important especially since for all subjects a selection of results is presented. Therefore I very much recommend the book for researchers and advanced students interested in the theory of rewriting.

FEMKE VAN RAAMSDONK
Vrije Universiteit, Amsterdam, The Netherlands