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. When combined with an appropriate algorithm, however, rewrite systems can be viewed as computer programs, and several (experimental) 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:

$\backslash mathrm\{plus\}(a,\; b)\; \backslash rightarrow\; a\; +\; b$

$\backslash mathrm\{times\}(a,\; b)\; \backslash rightarrow\; a\; \backslash times\; b$

where a+b denotes the sum of a and b, and a × b denotes the product of a and b.

In the following, we denote plus(a, b) by a+b and likewise for times(a, b). Suppose we are given the expression

$(11\; +\; 9)\; \backslash times\; (2\; +\; 4)$

We can rewrite this expression in two ways -- either simplifying the first bracket, or the second. Simplifying the first bracket, we have

$20\; \backslash times\; (2\; +\; 4)\; =\; 20\; \backslash times\; 6\; =\; 120$

Simplifying the second, gives

$(11\; +\; 9)\; \backslash times\; 6\; =\; 20\; \backslash times\; 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:

$\backslash neg\backslash neg\; A\; \backslash to\; A$ (double negative elimination)

$\backslash neg(A\; \backslash land\; B)\; \backslash to\; \backslash neg\; A\; \backslash lor\; \backslash neg\; B$ (distributivity)

$\backslash neg(A\; \backslash lor\; B)\; \backslash to\; \backslash neg\; A\; \backslash land\backslash neg\; B$

$\backslash neg\; (A\; \backslash land\; B)\; \backslash lor\; C\; \backslash to\; (A\; \backslash lor\; C)\; \backslash land\; (B\; \backslash lor\; C)$ (De Morgan's laws)

$\backslash neg\; A\; \backslash lor\; (B\; \backslash land\; C)\; \backslash to\; (A\; \backslash lor\; B)\; \backslash land\; (A\; \backslash lor\; C)$,

where the arrow ($\backslash to$) 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.

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

---

• Critical pair
• Confluence
• Graph rewriting
• Knuth-Bendix completion algorithm
• Lambda calculus
• Lindenmayer system
• MU puzzle
• Q programming language
• Rho calculus
• String rewriting

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, 2003

Formal languages | Formal methods | Logic in computer science | Mathematical logic | Theory of computation

Réécriture (informatique) | Terimi yeniden yazma