Table of Contents
Preface
1 Motivating Examples
2 Abstract Reduction Systems
2.1 Equivalence and reduction
2.1.1 Basic definitions
2.1.2 Basic results
2.2 Well-founded induction
2.3 Proving termination
2.4 Lexicographic orders
2.5 Multiset orders
2.6 Orders in ML
2.6.1 Lexicographic orders
2.6.2 Multiset orders
2.7 Proving confluence
2.8 Bibliographic notes
3 Universal Algebra
3.1 Terms, substitutions, and identities
3.2 Algebras, homomorphisms, and congruences
3.3 Free algebras
3.4 Term algebras
3.5 Equational classes
4 Equational Problems
4.1 Deciding =E
4.2 Term rewriting systems
4.3 Congruence closure
4.4 Congruence closure on graphs
4.5 Syntactic unification
4.6 Unification by transformation
4.7 Unification and term rewriting in ML
4.8 Unification of term graphs
4.8.1 A quadratic algorithm
4.8.2 An almost linear algorithm
4.8.3 The complexity of sharing
4.9 Bibliographic notes
5 Termination
5.1 The decision problem
5.1.1 Undecidability in the general case
5.1.2 A decidable subcase
5.2 Reduction orders
5.3 The interpretation method
5.4 Simplification orders
5.4.1 Polynomial simplification orders
5.4.2 Recursive path orders
5.4.3 Recursive path orders in ML
5.4.4 Knuth-Bendix orders
5.5 Bibliographic notes
6 Confluence
6.1 The decision problem
6.2 Critical pairs
6.3 Orthogonality
6.4 Beyond orthogonality
6.5 Bibliographic notes
7 Completion
7.1 The basic completion procedure
7.2 An improved completion procedure
7.3 Proof orders
7.4 Huet's completion procedure
7.5 Huet's completion procedure in ML
7.6 Bibliographic notes
8 Gröbner Bases and Buchberger's Algorithm
8.1 The ideal membership problem
8.2 Polynomial reduction
8.3 Gröbner bases
8.4 Buchberger's algorithm
8.5 Bibliographic notes
9 Combination Problems
9.1 Basic notions
9.2 Termination
9.3 Confluence
9.3.1 The disjoint case
9.3.2 The orthogonal case
9.4 Combining word problems
9.4.1 The key ideas
9.4.2 The formal solution
9.4.3 Correctness
9.4.4 The implementation in ML
9.5 Bibliographic notes
10 Equational Unification
10.1 Basic definitions and results
10.2 Commutative functions
10.2.1 A unification algorithm
10.2.2 The decision problem
10.3 Associative and commutative functions
10.3.1 Terms as vectors and substitutions as matrices
10.3.2 AC1-unification
10.3.3 AC-unification
10.3.4 Homogeneous linear diophantine equations
10.4 Boolean rings
10.4.1 Polynomials
10.4.2 Unification
10.4.3 Löwenheim's formula
10.4.4 Why Löwenheim's formula works
10.4.5 Successive variable elimination
10.4.6 Complexity
10.4.7 Boolean unification in ML
10.5 Bibliographic notes
11 Extensions
11.1 Rewriting modulo equational theories
11.2 Ordered rewriting
11.3 Conditional identities and conditional rewriting
11.4 Higher-order rewrite systems
11.5 Reduction strategies
11.6 Narrowing
Appendix 2 A Bluffer's Guide to ML
A2.1 Types
A2.2 Expressions
A2.2.1 Basic values
A2.2.2 Compound expressions
A2.3 Function declarations
A2.4 Standard functions
A2.4.1 Booleans
A2.4.2 Lists
A2.5 Datatypes
A2.6 Exceptions