Term Rewriting and All That

by Franz Baader , Tobias Nipkow

• ISBN13: 9780521455206
• ISBN10: 0521455200
• Format: Hardcover
• Copyright: 1998-03-13
• Publisher: Cambridge University Press

Summary

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 subjects: 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 researchers: 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.

Table of Contents

Preface	ix
1 Motivating Examples	1	(6)
2 Abstract Reduction Systems	7	(27)
2.1 Equivalence and reduction	7	(6)
2.2 Well-founded induction	13	(3)
2.3 Proving termination	16	(2)
2.4 Lexicographic orders	18	(3)
2.5 Multiset orders	21	(5)
2.6 Orders in ML	26	(2)
2.7 Proving confluence	28	(5)
2.8 Bibliographic notes	33	(1)
3 Universal Algebra	34	(24)
3.1 Terms, substitutions, and identities	34	(10)
3.2 Algebras, homomorphisms, and congruences	44	(3)
3.3 Free algebras	47	(2)
3.4 Term algebras	49	(1)
3.5 Equational classes	49	(9)
4 Equational Problems	58	(35)
4.1 Deciding Congruence E	59	(2)
4.2 Term rewriting systems	61	(1)
4.3 Congruence closure	62	(3)
4.4 Congruence closure on graphs	65	(6)
4.5 Syntactic unification	71	(2)
4.6 Unification by transformation	73	(6)
4.7 Unification and term rewriting in ML	79	(3)
4.8 Unification of term graphs	82	(9)
4.9 Bibliographic notes	91	(2)
5 Termination	93	(41)
5.1 The decision problem	93	(8)
5.2 Reduction orders	101	(3)
5.3 The interpretation method	104	(7)
5.4 Simplification orders	111	(20)
5.5 Bibliographic notes	131	(3)
6 Confluence	134	(24)
6.1 The decision problem	134	(1)
6.2 Critical pairs	135	(10)
6.3 Orthogonality	145	(6)
6.4 Beyond orthogonality	151	(6)
6.5 Bibliographic notes	157	(1)
7 Completion	158	(29)
7.1 The basic completion procedure	160	(4)
7.2 An improved completion procedure	164	(8)
7.3 Proof orders	172	(6)
7.4 Huet's completion procedure	178	(4)
7.5 Huet's completion procedure in ML	182	(2)
7.6 Bibliographic notes	184	(3)
8 Grobner Bases and Buchberger's Algorithm	187	(13)
8.1 The ideal membership problem	187	(2)
8.2 Polynomial reduction	189	(4)
8.3 Grobner bases	193	(3)
8.4 Buchberger's algorithm	196	(2)
8.5 Bibliographic notes	198	(2)
9 Combination Problems	200	(23)
9.1 Basic notions	200	(2)
9.2 Termination	202	(5)
9.3 Confluence	207	(4)
9.4 Combining word problems	211	(11)
9.5 Bibliographic notes	222	(1)
10 Equational Unification	223	(42)
10.1 Basic definitions and results	224	(6)
10.2 Commutative functions	230	(6)
10.3 Associative and commutative functions	236	(14)
10.4 Boolean rings	250	(12)
10.5 Bibliographic notes	262	(3)
11 Extensions	265	(11)
11.1 Rewriting modulo equational theories	265	(2)
11.2 Ordered rewriting	267	(2)
11.3 Conditional identities and conditional rewriting	269	(1)
11.4 Higher-order rewrite systems	270	(1)
11.5 Reduction strategies	271	(2)
11.6 Narrowing	273	(3)
Appendix 1 Ordered Sets	276	(2)
Appendix 2 A Bluffer's Guide to ML	278	(6)
Bibliography	284	(13)
Index	297