en | de

Term Rewriting

bachelor program

VU3  WS 2022/2023  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
1 03.10 examples, terms, matching algorithm
2 10.10 abstract rewrite systems, Newman's lemma
3 17.10 multiset orders, equational reasoning, algebras
4 24.10 term rewrite systems, undecidability
5 31.10 congruence closure, termination, polynomial interpretations
6 07.11 LPO, unification, critical pairs
7 14.11 completion, first-order theory of rewriting
8 21.11 KBO, normalization equivalence, abstract completion
9 28.11 confluence, orthogonality
10 05.12 strategies, normalization
11 12.12 strategy annotations, simple termination
12 09.01 dependency pairs, Z property
13 16.01 matrix interpretations, derivational complexity
14 23.01 completion modulo AC, test practice
15 30.01 test

Literature

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