Term Rewriting and All That Paperback August 28, 1999

by Franz Baader

Excellent Book

Genres: Computer Science, Mathematics, Logic, Programming

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.