Term Rewriting and All That

by Franz Baader, Tobias Nipkow

This textbook offers a unified and self-contained introduction to the field of term rewriting. It covers all the basic material (abstract reduction systems, termination, confluence, completion, and combination problems), but also some important and closely connected subjects: universal algebra, unification theory, Gröbner bases and Buchberger's algorithm. The main algorithms are presented both informally and as programs in the functional language Standard ML (an appendix contains a quick and easy introduction to ML). Certain crucial algorithms like unification and congruence closure are covered in more depth and Pascal programs are developed. The book contains many examples and over 170 exercises. This text is also an ideal reference book for professional researchers: results that have been spread over many conference and journal articles are collected together in a unified notation, 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, Kindle Edition

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.