A term rewrite system is a collection of
directed
equations that change an equation into a
standard
form.
The TRS for a very simple algebraic structure,
a monoid, might look like this:
(x*y)*z -> x*(y*z)
1*x -> x
x*1 ->
Here * does not necessarily mean multiplication. It
could mean addition or some other odd operator,
just as long as the operator follows the rules set
down by a monoid.
By applying these three rules on any equation defined
over this monoid, an equation can be both simplified
and changed into a form that allows its structure and
order to be compared to another equation for use in
a symbolic computation system.
Example: the equation ((x*1)*(1*y))*(z*1)
can be changed around like so:
((x*1)*(1*y))*(z*1) ->
(x*(1*y))*(z*1) ->
(x*y*(z*1) ->
(x*y)*z ->
x*(y*z)
A set of term rewrite rules is said to be terminating
if any sequence of term rewrites results in an equation
that cannot be changed after a finite number of steps.
If the final equation produced is unique, then that
equation is called the normal form of any equation in
the term rewrite steps that precede it.
Some of this information comes from "Logic for Mathematics and Computer Science" by Stanley N. Burris.