TERM REWRITING AND ALL THAT

Le Monde En Tique

Commandez cet ouvrage

Ouvrage 9780521779203 : TERM REWRITING AND ALL THAT

This is a unified and self-contained introduction 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 reference: it is the first time many of the results have been presented in book form.
Preface
Term rewriting is a branch of theoretical computer science which combines elements of logic, universal algebra, automated theorem proving and functional programming. Its foundation is equational logic. What distinguishes term rewriting from equational logic is that equations are used as directed replacement rules, i.e. the left-hand side can be replaced by the right-hand side, but not vice versa. This constitutes a Turing-complete computational model which is very close to functional programming. It has applications in algebra (e.g. Boolean algebra, group theory and ring theory), recursion theory (what is and is not computable with certain sets of rewrite rules), software engineering (reasoning about equationally defined data types such as numbers, lists, sets etc.), and programming languages (especially functional and logic programming). In general, term rewriting applies in any context where efficient methods for reasoning with equations axe required.
To date, most of the term rewriting literature has been published in specialist conference proceedings (especially Rewriting Techniques and Applications and Automated Deduction in Springer's LNCS series) and journals (e.g. Journal of Symbolic Computation and Journal of Automated Reasoning). In addition, several overview articles provide introductions into the field, and references to the relevant literature [141, 74, 204]. This is the first English book devoted to the theory and applications of term rewriting. It is ambitious in that it tries to serve two masters:
ùThe researcher, who needs a unified theory that covers, in detail and in a single volume, material that has previously only been collected in overview articles, and whose technical details are spread over the literature.
ùThe teacher or student, who needs a readable textbook in an area where there is hardly any literature for the non-specialist.
Our choice of material is fairly canonical: abstract reduction systems and universal algebra (the foundation), word problems (the motivation), unification (a central algorithm), termination, confluence and completion (the sine qua non of term rewriting). The inclusion of combination problems is also uncontroversial, except maybe for the rather technical topic of combining word problems. Two further topics show our own preferences and are not strictly core material: equational unification is included because of its significance for rewriting based theorem provers, Grobner bases because they form an essential link between term rewriting and computer algebra.
Prerequisites are minimal: readers who have taken introductory courses such as discrete mathematics, (linear) algebra, or theoretical computer science axe well equipped for this book. The basic notions of ordered sets are summarized in an appendix.
How to teach this book
The diagram below shows the dependencies between the different sections of the book.
Diagram not shown
An introductory undergraduate course should cover the trunk of the above tree. To give the students a more algorithmic understanding of completion, it is helpful also to introduce Huet's completion procedure (7.4) without formally justifying its correctness. The course should conclude with 11.2-11.6. A more advanced introduction at graduate level would also include 4.3-4.4, 4.8, 6.4, 7.2-7.4, 9.1-9.3, and (initial segments of) 10. For a mathematically oriented audience, 3.2-3.5 is mandatory and 8 contains an excellent application of rewriting methods in mathematics.
Chapter 2 on abstract reduction systems is the foundation that term rewriting rests on. Nevertheless we recommend not to teach this chapter en bloc but to interleave it with the rest of the book. Only Section 2.1 needs to be covered right at the start. The dependency of the remaining sections is as follows:
2.2-2.5 --- 5 ---2.7 --- 6.
This groups together the abstract and concrete treatments of termination (2.2-2.5 and 5) and confluence (2.7 and 6).
Chapter 5 on termination has a special status in the dependency diagram. It is not the case that all of Chapter 5 is a prerequisite for the remainder of the book. In fact, almost the opposite is the case: one could read most of the remainder quite happily, except that one Would not be able to follow particular termination arguments. However, due to the overall importance of termination, we recommend that students should be exposed at least to 5.1-5.3 and possibly one of the simplification orders in 5.4. The general theory of simplification orders should be reserved for a graduate-level course.
A final word of warning. A book also aimed at researchers is written with a higher level of formality than a pure textbook. In places, the formal rigour of the book needs to be adjusted to the requirements of the classroom.
The role Of ML
Most of the theory in this book is constructive. Either we explicitly deal with particular algorithms, e.g. unification, or the proof of some theorem is essentially an algorithm, e.g. a decision procedure. We find that many computer science students take more easily to logical formalisms once they understand how to represent formulae as data structures and how to transform them. Therefore we have tried to accompany every major algorithm in this book by an implementation. As an implementation language we have chosen ML: functional languages are closest to our algorithms and ML is one of its best-known representatives. For those readers not familiar with ML, a concise summary of the core of the language is provided as an appendix.
It should be emphasized that our ML programs are strictly added value: they reside in separate sections and are not required for an understanding of the main text (although we believe that their study enhances this understanding).
We should also point out that the programs are intentionally unoptimized.
Table of Contents
Preface
1. Motivating examples
2. Abstract reduction systems
3. Universal algebra
4. Equational problems
5. Termination
6. Confluence
7. Completion
8. Grobner bases and Buchberger's algorithm
9. Combination problems
10. Equational unification
11. Extensions
Appendix 1. Ordered sets
Appendix 2. A bluffer's guide to ML
Bibliography
Index.

Auteur : BAADER
Editeur : CAMBRIDGE UNIVERSITY PRESS
Nombre de pages : 301
Date de publication : 08 1999

Commandez cet ouvrage