Überarbeitung

In Mathematik , Linguistik , Informatik und Logik umfasst das Umschreiben eine Vielzahl von Methoden, um Unterterme einer Formel durch andere Terme zu ersetzen . Solche Methoden lassen sich durch Umschreibsysteme (auch bekannt als Umschreibsysteme , Umschreibmaschinen ^{[ 1 ] [ 2 ]} oder Reduktionssysteme ) realisieren. In ihrer einfachsten Form bestehen sie aus einer Menge von Objekten und Relationen , die festlegen, wie diese Objekte transformiert werden.

Das Umschreiben von Termen kann nichtdeterministisch sein . Eine Regel zum Umschreiben eines Terms kann auf viele verschiedene Arten auf diesen Term angewendet werden, oder es können mehrere Regeln anwendbar sein. Umschreibsysteme liefern daher keinen Algorithmus zum Ersetzen eines Terms durch einen anderen, sondern eine Menge möglicher Regelanwendungen. In Kombination mit einem geeigneten Algorithmus können Umschreibsysteme jedoch als Computerprogramme betrachtet werden , und mehrere Theorembeweiser ^{[ 3 ]} und deklarative Programmiersprachen basieren auf dem Umschreiben von Termen. ^{[ 4 ] [ 5 ]}

In der Logik lässt sich das Verfahren zur Bestimmung der konjunktiven Normalform (KNF) einer Formel als Umformungssystem implementieren. ^{[ 6 ]} Die Regeln eines solchen Systems wären beispielsweise:

${\displaystyle \neg \neg A\to A}$( Eliminierung der doppelten Negation )

${\displaystyle \neg (A\land B)\to \neg A\lor \neg B}$( De Morgansche Gesetze )

${\displaystyle \neg (A\lor B)\to \neg A\land \neg B}$

${\displaystyle (A\land B)\lor C\to (A\lor C)\land (B\lor C)}$( Distributivität )

${\displaystyle A\lor (B\land C)\to (A\lor B)\land (A\lor C),}$^{[ Anmerkung 1 ]}

In jeder Regel bezeichnet jede Variable einen Teilausdruck, und das Symbol ( ) zeigt an, dass ein Ausdruck, der der linken Seite entspricht, in einen Ausdruck umgeschrieben werden kann, der der rechten Seite entspricht. In einem solchen System stellt jede Regel eine logische Äquivalenz dar ; daher ändert eine Umformung eines Ausdrucks mithilfe dieser Regeln dessen Wahrheitswert nicht. Andere nützliche Umformungssysteme in der Logik erhalten möglicherweise nicht den Wahrheitswert (siehe z. B. Äquisitifizierbarkeit ). ${\displaystyle \to }$

Termersetzungssysteme können zur Berechnung arithmetischer Operationen mit natürlichen Zahlen verwendet werden . Dazu muss jede Zahl als Term kodiert werden . Die einfachste Kodierung ist die in den Peano-Axiomen verwendete , basierend auf der Konstanten 0 (Null) und der Nachfolgerfunktion S. Beispielsweise werden die Zahlen 0, 1, 2 und 3 durch die Terme 0, S(0), S(S(0)) bzw. S(S(S(0))) dargestellt. Das folgende Termersetzungssystem kann dann zur Berechnung von Summe und Produkt gegebener natürlicher Zahlen verwendet werden. ^{[ 7 ]}

${\displaystyle {\begin{aligned}A+0&\to A&{\textrm {(1)}},\\A+S(B)&\to S(A+B)&{\textrm {(2)}},\\A\cdot 0&\to 0&{\textrm {(3)}},\\A\cdot S(B)&\to A+(A\cdot B)&{\textrm {(4)}}.\end{aligned}}}$

Beispielsweise kann die Rechnung 2+2, die 4 ergibt, durch Umformung der Terme wie folgt wiederholt werden:

${\displaystyle S(S(0))+S(S(0))}$${\displaystyle \;\;{\stackrel {(2)}{\to }}\;\;}$${\displaystyle S(\;S(S(0))+S(0)\;)}$${\displaystyle \;\;{\stackrel {(2)}{\to }}\;\;}$${\displaystyle S(S(\;S(S(0))+0\;))}$${\displaystyle \;\;{\stackrel {(1)}{\to }}\;\;}$${\displaystyle S(S(S(S(0)))),}$

wobei die Notation über jedem Pfeil die für die jeweilige Umformung verwendete Regel angibt.

Ein weiteres Beispiel: Die Berechnung von 2⋅2 sieht folgendermaßen aus:

${\displaystyle S(S(0))\cdot S(S(0))}$${\displaystyle \;\;{\stackrel {(4)}{\to }}\;\;}$${\displaystyle S(S(0))+S(S(0))\cdot S(0)}$${\displaystyle \;\;{\stackrel {(4)}{\to }}\;\;}$${\displaystyle S(S(0))+S(S(0))+S(S(0))\cdot 0}$${\displaystyle \;\;{\stackrel {(3)}{\to }}\;\;}$${\displaystyle S(S(0))+S(S(0))+0}$${\displaystyle \;\;{\stackrel {(1)}{\to }}\;\;}$${\displaystyle S(S(0))+S(S(0))}$${\displaystyle \;\;{\stackrel {\textrm {s.a.}}{\to }}\;\;}$${\displaystyle S(S(S(S(0)))),}$

wobei der letzte Schritt die Berechnung des vorherigen Beispiels umfasst.

In der Linguistik werden Phrasenstrukturregeln , auch Umschreibungsregeln genannt, in einigen Systemen generativer Grammatiken [ ^{8 ] verwendet} , um grammatikalisch korrekte Sätze einer Sprache zu erzeugen. Eine solche Regel hat typischerweise die Form , wobei A eine syntaktische Kategoriebezeichnung wie Nominalphrase oder Satz ist und X eine Folge solcher Bezeichnungen oder Morpheme darstellt . Diese drückt aus, dass A bei der Generierung der Satzstruktur durch X ersetzt werden kann. Beispielsweise bedeutet die Regel , dass ein Satz aus einer Nominalphrase (NP) gefolgt von einer Verbalphrase (VP) bestehen kann; weitere Regeln spezifizieren, aus welchen Unterkonstituenten eine Nominalphrase und eine Verbalphrase bestehen können usw. ${\displaystyle {\rm {A\rightarrow X}}}$${\displaystyle {\rm {S\rightarrow NP\ VP}}}$

Aus den obigen Beispielen geht hervor, dass wir Umschreibungssysteme abstrakt betrachten können. Wir müssen eine Menge von Objekten und die Regeln, die zu ihrer Transformation angewendet werden können, spezifizieren. Die allgemeinste (eindimensionale) Formulierung dieses Konzepts wird als abstraktes Reduktionssystem ^{[ 9 ]} oder abstraktes Umschreibungssystem (abgekürzt ARS ) ^{[ 10 ]} bezeichnet . Ein ARS ist einfach eine Menge A von Objekten zusammen mit einer binären Relation → auf A , die Reduktionsrelation , Umschreibungsrelation ^{[ 11 ]} oder einfach Reduktion genannt wird . ^{[ 9 ]}

Many notions and notations can be defined in the general setting of an ARS. ${\displaystyle {\overset {*}{\rightarrow }}}$ is the reflexive transitive closure of ${\displaystyle \rightarrow }$. ${\displaystyle \leftrightarrow }$ is the symmetric closure of ${\displaystyle \rightarrow }$. ${\displaystyle {\overset {*}{\leftrightarrow }}}$ is the reflexive transitive symmetric closure of ${\displaystyle \rightarrow }$. The word problem for an ARS is determining, given x and y, whether ${\displaystyle x{\overset {*}{\leftrightarrow }}y}$. An object x in A is called reducible if there exists some other y in A such that ${\displaystyle x\rightarrow y}$; otherwise it is called irreducible or a normal form. An object y is called a "normal form of x" if ${\displaystyle x{\stackrel {*}{\rightarrow }}y}$, and y is irreducible. If the normal form of x is unique, then this is usually denoted with ${\displaystyle x{\downarrow }}$. If every object has at least one normal form, the ARS is called normalizing. ${\displaystyle x\downarrow y}$ or x and y are said to be joinable if there exists some z with the property that ${\displaystyle x{\overset {*}{\rightarrow }}z{\overset {*}{\leftarrow }}y}$. An ARS is said to possess the Church–Rosser property if ${\displaystyle x{\overset {*}{\leftrightarrow }}y}$ implies ${\displaystyle x\downarrow y}$. An ARS is confluent if for all w, x, and y in A, ${\displaystyle x{\overset {*}{\leftarrow }}w{\overset {*}{\rightarrow }}y}$ implies ${\displaystyle x\downarrow y}$. An ARS is locally confluent if and only if for all w, x, and y in A, ${\displaystyle x\leftarrow w\rightarrow y}$ implies ${\displaystyle x{\mathbin {\downarrow }}y}$. An ARS is said to be terminating or noetherian if there is no infinite chain ${\displaystyle x_{0}\rightarrow x_{1}\rightarrow x_{2}\rightarrow \cdots }$. A confluent and terminating ARS is called convergent or canonical.

Important theorems for abstract rewriting systems are that an ARS is confluentiff it has the Church–Rosser property, Newman's lemma (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.

Ein String-Ersetzungssystem (SRS), auch bekannt als Semi-Thue-System , nutzt die freie Monoidstruktur der Strings (Wörter) über einem Alphabet , um eine Ersetzungsrelation auf alle Strings im Alphabet zu erweitern, die die linke bzw. rechte Seite bestimmter Regeln als Teilstrings enthalten . Formal ist ein Semi-Thue-System ein Tupel , wobei ein (üblicherweise endliches) Alphabet und eine binäre Relation zwischen einigen (festen) Strings im Alphabet ist, der sogenannten Menge der Ersetzungsregeln . Die durch auf induzierte Ein-Schritt-Ersetzungsrelation ist definiert als: Sind beliebige Strings, dann gilt: Wenn es ein gibt , sodass , und . Da eine Relation auf ist , erfüllt das Paar die Definition eines abstrakten Ersetzungssystems. Da der leere String in liegt , ist eine Teilmenge von . Ist die Relation symmetrisch , so wird das System als Thue- System bezeichnet . ${\displaystyle R}$${\displaystyle (\Sigma ,R)}$${\displaystyle \Sigma }$${\displaystyle R}$${\displaystyle {\underset {R}{\rightarrow }}}$${\displaystyle R}$${\displaystyle \Sigma ^{*}}$${\displaystyle s,t\in \Sigma ^{*}}$${\displaystyle s{\underset {R}{\rightarrow }}t}$${\displaystyle x,y,u,v\in \Sigma ^{*}}$${\displaystyle s=xuy}$${\displaystyle t=xvy}$${\displaystyle uRv}$${\displaystyle {\underset {R}{\rightarrow }}}$${\displaystyle \Sigma ^{*}}$${\displaystyle (\Sigma ^{*},{\underset {R}{\rightarrow }})}$${\displaystyle \Sigma ^{*}}$${\displaystyle R}$${\displaystyle {\underset {R}{\rightarrow }}}$${\displaystyle R}$

In einem SRS ist die Reduktionsrelation mit der Monoidoperation kompatibel, d. h., sie impliziert für alle Zeichenketten . Analog dazu ist der reflexive transitive symmetrische Abschluss von , bezeichnet mit , eine Kongruenz , d. h. sie ist (per Definition) eine Äquivalenzrelation und ebenfalls mit der Zeichenkettenverkettung kompatibel. Die Relation wird als Thue-Kongruenz bezeichnet , die von erzeugt wird . In einem Thue-System, d. h. wenn symmetrisch ist, stimmt die Umschreibungsrelation mit der Thue-Kongruenz überein . ${\displaystyle {\overset {*}{\underset {R}{\rightarrow }}}}$${\displaystyle x{\overset {*}{\underset {R}{\rightarrow }}}y}$${\displaystyle uxv{\overset {*}{\underset {R}{\rightarrow }}}uyv}$${\displaystyle x,y,u,v\in \Sigma ^{*}}$${\displaystyle {\underset {R}{\rightarrow }}}$${\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}$${\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}$${\displaystyle R}$${\displaystyle R}$${\displaystyle {\overset {*}{\underset {R}{\rightarrow }}}}$${\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}$

Der Begriff des Semi-Thue-Systems entspricht im Wesentlichen der Präsentation eines Monoids . Da es sich um eine Kongruenz handelt, können wir das Faktormonoid des freien Monoids durch die Thue-Kongruenz definieren. Ist ein Monoid isomorph zu , so wird das Semi-Thue-System als Monoidpräsentation von bezeichnet . ${\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}$${\displaystyle {\mathcal {M}}_{R}=\Sigma ^{*}/{\overset {*}{\underset {R}{\leftrightarrow }}}}$${\displaystyle \Sigma ^{*}}$${\displaystyle {\mathcal {M}}}$${\displaystyle {\mathcal {M}}_{R}}$${\displaystyle (\Sigma ,R)}$${\displaystyle {\mathcal {M}}}$

Wir erhalten unmittelbar einige sehr nützliche Verbindungen zu anderen Gebieten der Algebra. Beispielsweise ist das Alphabet mit den Regeln , wobei die leere Zeichenkette ist , eine Präsentation der freien Gruppe über einem Erzeuger. Lauten die Regeln stattdessen nur , so erhalten wir eine Präsentation des bizyklischen Monoids . Somit bilden semi-Thue-Systeme einen natürlichen Rahmen zur Lösung des Wortproblems für Monoide und Gruppen. Tatsächlich besitzt jedes Monoid eine Präsentation der Form , d. h. es kann stets durch ein semi-Thue-System präsentiert werden, möglicherweise über einem unendlichen Alphabet. ${\displaystyle \{a,b\}}$${\displaystyle \{ab\rightarrow \varepsilon ,ba\rightarrow \varepsilon \}}$${\displaystyle \varepsilon }$${\displaystyle \{ab\rightarrow \varepsilon \}}$${\displaystyle (\Sigma ,R)}$

Das Wortproblem für ein semi-Thue-System ist im Allgemeinen unentscheidbar; dieses Ergebnis ist manchmal als Post-Markov-Theorem bekannt . ^{[ 12 ]}

Ein Termersetzungssystem ( TRS ) ist ein System, dessen Objekte Terme sind , also Ausdrücke mit verschachtelten Teilausdrücken. Das oben unter § Logik dargestellte System ist beispielsweise ein Termersetzungssystem. Die Terme dieses Systems bestehen aus den binären Operatoren und und dem unären Operator . Die Regeln enthalten außerdem Variablen, die jeden möglichen Term repräsentieren (wobei eine einzelne Variable innerhalb einer Regel immer denselben Term repräsentiert). ${\displaystyle (\vee )}$${\displaystyle (\wedge )}$${\displaystyle (\neg )}$

Im Gegensatz zu String-Ersetzungssystemen, deren Objekte Symbolfolgen sind, bilden die Objekte eines Term-Ersetzungssystems eine Termalgebra . Ein Term lässt sich als Symbolbaum visualisieren, wobei die Menge der zulässigen Symbole durch eine gegebene Signatur festgelegt ist . Als Formalismus besitzen Term-Ersetzungssysteme die volle Leistungsfähigkeit von Turingmaschinen , d. h. jede berechenbare Funktion kann durch ein Term-Ersetzungssystem definiert werden. ^{[ 13 ]}

Einige Programmiersprachen basieren auf Termersetzung. Ein Beispiel hierfür ist Pure, eine funktionale Programmiersprache für mathematische Anwendungen. ^{[ 14 ] [ 15 ]}

Eine Umschreibungsregel ist ein Termpaar , üblicherweise geschrieben als , das angibt, dass die linke Seite l durch die rechte Seite r ersetzt werden kann . Ein Termumschreibungssystem ist eine Menge R solcher Regeln. Eine Regel kann auf einen Term s angewendet werden , wenn der linke Term l mit einem Unterterm von s übereinstimmt , d. h., wenn es eine Substitution gibt , sodass der Unterterm von an Position p das Ergebnis der Anwendung der Substitution auf den Term l ist . Der Unterterm, der mit der linken Seite der Regel übereinstimmt, wird als Redex oder reduzierbarer Ausdruck bezeichnet . ^{[ 16 ]} Der Ergebnisterm t dieser Regelanwendung ist dann das Ergebnis der Ersetzung des Unterterms an Position p in s durch den Term mit der angewendeten Substitution (siehe Abbildung 1). In diesem Fall wird gesagt, dass in einem Schritt umgeschrieben oder direkt durch das System in umgeschrieben wird , formal als , oder von einigen Autoren als bezeichnet .${\displaystyle l\rightarrow r}$${\displaystyle l\rightarrow r}$${\displaystyle \sigma }$${\displaystyle s}$${\displaystyle \sigma }$${\displaystyle r}$${\displaystyle \sigma }$${\displaystyle s}$${\displaystyle t}$${\displaystyle R}$${\displaystyle s\rightarrow _{R}t}$${\displaystyle s{\underset {R}{\rightarrow }}t}$${\displaystyle s{\overset {R}{\rightarrow }}t}$

Lässt sich ein Term in mehreren Schritten in einen Term umschreiben , d. h. wenn , so spricht man von einer Umschreibung zu , formal als . Anders ausgedrückt: Die Relation ist der transitive Abschluss der Relation . Oft wird auch die Notation verwendet, um den reflexiv-transitiven Abschluss von zu bezeichnen , d. h. wenn oder . ^{[ 17 ]} Eine durch eine Menge von Regeln gegebene Termumschreibung kann als abstraktes Umschreibungssystem im oben definierten Sinne betrachtet werden , mit Termen als Objekten und als Umschreibungsrelation. ${\displaystyle t_{1}}$${\displaystyle t_{n}}$${\displaystyle t_{1}{\underset {R}{\rightarrow }}t_{2}{\underset {R}{\rightarrow }}\cdots {\underset {R}{\rightarrow }}t_{n}}$${\displaystyle t_{1}}$${\displaystyle t_{n}}$${\displaystyle t_{1}{\overset {+}{\underset {R}{\rightarrow }}}t_{n}}$${\displaystyle {\overset {+}{\underset {R}{\rightarrow }}}}$${\displaystyle {\underset {R}{\rightarrow }}}$${\displaystyle {\overset {*}{\underset {R}{\rightarrow }}}}$${\displaystyle {\underset {R}{\rightarrow }}}$${\displaystyle s{\overset {*}{\underset {R}{\rightarrow }}}t}$${\displaystyle s=t}$${\displaystyle s{\overset {+}{\underset {R}{\rightarrow }}}t}$${\displaystyle R}$${\displaystyle {\underset {R}{\rightarrow }}}$

Beispielsweise ist eine Umformungsregel, die häufig verwendet wird, um eine Normalform bezüglich der Assoziativität von zu etablieren . Diese Regel kann auf den Zähler des Terms mit der entsprechenden Substitution angewendet werden (siehe Abbildung 2). ^{[ Anmerkung 2 ]} Wendet man diese Substitution auf die rechte Seite der Regel an, erhält man den Term , und ersetzt man den Zähler durch diesen Term , erhält man , welches der Ergebnisterm der Anwendung der Umformungsregel ist. Insgesamt hat die Anwendung der Umformungsregel das erreicht, was in der elementaren Algebra als „Anwendung des Assoziativgesetzes von auf “ bezeichnet wird. Alternativ hätte die Regel auch auf den Nenner des ursprünglichen Terms angewendet werden können, was zu hätte führen würde . ${\displaystyle x*(y*z)\rightarrow (x*y)*z}$${\displaystyle *}$${\displaystyle {\frac {a*((a+1)*(a+2))}{1*(2*3)}}}$${\displaystyle \{x\mapsto a,\;y\mapsto a+1,\;z\mapsto a+2\}}$${\displaystyle (a*(a+1))*(a+2)}$${\displaystyle {\frac {(a*(a+1))*(a+2)}{1*(2*3)}}}$${\displaystyle *}$${\displaystyle {\frac {a*((a+1)*(a+2))}{1*(2*3)}}}$${\displaystyle {\frac {a*((a+1)*(a+2))}{(1*2)*3}}}$

Terminierungsprobleme von Rewriting-Systemen im Allgemeinen werden in „Abstrakte Rewriting-Systeme#Terminierung und Konvergenz“ behandelt . Insbesondere für Term-Rewriting-Systeme sind die folgenden zusätzlichen Feinheiten zu beachten.

Die Terminierung selbst eines Systems, das nur aus einer Regel mit linearer linker Seite besteht, ist unentscheidbar. ^{[ 18 ] [ 19 ]} Auch für Systeme, die ausschließlich unäre Funktionssymbole verwenden, ist die Terminierung unentscheidbar; für Systeme mit endlichem Grundgrund ist sie jedoch entscheidbar . ^{[ 20 ]}

Das folgende Termersetzungssystem ist normalisierend, ^{[ Anmerkung 3 ]} aber nicht terminierend, ^{[ Anmerkung 4 ]} und nicht konfluent: ^{[ 21 ].}$${\displaystyle {\begin{aligned}f(x,x)&\rightarrow g(x),\\f(x,g(x))&\rightarrow b,\\h(c,x)&\rightarrow f(h(x,c),h(x,x)).\\\end{aligned}}}$$

Die folgenden beiden Beispiele für Systeme zur Umschreibung von terminierenden Termen gehen auf Toyama zurück: ^{[ 22 ]}

${\displaystyle f(0,1,x)\rightarrow f(x,x,x)}$

Und

${\displaystyle g(x,y)\rightarrow x,}$

${\displaystyle g(x,y)\rightarrow y.}$

Ihre Vereinigung ist ein System ohne Auflösung, da

$${\displaystyle {\begin{aligned}&f(g(0,1),g(0,1),g(0,1))\\\rightarrow &f(0,g(0,1),g(0,1))\\\rightarrow &f(0,1,g(0,1))\\\rightarrow &f(g(0,1),g(0,1),g(0,1))\\\rightarrow &\cdots \end{aligned}}}$$ Dieses Ergebnis widerlegt eine Vermutung von Dershowitz ^{[ 23 ]} , der behauptete, dass die Vereinigung zweier endlicher Termersetzungssysteme wieder endlich ist , wenn alle linken Seiten von und alle rechten Seiten von linear sind und es keine Überlappungen zwischen den linken Seiten von und den rechten Seiten von gibt . Alle diese Eigenschaften werden durch Toyamas Beispiele erfüllt. ${\displaystyle R_{1}}$${\displaystyle R_{2}}$${\displaystyle R_{1}}$${\displaystyle R_{2}}$${\displaystyle R_{1}}$${\displaystyle R_{2}}$

Siehe Umschreibungsreihenfolge und Pfadreihenfolge (Term-Umschreibung) für Ordnungsrelationen, die in Terminierungsbeweisen für Term-Umschreibungssysteme verwendet werden.

Höhere Umschreibungssysteme sind eine Verallgemeinerung von Termumschreibungssystemen erster Ordnung auf Lambda-Terme und ermöglichen Funktionen höherer Ordnung und beschränkte Variablen. ^{[ 24 ]} Verschiedene Ergebnisse über Termumschreibungssysteme erster Ordnung lassen sich auch auf höhere Umschreibungssysteme übertragen. ^{[ 25 ]}

Graph-Rewrite-Systeme sind eine weitere Verallgemeinerung von Term-Rewrite-Systemen, die auf Graphen anstatt auf ( Grund- ) Termen bzw. deren entsprechender Baumdarstellung operieren .

Die Spurentheorie ermöglicht es, Multiprocessing formaler zu beschreiben, beispielsweise mithilfe des Spurenmonoids und des Verlaufsmonoids . Auch in Spurensystemen lassen sich Umschreibungen durchführen.

• Kritisches Paar (Logik)
• Compiler
• Knuth-Bendix-Vervollständigungsalgorithmus
• L-Systeme spezifizieren das Umschreiben, das parallel erfolgt.
• Referenzielle Transparenz in der Informatik
• Reguliertes Umschreiben
• Interaktionsnetze

• Baader, Franz ; Nipkow, Tobias (1999). Term rewriting and all that . Cambridge University Press. ISBN 978-0-521-77920-3Die316 Seiten.
• Marc Bezem , Jan Willem Klop , Roel de Vrijer („Terese“), Term Rewriting Systems („TeReSe“), Cambridge University Press, 2003, ISBN 0-521-39115-6Dies ist die aktuellste umfassende Monographie. Sie verwendet jedoch eine beträchtliche Anzahl noch nicht standardisierter Notationen und Definitionen. Beispielsweise wird die Church-Rosser-Eigenschaft als identisch mit der Konfluenz definiert.
• Nachum Dershowitz und Jean-Pierre Jouannaud, „Rewrite Systems“ , Kapitel 6 in: Jan van Leeuwen (Hrsg.), Handbook of Theoretical Computer Science , Band B: Formal Models and Semantics , Elsevier und MIT Press, 1990, ISBN 0-444-88074-7, S. 243–320. Die Vorabversion dieses Kapitels ist bei den Autoren frei erhältlich, enthält jedoch keine Abbildungen.
• Nachum Dershowitz und David Plaisted . „Rewriting“ , Kapitel 9 in John Alan Robinson und Andrei Voronkov (Hrsg.), Handbook of Automated Reasoning , Band 1 .
• Gérard Huet und Derek Oppen, Equations and Rewrite Rules, A Survey (1980) Stanford Verification Group, Bericht Nr. 15, Bericht der Informatikabteilung Nr. STAN-CS-80-785
• Jan Willem Klop . "Term Rewriting Systems", Kapitel 1 in Samson Abramsky , Dov M. Gabbay und Tom Maibaum (Hrsg.), Handbook of Logic in Computer Science , Band 2: Hintergrund: Computerstrukturen .
• David Plaisted. „Gleichungslogik und Termersetzungssysteme“ , in Dov M. Gabbay , CJ Hogger und John Alan Robinson (Hrsg.), Handbuch der Logik in der Künstlichen Intelligenz und der Logikprogrammierung , Band 1 .
• Jürgen Avenhaus und Klaus Madlener. „Term-Rewriting und Gleichungslogik“. In: Ranan B. Banerji (Hrsg.), Formale Techniken in der Künstlichen Intelligenz: Ein Quellenbuch , Elsevier (1990).

String-Umschreibung

• Ronald V. Book und Friedrich Otto, String-Rewriting Systems , Springer (1993).
• Benjamin Benninghofen, Susanne Kemmerich und Michael M. Richter , Systeme der Reduktion . LNCS 277 , Springer-Verlag (1987).

Andere

• Martin Davis , Ron Sigal , Elaine J. Weyuker (1994) : Berechenbarkeit, Komplexität und Sprachen: Grundlagen der theoretischen Informatik – 2. Auflage , Academic Press, ISBN 0-12-206382-1Die

• Die Startseite zum Thema Umschreiben
• IFIP-Arbeitsgruppe 1.6
• Forscher im Bereich des Umschreibens von Aart Middeldorp , Universität Innsbruck
• Kündigungsportal
• Maude-System – eine Software-Implementierung eines generischen Termersetzungssystems. ^{[ 5 ]}