After successful completion of the course, students are able to understand the basics of term rewrite systems as well as selected advanced topics. The foundations at least amout to (i) (i) Abstract Rewrite Systems; (ii) (First-Order) Term Rewrite Systems; (iii) Completion, Complexity, Confluence and Termination. Selected Topics will be clarified before commencement of the course.
The following topics are discussed:
Foundations.
(i) Abstract Rewrite Systems: definitions, properties, Newman's Lemma, commutation, strategies; (ii) (First-Order) Term Rewrite Systems: definitions, properties, equational reasoning, word problem; (iii) Completion, Complexity, Confluence and Termination: critical pair lemma, Gröbner basis, derivational complexity, connection to subrecursive hierarchies, (beyond) orthogonality, decreasing diagrams, polynomial and matrix interpretations, dependency pairs.
Advanced Topics (one or two of these, depending on interest).
(i) Mathematical Foundations; (ii) Automated Resource Analysis; (iii) Probabilistic Term Rewriting; (iv) Tree Automata; (v) Strategies.
The course is taught in English and will be held (mainly) online with a discussion phase on July 13-17. See the organisational details on the TUWEL page. At the moment it is unclear, whether regulations allow to hold the discussion phase in attendance. Supporting material, slides, recordings, as well exercises have been made available on TUWEL. During the discussion the feedback to selected exercises, special interest will be provided.
The course is partly based on the following lecture notes:
- Term Rewrite Systems, Aart Middeldorp, lecture notes, University of Innsbruck.
Additional material can also be found on the course homepage.