[ [[ChapterProgramRepresentation][Previous]] 
| [[Part III][Up]]
| [[ChapterProgramTransformationWithConcreteObjectSyntax][Next]]
]

------+++ Introduction

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

	* [[http://www.cs.uu.nl/~visser/book/Chapter-5.pdf][Chapter-5.pdf]]
	* [[http://www.cs.uu.nl/~visser/book/Chapter-5.ps][Chapter-5.ps]]