Term Rewriting and All That

by Franz Baader, Tobias Nipkow

This textbook offers a unified, self-contained introduction to the field of term rewriting. Baader and Nipkow cover all the basic material--abstract reduction systems, termination, confluence, completion, and combination problems--but also some important and closely connected universal algebra, unification theory, Gröbner bases, and Buchberger's algorithm. They present the main algorithms both informally and as programs in the functional language Standard ML (An appendix contains a quick and easy introduction to ML). Key chapters cover crucial algorithms such as unification and congruence closure in more depth and develop efficient Pascal programs. The book contains many examples and over 170 exercises. This is also an ideal reference book for professional results spread over many conference and journal articles are collected here in a unified notation, detailed proofs of almost all theorems are provided, and each chapter closes with a guide to the literature.

Genres: Computer Science, Mathematics, Logic, Programming

316 pages, Paperback

First published March 5, 1998

Reviews

[Case · Rating 5 out of 5]

This book changed how I thought about computer science, logic, and language forever. By stripping down computation to its core - rewriting of syntax - we gain a powerful method of analysis. This is not some magical grand unifying theory, but I have found casting problems in this light to be very useful.

Initially, I purchased this book to help implement automated theorem provers. If we can state an equational theory as a term rewrite system and show that it is confluent and terminating, then we can form an algorithm for proving (or disproving) an equation; normalize both sides of the equation and then check if you end up at a reflexive equality.

The unexpected relationship I found was how term rewrite systems can provide a link between logic programming and dependently-typed programming. By constructing a type indexed by terms in our logic with each constructor corresponding to a rewrite, we end up with an effective technique of embedding a logical system.

[Hemanth Kapila · Rating 4 out of 5]

Tough going, especially the proofs, but absolutely spot on about the "All That" part of the title.