Rewriting

Rewriting in mathematics, computer science and logic covers a wide range of methods of transforming strings, written in some fixed alphabet, that are not deterministic but are governed by explicit rules. This is a powerful general method for dealing with equation. A rewrite system is a set of equations that characterize a system of computation. 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.

The non-deterministic nature of a rewriting system indicates that it is not an algorithm for changing one string to another, but a system of 'permissions'. 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.

Some of the more common types are:

• String rewriting – see string rewriting system
• Term rewriting – see Confluence
• Graph rewriting