en | de

Term Rewriting

bachelor program

VU3  WS 2023/2024  703141

Content

The course provides an introduction to term rewriting. Term rewriting is a general model of computation which has been successfully applied in many areas of computer science. Here one can think of the analysis and implementation of algebraic specifications of abstract data types, the foundations of functional (logic) programming, automated theorem proving, and code optimization in compilers, to name just a few.

Schedule

week date topics slides solutions material
1 02.10 examples, terms, matching algorithm lecture notes
2 09.10 abstract rewrite systems, Newman's lemma link
3 16.10 multiset orders, equational reasoning, algebras
4 23.10 term rewrite systems, undecidability
5 30.10 congruence closure, termination, polynomial interpretations link
6 06.11 LPO, unification, critical pairs
7 13.11 completion, first-order theory of rewriting
8 20.11 KBO, normalization equivalence, abstract completion link
9 27.11 confluence, orthogonality link
10 04.12 strategies, normalization
11 11.12 strategy annotations, simple termination
12 08.01 dependency pairs, Z property
13 15.01 matrix interpretations, dependency pairs
14 22.01 derivational complexity, completion modulo AC, test practice
15 29.01 test (solution)

Literature

The course material and slides will be made available online. The same holds for solutions to selected exercises.