Foundations of Information Technologies

- FIT 2009 -

June 14-27, 2009, Novi Sad

 

Introduction to Term Rewriting: Techniques and Applications

 Salvador Lucas

                                                           Abstarct 

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.