3rd International School on Rewriting
3 – 8 July 2010, Drift 21, Utrecht, Netherlands
Introduction to Term Rewriting
Lecturers
Aart Middeldorp (University of Innsbruck, Austria)Femke van Raamsdonk (VU Amsterdam, The Netherlands)
Abstract
(basic track, 11 lecture sessions, 4 exercise sessions, exam, 3 ECTS)
This course provides an introduction to term rewriting, a Turing-complete computational model based on directed equations. We discuss the basic concepts and results. After an optional exam we conclude by providing an outlook to some recent research in term rewriting.
The following topics will be covered:
- introduction (motivation, equational reasoning, rewriting),
- abstract rewriting (basic notions, relationships, Newman's lemma),
- equational reasoning (terms, semantics, matching),
- term rewriting (soundness and completeness, Turing-completeness, combinatory logic),
- termination (polynomial interpretations, lexicographic path order, Knuth-Bendix order, dependency pairs)
- completion (unification, critical pairs, fairness, redundancy),
- confluence (orthogonality, developments, sufficient conditions),
- modularity (signature extension, disjoint combinations, constructor-sharing combinations),
- strategies (normalisation, sequential strategies, perpetual strategies),
- advanced topics (modern termination techniques, complexity, higher-order rewriting, conditional rewriting).
Material
- zip file with slides and exercises (updated 11-8-2010).
- external link to up-to-date course material - July 9th