# 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. The objects of focus for this article include rewriting systems (also known as rewrite systems, rewrite engines 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 and declarative programming languages are based on term rewriting.

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

where the symbol (${\displaystyle \to }$) indicates that an expression matching the left hand side of the rule can be rewritten to one formed by the right hand side, and the symbols each denote a subexpression. In such a system, each rule is chosen so that the left side is equivalent to the right side, and consequently when the left side matches a subexpression, performing a rewrite of that subexpression from left to right maintains logical consistency and value of the entire expression.

In linguistics, rewrite rules, also called phrase structure rules, are used in some systems of generative grammar, as a means of generating the grammatically correct sentences of a language. Such a rule typically takes the form A → X, 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. For example, the rule S → NP VP means that a sentence can consist of a noun phrase followed by a verb phrase; further rules will specify what sub-constituents a noun phrase and a verb phrase can consist of, and so on.

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, (abbreviated ARS), although more recently authors use abstract rewriting system as well. (The preference for the word "reduction" here instead of "rewriting" constitutes a departure from the uniform use of "rewriting" in the names of systems that are particularizations of ARS. Because the word "reduction" does not appear in the names of more specialized systems, in older texts reduction system is a synonym for ARS).

## Related Topics

Warning: DOMDocument::loadHTML(): Tag math invalid in Entity, line: 1 in /home/ashver/webapps/infospaze/index.php on line 389

Warning: DOMDocument::loadHTML(): Tag semantics invalid in Entity, line: 1 in /home/ashver/webapps/infospaze/index.php on line 389

Warning: DOMDocument::loadHTML(): Tag mrow invalid in Entity, line: 1 in /home/ashver/webapps/infospaze/index.php on line 389

Warning: DOMDocument::loadHTML(): Tag mstyle invalid in Entity, line: 1 in /home/ashver/webapps/infospaze/index.php on line 389

Warning: DOMDocument::loadHTML(): Tag mo invalid in Entity, line: 1 in /home/ashver/webapps/infospaze/index.php on line 389

Warning: DOMDocument::loadHTML(): Tag annotation invalid in Entity, line: 1 in /home/ashver/webapps/infospaze/index.php on line 389