Introductory / advanced course


Faculty of Mathematics and Computer Science, Free University of Amsterdam

Both weeks and
Course description

I Introductory Course (first week):

This course is meant to give an introduction to the theory of first order rewriting. We will treat the following basic topics: unification, termination and confluence. Two basic techniques for proving termination will be covered: monotone algebras and path orderings (Kruskal's Tree Theorem). Concerning confluence, we will focus on critical pair analysis and orthogonality. Finally, the relation with equational logic will be discussed (Knuth-Bendix completion and narrowing).

The level and the gist of the course is that of the standard text by Klop, ``Term Rewriting Systems" in the Handbook of Logic in Computer Science (Vol.2). It will be based on a forthcoming book on term rewriting systems by the same author (et al.).

Emphasis is put on the main techniques and results in term rewriting, which implies that only parts will be highlighted of the other standard text by N. Dershowitz and J.-P. Jouannaud: ``Rewrite Systems", in the Handbook of Theoretical Computer Science (Vol. B).

II Advanced Course (2. week):

In the advanced part of the course four types of rewrite systems are presented: abstract rewriting systems (ARSs), first-order term rewriting systems (TRS) and lambda calculus (\), infinitary rewrite systems (oo), and higher-order rewrite systems (HRS). It will be shown how prooftechniques from the well-established theory of TRSs and \ can be lifted to the more recently introduced oo and HRSs. Infinitary rewriting allows to study properties of infinite computations (e.g. lazy rewriting in functional programming), but is also employed as a semantics for graph rewriting. HRSs constitute a high-level specification mechanism and their study can be seen as an investigation of the meta-theory of systems such as lambda Prolog (programming language), Isabelle (Theorem Prover) and Mathematica.

The course starts by introducing abstract rewriting systems, anda powerful confluence theorem (decreasing diagrams thm) for them.Next, the theory of orthogonality (independence of rewrite steps) will be introduced by means of an abstract rewrite system for braids.Typical topics in the theory of orthogonality are: confluence, permutation/shift equivalence, and optimality. Subsequently, the classes of TRSs, \, oo, and HRSs will be motivated, introduced and the theory of orthogonality will be developed for each of them.


I Introductory Course (first week):

Assumed knowledge: basic discrete mathematics (e.g., properties of relations, proofs by induction).

II Advanced Course (2. week):

Assumed knowledge: term rewriting (as e.g. provided by Part I of the course); and basic knowledge the lambda calculus.


There's no book or handbook chapter covering the whole area, but

  • Combinatory Reduction Systems, J.W. Klop, PhD thesis, Utrecht University 1980

comes close to the spirit of the course. Other literature of interest:

  • HRS
    • Higher-Order Critical Pairs, T. Nipkow, LICS 1991.
    • Confluence and Normalisation for Higher-Order Rewriting, F. van Raamsdonk, PhD thesis, VU. Amsterdam 1997.
  • abstract
    • Description Abstraite des Systemes de Reecriture, P.A. Mellies, PhD thesis, Universite Paris 7, 1997.
  • oo
    • Infinitary lambda calculus, TCS 175, 1997. J.R. Kennaway, J.W. Klop, M.R. Sleep, F.J. de Vries,
  • abstract and HRS
    • Confluence for Abstract and Higher-Order Rewriting, V. van Oostrom, PhD thesis, VU, Amsterdam 1994.
  • and backpointers.