Rewriting

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 their 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, or more than one rule could be applicable. Rewriting systems then do not provide an algorithm for changing one term to another, but a set of possible rule applications. When combined with an appropriate algorithm, however, rewrite systems can be viewed as computer programs, and several declarative programming languages are based on term rewriting.

Examples

Arithmetic

Consider the rules of regular arithmetic. We can think of these rules as forming a rewriting system, with rules including:: $mathrm\{plus\}(a,\; b)\; ightarrow\; a\; +\; b$: $mathrm\{times\}(a,\; b)\; ightarrow\; a\; imes\; b$where "a"+"b" denotes the sum of "a" and "b", and "a" × "b" denotes the product of "a" and "b".

Suppose we are given the expression: $mathrm\{times\}(mathrm\{plus\}(11,9),\; mathrm\{plus\}(2,4))$We can rewrite this expression in two ways, simplifying either the first bracket or the second. Simplifying the first bracket, we have: $mathrm\{times\}(20,\; mathrm\{plus\}(2,\; 4))\; =\; mathrm\{times\}(20,\; 6)\; =\; 120$Simplifying the second gives: $mathrm\{times\}(mathrm\{plus\}(11,9),\; 6)\; =\; mathrm\{times\}(20,\; 6)\; =\; 120.$

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".

Logic

In logic, the procedure for determining the conjunctive normal form (CNF) of a formula can be conveniently written as a rewriting system. The rules of such a system would be:

:$eg\; eg\; A\; o\; A$ (double negative elimination):$eg(A\; land\; B)\; o\; eg\; A\; lor\; eg\; B$ (De Morgan's laws):$eg(A\; lor\; B)\; o\; eg\; A\; land\; eg\; B$ :$(A\; land\; B)\; lor\; C\; o\; (A\; lor\; C)\; land\; (B\; lor\; C)$ (Distributivity):$A\; lor\; (B\; land\; C)\; o\; (A\; lor\; B)\; land\; (A\; lor\; C)$,where the arrow ($o$) indicates that the left side of the rule can be rewritten to the right side (so it does not denote logical implication).

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 the set of terms "T" = {"a", "b", "c"} and the rules are "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, that "c" is, in a sense, a "simplest" term in the system, since nothing can be applied to "c" to transform it any further.

Philosophy

Rewriting systems can be seen as programs that infer end-effects from a list of cause-effect relationships. In this way, rewriting systems can be considered to be automated Causality provers.

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.

ee also

* Causality
* Confluence
* Critical pair
* Graph rewriting
* Just-in-time compilation
* Knuth-Bendix completion algorithm
* Lambda calculus
* Lindenmayer system
* Mathematica
* Maude system
* MU puzzle
* Q (programming language)
* Reduction strategy
* Reduction system
* Regulated rewriting
* Rho calculus
* String rewriting
* Tom (pattern matching language)

References

* Nachum Dershowitz and Jean-Pierre Jouannaud. [http://citeseer.ist.psu.edu/dershowitz90rewrite.html 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, 2003
* "Term Rewriting and All That", Franz Baader and Tobias Nipkow, Cambridge University Press, 1998