Rewriting
|
|
Rewriting in mathematics, computer science and logic covers a wide range of non-deterministic methods of replacing subterms of a formula with another terms. This is a powerful general method for dealing with equation. A rewrite system is a set of equations over a given set of terms called rules that characterize a system of computation.
The non-deterministic nature of a rewriting system indicates that it is not an algorithm for changing one term to another, but a set of possible substitutions.
Rewrite systems provide a convenient method of automating theorem proving. If we begin with a set of equational hypotheses, then these may be used to formulate a set of rewrite rules. An example from school algebra goes under the heading collect like terms in an equation. There will usually be several ways to proceed, in collecting up and simplifying an equation
- P(x) = Q(x)
in which P and Q are polynomials. After some application of the conventional rules of algebra we may end with an equation
- R(x) = 0.
This is something like a normal form, though we may well have different signs (at least) for R found by different routes. If we insist that R is monic there is actually a normal form (as is usually tacitly assumed) in which R(x) is written in terms of decreasing powers of x. The feature of this rewriting system that has some general application is that some unique result or normal form is obtainable; and naturally any serious computer algebra system will have to perform this simplification automatically.