REWRITE SYSTEMS MINI-COURSE

Ben-Gurion University
April 1997

N. Dershowitz

DESCRIPTION

Equational reasoning is important in artificial intelligence, automated deduction, symbolic algebra, program verification, and high-level programming languages. Reasoning with equations includes deriving consequences of given equations and finding values for variables that satisfy a given equation.

Rewriting is a very powerful method for dealing with equations. It is a topic of much recent theoretical and applied research in Europe, Japan, and the U.S. Rewrite rules, that is directed equations, are used to replace equals by equals, but only in a direction that results in a simpler expression. The theory of rewriting centers around the notion of "normal forms", expressions that cannot be rewritten any further. When equal terms always have the same normal form, the system is said to be "canonical" or "complete".

The course will be self-contained. There are no prerequisites.

There will be two one-week homework assignments and no exam.

COURSE OUTLINE

  • Introduction: equational reasoning, rewrite systems, term orderings
  • Rewriting: normal forms, existence, uniqueness, deciding equality
  • Confluence: Church-Rosser property, Newman's Lemma, local confluence, critical pairs
  • Orthogonality: strong confluence, Parallel Moves Lemma, outermost computations
  • Termination: undecidability, interpretations, Kruskal's Tree Theorem, recursive path orderings
  • Completion: proof orderings, Knuth-Bendix procedure, ordered completion
  • Theorem proving: equational reasoning, induction, first-order
  • The future: extensions, open problems

    LECTURE NOTES

    HOMEWORK

  • First
  • Second

    OTHER REFERENCES (Optional)

    A Taste of Rewriting

    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.)

    Rewrite Systems

    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.)

    Term Rewriting Systems

    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.)

    Equational Inference, Canonical Proofs, and Proof Orderings

    L. Bachmair and N. Dershowitz. J. of the ACM 41 (2) 236-276 (Feb. 1994)

    This paper describes the application of proof orderings--a technique for reasoning about inference systems--to various rewrite-based theorem-proving methods, including ordered completion and a proof by consistency procedure for proving inductive theorems. (The on-line version is a pre-publication technical report.)