Rewriting
From Free net encyclopedia
In mathematics, computer science and logic, rewriting covers a wide range of potentially non-deterministic methods of replacing subterms of a formula with other terms. What is considered are rewrite systems (also rewriting systems, or term rewriting systems, though the latter term may imply a more specific system), which in its most basic form, consist of a set of terms, plus relations on how to transform these terms.
Term rewriting can be non-deterministic. One rule to rewrite a term could be applied in many different ways to that term. Rewriting systems then do not provide an algorithm for changing one term to another, but a set of possible substitutions that could be applied.
Contents |
Examples
Basic algebra
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.
Abstract rewriting systems
We can think of rewriting systems in an abstract manner also. We need to specify our set of terms and the rules that can be applied to transform them.
Suppose S = {a, b, c} and the rules a → b, b → a, a → c, and b → c hold. From these rules, observe that these rules can be applied to both a and b in any fashion to get the term c. Such a property is clearly an important one. Note also, since c is, in a sense, a "simplest" term in the system, since nothing can be applied to c to transform it any further.
Properties of rewriting systems
Observe that in both of the above rewriting systems, it is possible to get terms rewritten to a "simplest" term, where this term cannot be modified any further from the rules in the rewriting system. Terms which cannot be written any further are called normal forms. The potential existence or uniqueness of normal forms can be used to classify and describe certain rewriting systems. There are rewriting systems which do not have normal forms: a very simple one is the rewriting system on two terms a and b with a → b, b → a.
The property exhibited above where terms can be rewritten regardless of the choice of rewriting rule to obtain the same normal form is known as confluence. The property of confluence is linked with the property of having unique normal forms.
See also
- Confluence
- String rewriting
- Graph rewriting
- Lambda calculus
- Rho calculus
- Knuth-Bendix completion algorithm
- Lindenmayer system
References
- Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite Systems (1990). Chapter 6 of Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pp.243–320.
- Term Rewriting Systems, Terese, Cambridge Tracts in Theoretical Computer Science, 2003fr:Réécriture