# Chapter Term Rewriting

Strategies for Program Transformation

### Abstract

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.

### Preprint