- 0. Introduction
-
We start the book by presenting some basic examples of
rewriting, in order to set the stage.
- 1. Abstract reduction systems
-
Many aspects of rewriting can be
studied independently of the nature of the objects that are rewritten.
This abstract approach is expressed by the title of this chapter.
We formally introduce the basic notions of abstract reduction systems
such as reduction, conversion, confluence and normalization. We study
some variations and interrelations and collect several extensions in
the form of exercises at the end of the chapter.
Authors: M.A. Bezem and J.W. Klop
- 2. First-order term rewriting systems
-
This chapter introduces first-order term rewriting systems
and
basic notions such as terms, occurrences, contexts, substitutions
and matching, and the concept of a rewrite rule.
Only simple examples of term rewriting sytems are given,
just to illustrate the definitions.
A preliminary discussion of equational reasoning and
its semantics is given. As an application of rewriting, it
is explained how complete term rewriting systems can sometimes be used
to solve a word problem.
The chapter concludes with an analysis of overlap between reduction rules,
leading to the notion of a critical pair and to the Critical Pair Lemma.
Authors: J.W. Klop and R.C. de Vrijer
-
3. Examples of TRSs and special rewriting formats
-
In this chapter some more extended examples of term rewriting sytems are
presented.
Typical examples are TRSs containing numerals, i.e. representations of
the natural numbers. We introduce the concept of stream,
illustrating that it is not always only the
normal form of a term that counts, but also its infinitary behaviour.
As another illustration of TRSs with numerals,
a historical note about Herbrand-Gödel computability is
included, which turns out to be an application avant la lettre
of term rewriting techniques, giving one of the earliest characterizations
of computable functions.
The paradigm example of a TRS, combinatory logic, gets an extensive
treatment.
As modifications of the first-order format
string rewriting and many-sorted rewriting are briefly
dicussed. The chapter concludes with a section about conditional
rewriting.
Authors: J.W. Klop and R.C. de Vrijer
- 4. Orthogonality
- This chapter treats the basic theory of orthogonal
(first-order) term rewriting systems.
After some examples of orthogonal and
weakly orthogonal TRSs,
we prove confluence for orthogonal TRSs in several ways.
Key concepts in the various confluence proofs are:
descendant and residual,
parallel move,
labelling,
underlining,
complete development and finiteness of developments,
tiling with elementary diagrams,
multi-step,
inductive proof.
In the section about non-erasing reductions
the theorems of Church and O'Donnell are proved.
Next, a brief introduction to reduction strategies is given,
with definitions of some important strategies and several notions of fairness;
an extensive treatment can be found in
Chapter 9.
The chapter concludes with some extensions.
The confluence proof using tiling for the completion of reduction diagrams is
extended
to the case of weakly orthogonal TRSs,
and then to (weakly) orthogonal
CTRSs.
Authors:
J.W. Klop, V. van Oostrom and R.C. de Vrijer
- 5. Properties of rewriting: decidability and modularity
-
This chapter has two main topics, each one presenting a part
of the basic theory of first-order term tewriting systems.
In the first sections the issue of decidability of
properties
of rewriting, such as confluence and
termination is addressed. Special attention is given to CL.
There are also sections on the decidability of being a normal
form in CTRSs and on the decidability of WN for recursive
program schemes.
Then the focus shifts to the question
whether, and under what conditions, properties such as
confluence and termination are preserved when
term rewriting systems with these
properties are combined. This subject is called modularity.
Authors:
J.W. Klop and R.C. de Vrijer
- 6. Termination
-
This chapter gives an overview of techniques
for proving termination of first-order term rewriting systems. Three
kinds of techniques are distinguished: semantical methods, syntactical
methods and transformational methods. Semantical methods are based on
finding a suitable interpretation. They are suitable for all terminating
systems but are hard to automate. Syntactical methods like the recursive
path order can be automated in a straightforward manner but only apply
for a restricted class of term rewriting systems. Therefore a number
of transformational methods has been developed by which term rewriting
systems outside this class can be transformed to systems inside this class
in such a way that termination of the original systems can be concluded.
Author: H. Zantema
- 7. Completion of equational specifications
-
This chapter examines rewriting techniques as tools
for the validity problem of equational specifications.
The first two sections develop the basic theory of
equational deduction and initial algebra
semantics. After a short third section which discusses
a conditional version of equational deduction,
we embark on the study of completion procedures
in practical and abstract settings. In the two
remaining sections we discuss proofs by consistency
and E-unification.
Author: I. Bethke
- 8. Equivalence of reductions
-
This chapter presents an advanced treatment of orthogonality
in first-order term rewriting.
The focus will be on orthogonality of rewrite steps
rather than on orthogonality of rewriting systems.
That is, the framework applies not just to orthogonal
term rewriting systems, where steps are always orthogonal to one another,
but to all left-linear term rewriting systems.
This includes systems with critical pairs such as
the lambda-sigma calculus or weakly orthogonal term rewriting systems.
Central to the chapter is the notion of equivalence of reductions.
This notion will be captured from several directions.
We present five equivalent characterizations:
permutation equivalence, labelling equivalence,
standardization equivalence, extraction equivalence,
and projection equivalence.
We carry out in-depth investigations of the
techniques of labelling, standardization, tracing, and projection.
For instance, several well-known labelling methods are presented,
such as Lévy labels, Hyland-Wadsworth labels, and
Boudol-Khasidashvili labels.
The investigations are all based on the
technical tool of proof terms for Meseguer's rewriting logic.
A proof term codifies a proof that there is a reduction
from one term to another, as a single term,
comparable to the way a typed lambda term
codifies a natural deduction proof.
The scope of the concepts and methods introduced
extends beyond first-order term rewriting.
This is illustrated in the final section of this chapter,
where the notion of projection equivalence is applied
to the example of braids and their topological equivalence.
Authors:
V. van Oostrom and R.C. de Vrijer
- 9. Strategies
-
In this chapter we refine the results in
Chapter 4 on strategies,
using the notions and methods established in
Chapter 8.
Most of our results will pertain to (weakly)
orthogonal term rewriting systems.
After placing the notion of strategy in an abstract context,
we resume and extend the study of needed and
fair reductions introduced in Chapter 8 and
Chapter 4.
We then give a treatment of optimal strategies and
their dual, pessimal
(from Latin pessimus, worst)
strategies.
Unfortunately, computable optimal strategies
do not exist in general.
To remedy this problem, we show that a simple optimal
strategy does exist for family rewriting.
Family rewriting is an extension of ordinary
rewriting, where instead of single redexes whole
families of redexes, i.e. sets of redexes
having the same `creation history', are contracted in one go.
We show that family rewriting can be efficiently
implemented by means of graph rewriting.
Finally, we treat computable history free
one-step strategies.
Authors:
V. van Oostrom and R.C. de Vrijer
- 10. Lambda calculus
-
In this chapter, we present the paradigm higher-order rewriting
system - lambda calculus. We thoroughly work through
the fundamentals, discussing such topics as confluence,
finiteness of developments, parallel moves,
standardization and normalization, and definability.
We explore the ramifications of extensions of the basic theory
and study their confluence properties. We round off the chapter
with a short discussion of a typed version of the calculus
which exhibits a rather different character as compared
with the untyped version.
Author: I. Bethke
- 11. Higher-order rewriting
-
This chapter is concerned with term rewriting with bound variables.
To start with, the syntax of higher-order rewriting systems
(HRSs)
is presented.
Here rewriting is defined modulo the relation of
beta-eta conversion of simply typed lambda calculus.
Some of the rewriting theory developed for HRSs is discussed,
with a focus on the subjects of confluence and termination.
We further present another format of higher-order rewriting,
namely that of combinatory reduction systems (CRSs),
and study the relationship between HRSs and CRSs.
Author: F. van Raamsdonk
- 12. Infinitary rewriting
-
In this chapter we will give the basic definitions and properties
of infinite terms and infinite reduction sequences,
for both term rewriting systems and the lambda calculus.
We will then study confluence properties in orthogonal systems,
which turns out to be significantly more complicated than in the finitary case.
In general, these systems are only confluent
up to an identification of a certain class of terms.
The breakdown of confluence leads us to consider the concept of
a meaningless term, which further suggests a link with the
lambda calculus
concept of Böhm reduction
and to denotational semantics for TRSs.
Authors: J.R. Kennaway and F.J. de Vries
- 13. Term graph rewriting
-
This chapter presents an introduction to term graph rewriting.
In term graphs, subterms may be shared and there may be cycles.
We introduce and analyse the usual notion of a graph homomorphism and
the fundamental notion of bisimilarity.
We prove that orthogonal term graph rewriting systems are confluent. We also
give an equational presentation of term graphs. Next, we prove an adequacy
result for term graph rewriting with respect to term rewriting. Finally, we
present a complete proof system for terms with recursion, or mu-terms
Author: E. Barendsen
- 14. Advanced ARS theory
-
In this chapter we present advanced ARS theory on confluence,
and reduction modulo an equivalence relation.
We refer to the subsection on abstract commutation in
Chapter 6
for advanced results on termination in ARSs.
Authors: M.A. Bezem, J.W. Klop and V. van Oostrom
- 15. Rewriting-based languages and systems
-
Many systems are at least partly and indirectly based on term
rewriting. Examples are functional languages, computer algebra
systems, and theorem provers. We give a brief survey of these
systems, and provide a more in-depth comparison of the features of
systems that use term rewriting as their primary execution mechanism.
We give links to rewrite tools and projects as well as pointers to
notions and techniques covered in the preceding chapters.
Authors: J. Heering and P. Klint
- A. Mathematical background
-
This appendix provides a self-contained introduction to all basic
mathematical concepts and results used throughout the book.
We treat successively: relations, functions and orders;
ordinals and inductive definitions; metric topology; infinite
combinatorics; multisets.
Author: M.A. Bezem