Rewriting

In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. Such methods may be achieved by rewriting systems (also known as rewrite systems, rewrite engines,[1][2] or reduction systems). In their most basic form, they consist of a set of objects, plus relations on how to transform those objects.

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 theorem provers[3] and declarative programming languages are based on term rewriting.[4][5]

In logic, the procedure for obtaining the conjunctive normal form (CNF) of a formula can be implemented as a rewriting system.[6] The rules of an example of such a system would be:

Term rewriting systems can be employed to compute arithmetic operations on natural numbers. To this end, each such number has to be encoded as a term. The simplest encoding is the one used in the Peano axioms, based on the constant 0 (zero) and the successor function S. for example, the numbers 0, 1, 2, and 3 are represented by the terms 0, S(0), S(S(0)), and S(S(S(0))), respectively. The following term rewriting system can then be used to compute sum and product of given natural numbers.[7]

For example, the computation of 2+2 to result in 4 can be duplicated by term rewriting as follows:

From the above examples, it is clear that we can think of rewriting systems in an abstract manner. We need to specify a set of objects and the rules that can be applied to transform them. The most general (unidimensional) setting of this notion is called an abstract reduction system[9] or abstract rewriting system (abbreviated ARS).[10] An ARS is simply a set A of objects, together with a binary relation → on A called the reduction relation, rewrite relation[11] or just reduction.[9]

Important theorems for abstract rewriting systems are that an ARS is confluent iff it has the Church-Rosser property, Newman's lemma which states that a terminating ARS is confluent if and only if it is locally confluent, and that the word problem for an ARS is undecidable in general.

The word problem for a semi-Thue system is undecidable in general; this result is sometimes known as the Post-Markov theorem.[12]

In contrast to string rewriting systems, whose objects are sequences of symbols, the objects of a term rewriting system form a term algebra. A term can be visualized as a tree of symbols, the set of admitted symbols being fixed by a given signature.

Termination issues of rewrite systems in general are handled in . For term rewriting systems in particular, the following additional subtleties are to be considered.

Termination even of a system consisting of one rule with a linear left-hand side is undecidable.[15][16] Termination is also undecidable for systems using only unary function symbols; however, it is decidable for finite ground systems.[17]

The following term rewrite system is normalizing,[note 3] but not terminating,[note 4] and not confluent:[18]

The following two examples of terminating term rewrite systems are due to Toyama:[19]

See Rewrite order and Path ordering (term rewriting) for ordering relations used in termination proofs for term rewriting systems.

Higher-order rewriting systems are a generalization of first-order term rewriting systems to lambda terms, allowing higher order functions and bound variables[21]. Various results about first-order TRSs can be reformulated for HRSs as well.[22]

Graph rewrite systems are another generalization of term rewrite systems, operating on graphs instead of (ground-) terms / their corresponding tree representation.

Trace theory provides a means for discussing multiprocessing in more formal terms, such as via the trace monoid and the history monoid. Rewriting can be performed in trace systems as well.

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.[citation needed]