Katana VentraIP

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.

Critical pair (logic)

Compiler

Knuth–Bendix completion algorithm

specify rewriting that is done in parallel.

L-systems

in computer science

Referential transparency

Regulated rewriting

Interaction Nets

; Nipkow, Tobias (1999). Term rewriting and all that. Cambridge University Press. ISBN 978-0-521-77920-3. 316 pages.

Baader, Franz

Jan Willem Klop, Roel de Vrijer ("Terese"), Term Rewriting Systems ("TeReSe"), Cambridge University Press, 2003, ISBN 0-521-39115-6. This is the most recent comprehensive monograph. It uses however a fair deal of non-yet-standard notations and definitions. For instance, the Church–Rosser property is defined to be identical with confluence.

Marc Bezem

and Jean-Pierre Jouannaud "Rewrite Systems", Chapter 6 in Jan van Leeuwen (Ed.), Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics., Elsevier and MIT Press, 1990, ISBN 0-444-88074-7, pp. 243–320. The preprint of this chapter is freely available from the authors, but it is missing the figures.

Nachum Dershowitz

Nachum Dershowitz and . "Rewriting", Chapter 9 in John Alan Robinson and Andrei Voronkov (Eds.), Handbook of Automated Reasoning, Volume 1.

David Plaisted

et Derek Oppen, Equations and Rewrite Rules, A Survey (1980) Stanford Verification Group, Report N° 15 Computer Science Department Report N° STAN-CS-80-785

Gérard Huet

. "Term Rewriting Systems", Chapter 1 in Samson Abramsky, Dov M. Gabbay and Tom Maibaum (Eds.), Handbook of Logic in Computer Science, Volume 2: Background: Computational Structures.

Jan Willem Klop

David Plaisted. , in Dov M. Gabbay, C. J. Hogger and John Alan Robinson (Eds.), Handbook of Logic in Artificial Intelligence and Logic Programming, Volume 1.

"Equational reasoning and term rewriting systems"

Jürgen Avenhaus and Klaus Madlener. "Term rewriting and equational reasoning". In Ranan B. Banerji (Ed.), Formal Techniques in Artificial Intelligence: A Sourcebook, Elsevier (1990).

The

Rewriting Home Page

IFIP Working Group 1.6

by Aart Middeldorp, University of Innsbruck

Researchers in rewriting

Termination Portal

— a software implementation of a generic term rewriting system.[5]

Maude System