Advanced topics in term rewriting

Publication date 16 April 2002

Research exposition (monographs, survey articles) pertaining to computer science (68-02) Grammars and rewriting systems (68Q42)

Review text

The book starts with some motivating examples of Term Rewriting Systems (TRSs) (e.g. ``coffee can problem). Then, in chapter 2, abstract reduction systems are studied in the usual way (termination, confluence, partial orderings) but including reduction modulo an equivalence. Chapter 3 gives the basic notions of term rewriting. In chapter 4 first the undecidability of confluence is stated. Then the two most important methods for proving confluence are reviewed: proving termination and the joinability of all critical pairs or using orthogonality. Chapter 5 deals with termination of TRSs: after stating the undecidability of termination, standard methods (interpretation, simplification orderings) are reviewed. Next the termination hierarchy is introduced, followed by more sophisticated methods for proving termination such as the dependency pair method and transformational methods. The chapter ends up with the study of innermost termination. In the termination hierarchy (and similar in the confluence hierarchy) the implication \(X \Rightarrow Y\) for properties \(X\) and \(Y\) of TRSs means that every TRS satisfying \(X\) satisfies also \(Y\). Relative undecidability of of \(X\Rightarrow Y\) means that property \(X\) is undecidable for TRSs satisfying property \(Y\). In chapter 6 the relative undecidability is proved for all implications of the confluence hierarchy and for all implications of the termination hierarchy except \(PT\Rightarrow \varpi T\) (polynomial termination implies \(\varpi\)-termination), which is still an open question. For most implications of the termination hierarchy relative undecidability holds even for one-rule-systems. Chapter 7 addresses the important topic of conditional term rewriting, being much more complicated than unconditional rewriting. As for unconditional TRSs various methods for proving termination (effective termination) and confluence respectively of conditional TRSs are given. A property \(P\) is called modular for TRSs if, for all TRSs \(R_1\) and \(R_2\) having property \(P\) their union also has property \(P\). Chapter 8 gives first an overview of existing modularity results, most of them are not treated in detail. Then new modularity results are given: sufficient conditions for modularity of termination for disjoint union; sufficient conditions for modularity of confluence for constructor sharing systems (from which Toyamas theorem follows); modularity results for hierarchical combinations of TRSs. Finally modularity results for conditional TRSs are treated. Chapter 9 gives a new unified framework of graph rewriting and term rewriting -- called marked rewriting. It is demonstrated that this framework can be used to establish general results and then to obtain results for term rewriting and graph rewriting as corollaries. The last chapter deals with methods for proving termination of well-moded logic programs using techniques which transform the logic program into a TRS. There are other books on TRSs but these are in fact introductory textbooks whereas Ohlebusch's book covers several important fields in term rewriting that go beyond the scope of an introductory book -- especially fields to which the author himself made essential contributions. In this way this monograph is an outstanding one, suitable for all Computer scientists who study and use term rewriting. On the other hand some essential topics such as unification and completion are not dealt with. So for an introductory course the book has to be supplemented with other material.

Recommendations

Cited in

(only showing first 100 items - show all)

This page was built for publication: Advanced topics in term rewriting

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2783416)