Term Rewriting

Term rewriting is the process of simplifying symbolic expressions (terms) by means of a RewriteSystem^?, i.e., a set of RewriteRules.

An example rewrite system is the following:

         0 + x -> x
      s(x) + y -> s(x + y)
   (x + y) + z -> x + (y + z)

The NormalForm^? of the term ((s(s(a)) + s(b)) + c) under these rewrite rules is the term s(s(s(a + (b + c)))).

The order in which rules are applied to the term is determined by the RewritingStrategy.

See also

• AlgebraicSpecification^?
• TermRewritingImplementation
• RewritingHomePage