book announcement: Terese

                         Book announcement

Term Rewriting Systems

by Terese

Cambridge Tracts in Theoretical Computer Science 55
Cambridge University Press 2003, ISBN 0521391156, Hardback, 90.00

906 pages, 273 line diagrams, 500 bibliographical references,
2500 index entries, 334 exercises

solutions to selected exercises will appear on the book website

Term rewriting systems (TRSs) developed out of mathematical logic and
are an important part of theoretical computer science. They describe
sequences of discrete transformation steps where one term is replaced
with another. TRSs have applications in many areas, from functional
programming to automatic theorem proving and computer algebra. This book
starts at an elementary level with the earlier chapters providing a
foundation for the rest of the work. The later chapters contain more
advanced material, appearing here for the first time in book form.
Subjects treated include confluence, termination, orthogonality,
completion, lambda calculus, higher-order rewriting, infinitary
rewriting and term graph rewriting. Many exercises are included with
selected solutions provided on the web. A chapter is included presenting
applications of term rewriting systems, with many pointers to actual
implementations. A comprehensive bibliography makes this book ideal
both for teaching and research. The necessary mathematical background
has been collected in an appendix.


 1. Abstract reduction systems
 2. First-order term rewriting systems
 3. Examples of TRSs and special rewriting formats
 4. Orthogonality
 5. Properties of rewriting: decidability and modularity
 6. Termination
 7. Completion of equational specifications
 8. Equivalence of reductions
 9. Strategies
10. Lambda calculus
11. Higher order rewriting
12. Infinitary rewriting
13. Term graph rewriting
14. Advanced ARS theory
15. Rewriting-based languages and systems
Appendix. Mathematical background.