Term re-writing what is it for?

As I said in the last lecture, a term rewriting system is the set of symbols
and rules for rewriting terms made up of those symbols. The aim, in general, is
to reduce terms to their minimal or "normal" form.

There's at least one term rewriting system that you all know *really well*

Algebra

In primary school, we learn the rewrite rules for algebra:

- If you take a subterm over the other side of the = , you change the sign

	x + y = 0
rewrites to 
	x = -y + 0


- Anything plus zero is zero

	x = -y + 0
rewrites to 
	x = -y


The point of algebraic rules is to reduce the equation to an "answer", or at
least to the smallest form possible. You can take something like:

	x * (y + 3)
        ----------      =  2x
             y


and reduce it to 
	y = 3


at any point there are usually several rules you could choose to apply.

The term rewriting systems that we create in CafeOBJ are similar. We want to be
able to reduce complex terms to simpler forms, so that we can answer specific
questions about them.

Example proof:
	associativity of list append
	by induction

induction is all about recursion
base case, recursive case


http://www.ldl.jaist.ac.jp/cafeobj/lib/list.mod