# Dictionary Definition

rewriting n : editing that involves writing
something again [syn: revising]

# User Contributed Dictionary

## English

### Noun

- logic computer science a wide range of potentially non-deterministic methods of replacing subterms of a formula with other terms

### Verb

rewriting- present participle of rewrite

# Extensive Definition

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(a, b) \rightarrow a + b
- \mathrm(a, b) \rightarrow a \times b

Suppose we are given the expression

- \mathrm(\mathrm(11,9), \mathrm(2,4))

- \mathrm(20, \mathrm(2, 4)) = \mathrm(20, 6) = 120

- \mathrm(\mathrm(11,9), 6) = \mathrm(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:- \neg\neg A \to A (double negative elimination)
- \neg(A \land B) \to \neg A \lor \neg B (De Morgan's laws)
- \neg(A \lor B) \to \neg A \land\neg B
- (A \land B) \lor C \to (A \lor C) \land (B \lor C) (Distributivity)
- A \lor (B \land C) \to (A \lor B) \land (A \lor C),

### 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 = 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.

## See 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. 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

rewriting in German: Termersetzungssystem

rewriting in French: Réécriture
(informatique)

rewriting in Italian: Riscrittura

rewriting in Japanese: 項書き換え

rewriting in Turkish: Terimi yeniden
yazma