Introduction to Term Rewriting: Techniques and Applications

Salvador Lucas

A first exposure to term rewriting
techniques, already in the school, is obtained from the arithmetic
calculus. For instance, the evaluation of an arithmetic expression like
3*(2+2) is performed through the application of rewriting techniques to
replace some expressions (e.g., 2+2) by equivalent but usually simpler
ones (like 4) until no further simplification is possible. A set of
equations is used to specify equivalent expressions (for instance, 2+2=4
and 3*4=12). Actually, equational reasoning is in the origin of term
rewriting as an independent discipline. Nowadays, term rewriting
techniques are used in many fields of computer science: software
engineering, programming languages, program verification, automated
deduction, and (computer) algebra, among others. In this course we aim
at providing an overview of the field, emphasizing the essential
features of term rewriting and term rewriting systems which are crucial
to understand rewriting-based programming languages, programs, and
computational systems. And, since they are often required in many
applications, we pay some specific attention to the analysis and
automatic proof of confluence and termination properties of term
rewriting systems.

Related slides:
1
2
3
4
5
6.