[(Term Rewriting and All That )] [Author: Franz Baader] [Jul-2006]

by Franz Baader

This is the first unified and self-contained introduction, in English, to the field of term rewriting, a high-level method for describing the behaviour of computer programs and for automating mathematical computations and proofs. The main algorithms are presented both informally and as programs in the ML language. Many examples and over 170 exercises are provided; each chapter closes with a guide to the literature. This text can be used for advanced undergraduate courses or as a professional it is the first time many of the results have been presented in book form.

Genres: Computer Science, Mathematics, Logic, Programming

Unknown Binding

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.