Chapter Term Rewriting

Strategies for Program Transformation
[ Previous | Up | Next ]


In the previous chapter we saw how terms provide a structured representation for programs derived from a formal definition of the syntax of the programming language. Transforming programs then requires tranformation of terms. There are various ways such transformations could be defined. In this chapter we consider the paradigm of term rewriting for specifying program transformations. In term rewriting a term is transformed by repeated application of rewrite rules. In the first section we first examine the equivalence of expressions and equational reasoning. Then we will formally define term patterns, substitution, term pattern matching, rewrite rules, and normalization with respect to a set of rewrite rules.