Rewrite systems play an important role in various areas of computer science, such as automated deduction, artificial intelligence, program verification, and high-level programming languages. The course will cover some of the important topics related to the use of the theory of rewriting in (1) functional programming and (2) equational reasoning.
(1) Rewrite systems (or reduction systems) form a basic model of computation. Computation (= reduction) is performed according to rewrite rules, such as rules for addition and multiplication. A computation may end with a normal form (which is the value of the given expression) or diverge. Typical questions are existence of normal forms, confluence (which implies uniqueness of normal forms), termination (of all reduction paths), normalizing strategies (allowing to compute a normal form when it exists), etc.
The most well-known rewrite system is Church's Lambda-calculus. All (partial) recursive functions can be represented as Lambda-expressions, which makes the Lambda-calculus a paradigmatic functional programming language. All recent functional programming languages are based on typed Lambda-calculi.
(2) Reasoning with equations includes (a) deriving consequences of a set of equations and (b) finding solutions to a given set of equations.
(a) To decide whether an equation s=t is a consequence of a set of equations E, it is enough to construct a rewrite system R which is both terminating and confluent, and which `proves' the same equations as E. Then s=t is a consequence of E iff t and s reduce to the same normal form in R. To construct such a rewrite system R, one starts by orienting the equations in E, and then tries to resolve all divergent `critical pairs' in the obtained rewrite system. Termination proof techniques are of great importance in this process.
(b) Solving equations using unification will be addressed briefly.
The course will be self-contained. There are no strict prerequisites.
Barendregt H.P. Lambda Calculus. Its syntax and semantics. North Holland, 1984.
Barendregt H.P. Lambda Calculi with types. Chapter 2, V. 2 of the Handbook of Logic in Computer Science, Abramsky et al, eds, OUP, 1992.
N. Dershowitz. Functional Programming, Concurrency, Simulation and Automated Reasoning, Lecture Notes in Computer Science 693, 199-228 (1993)
A gentle introduction to the theory and applications of rewriting with equations. It discusses the existence and uniqueness of normal forms, the Knuth-Bendix completion procedure and its variations, as well as rewriting-based (functional and logic) programming and (equational, first-order, and inductive) theorem proving. An extensive bibliography is included. (The on-line version is better than the published one.)
N. Dershowitz and J.-P. Jouannaud. Chap. 6 of Handbook of Theoretical Computer Science B: Formal Methods and Semantics, J. van Leeuwen, ed., North-Holland, Amsterdam (1990) 243-320
This is a survey of the theory of rewriting. (The on-line version is imprecise.)
J. W. Klop. Chap. 1 in Handbook of Logic in Computer Science, vol. 2, S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, eds., Oxford University Press, Oxford (1992) 1-117.
This excellent survey stresses confluence properties, orthogonal systems, and completion. It includes exercises. (The on-line version does not have the valuable diagrams.)