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

Revision: r1.2 - 07 Nov 2001 - 10:12 - ArieVanDeursen
Transform > TermRewriting
Copyright © 1999-2020 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback