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, as well as some selected topics of advanced material.
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 online with a discussion phase on June 28 - July 9. During the discussion feedback to selected exercises, special interest will be provided. See the organisational details on the TUWEL page. Supporting material, slides, recordings, as well exercises will be made available on TUWEL before June 14. Please register timely for the course, so that the interest into the course can be properly anticipated.
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.
