VINCENT VAN OOSTROM and YDE VENEMA Faculty of Mathematics and Computer Science, Free University of
Amsterdam 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 comes close to the spirit of the course. Other literature of interest:
Computation
TERM REWRITING SYSTEMS (I & II)
Introductory / advanced course
Both weeks
oostrom@cs.vu.nl and yde@cs.vu.nl
Course description
Prerequisites
Literature