Term Rewriting Systems
Summary of the Course
Term rewriting is one of the core and wellestablished subjects of theoretical computer science. The tools and methods of rewriting pervasively appear in various fields of computer science including formal languages, computability theory, computer algebra, programming and verification.
In nutshell, term rewriting deals with successive transformations of terms by patternmatching and replacement. This simple procedure leads to a rich theory dealing with termination, decidability, confluence of rewrite systems, derivation of rewrite systems from equational theories, combining rewrite systems, etc.
In this course, we study the basic concepts and tools of term rewriting. We study basic properties of rewriting systems such as termination, confluence and canonicity. We show how systems of equations can be converted into rewriting systems (KnuthBendix completion). We study various techniques of proving termination of rewriting (polynomial interpretation, simplification term orderings). We illustrate the use of methods of term rewriting for highorder languages by establishing strong normalization for simplytyped lambda calculus and clarify its connection to the (intuitionistic) logic via Gentzen’s cut elimination theorem.
Learning Goals

Learn to recognize and to formalize problems dealing with term transformations as rewriting systems.

Learn the techniques for checking and establishing properties of rewrite systems crucial for calculating normal forms (termination, confluence).

Understanding the connections of term rewriting to other areas of computer science, in particular, by establishing it as a fullfledged Turingcomplete model of computation (i.e. essentially an idealized programming language).
Literature

Baader, Franz; Nipkow, Tobias (1998). Term Rewriting and All That. Cambridge University Press.

Marc Bezem, Jan Willem Klop, Roel de Vrijer (“Terese”), Term rewriting systems, Cambridge University Press, 2003.