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.
For other uses, see Rewriting (disambiguation).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]
Example cases[edit]
Logic[edit]
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:
Trace rewriting systems[edit]
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.