Rewriting
In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms.
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.
Term rewriting systems can be employed to compute arithmetic operations on natural numbers.
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: where the rule numbers are given above the rewrites-to arrow.
In linguistics, phrase structure rules, also called rewrite rules, are used in some systems of generative grammar,[8] as a means of generating the grammatically correct sentences of a language.
, where A is a syntactic category label, such as noun phrase or sentence, and X is a sequence of such labels or morphemes, expressing the fact that A can be replaced by X in generating the constituent structure of a sentence.
A confluent and terminating ARS is called convergent or canonical.
A string rewriting system (SRS), also known as semi-Thue system, exploits the free monoid structure of the strings (words) over an alphabet to extend a rewriting relation,
, to all strings in the alphabet that contain left- and respectively right-hand sides of some rules as substrings.
is a binary relation between some (fixed) strings in the alphabet, called the set of rewrite rules.
, is a congruence, meaning it is an equivalence relation (by definition) and it is also compatible with string concatenation.
The notion of a semi-Thue system essentially coincides with the presentation of a monoid.
Thus semi-Thue systems constitute a natural framework for solving the word problem for monoids and groups.
The word problem for a semi-Thue system is undecidable in general; this result is sometimes known as the Post–Markov theorem.
In contrast to string rewriting systems, whose objects are sequences of symbols, the objects of a term rewriting system form a term algebra.
As a formalism, term rewriting systems have the full power of Turing machines, that is, every computable function can be defined by a term rewriting system.
One such example is Pure, a functional programming language for mathematical applications.
[14] [15] A rewrite rule is a pair of terms, commonly written as
to the term l. The subterm matching the left hand side of the rule is called a redex or reducible expression.
of rules can be viewed as an abstract rewriting system as defined above, with terms as its objects and
is a rewrite rule, commonly used to establish a normal form with respect to the associativity of
[note 2] Applying that substitution to the rule's right-hand side yields the term
Alternately, the rule could have been applied to the denominator of the original term, yielding
Termination even of a system consisting of one rule with a linear left-hand side is undecidable.
This result disproves a conjecture of Dershowitz,[23] who claimed that the union of two terminating term rewrite systems
Higher-order rewriting systems are a generalization of first-order term rewriting systems to lambda terms, allowing higher order functions and bound variables.
