Term Rewriting Systems

Summary of the Course

Term rewriting is one of the core and well-established 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 pattern-matching 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 (Knuth-Bendix 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 high-order languages by establishing strong normalization for simply-typed 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 full-fledged Turing-complete model of computation (i.e. essentially an idealized programming language).

 

Literature