Editing Rewriting

{{Short description|Replacing subterm in a formula with another term}}
{{other uses}}

In [[mathematics]], [[computer science]], and [[logic]], '''rewriting''' covers a wide range of methods of replacing subterms of a [[well-formed formula|formula]] with other terms. Such methods may be achieved by '''rewriting systems''' (also known as '''rewrite systems''', '''rewrite engines''',<ref>
[[Joseph Goguen]] "Proving and Rewriting" International Conference on Algebraic and Logic Programming, 1990 Nancy, France pp 1-24</ref><ref name="SculthorpeFrisby2014">{{cite journal |last1=Sculthorpe |first1=Neil |last2=Frisby |first2=Nicolas |last3=Gill |first3=Andy |title=The Kansas University rewrite engine |journal=[[Journal of Functional Programming]] |volume=24 |issue=4 |year=2014 |pages=434–473 |issn=0956-7968 |doi=10.1017/S0956796814000185 |s2cid=16807490 |url=http://irep.ntu.ac.uk/id/eprint/27901/1/PubSub5454_Sculthorpe.pdf |access-date=2019-02-12 |archive-date=2017-09-22 |archive-url=https://web.archive.org/web/20170922234803/http://irep.ntu.ac.uk/id/eprint/27901/1/PubSub5454_Sculthorpe.pdf |url-status=live }}</ref> or '''reduction systems'''). In their most basic form, they consist of a set of objects, plus [[Relation (mathematics)|relations]] on how to transform those objects.

Rewriting can be [[non-deterministic algorithm|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 program]]s, and several [[automated theorem proving|theorem prover]]s<ref>{{cite journal|doi=10.1016/0743-1066(92)90047-7|title=The term rewriting approach to automated theorem proving|journal=The Journal of Logic Programming|volume=14|issue=1–2|pages=71–99|year=1992|last1=Hsiang|first1=Jieh|last2=Kirchner|first2=Hélène|last3=Lescanne|first3=Pierre|last4=Rusinowitch|first4=Michaël|doi-access=free}}</ref> and [[declarative programming language]]s are based on term rewriting.<ref>{{cite journal|doi=10.1016/S0743-1066(98)10005-5 |title=Theory and practice of constraint handling rules |journal=The Journal of Logic Programming |volume=37 |issue=1–3 |pages=95–138 |year=1998 |last1=Frühwirth |first1=Thom |doi-access=free }}</ref><ref name="Clavel.Duran.Eker.2002">{{Cite journal | doi=10.1016/S0304-3975(01)00359-0| title=Maude: Specification and programming in rewriting logic| journal=Theoretical Computer Science| volume=285| issue=2| pages=187–243| year=2002| last1=Clavel| first1=M.| last2=Durán| first2=F.| last3=Eker| first3=S.| last4=Lincoln| first4=P.| last5=Martí-Oliet| first5=N.| last6=Meseguer| first6=J.| last7=Quesada| first7=J.F.| doi-access=free}}</ref>

== Example cases ==
=== Logic ===
In [[logic]], the procedure for obtaining the [[conjunctive normal form]] (CNF) of a formula can be implemented as a rewriting system.<ref name="MarriottStuckey1998">{{cite book|author1=Kim Marriott|author2=Peter J. Stuckey|title=Programming with Constraints: An Introduction|url=https://books.google.com/books?id=jBYAleHTldsC&q=%22conjunctive+normal+form%22+%28%22%28rewrite+OR+rewriting%29+%28system+OR+engine%29%22+OR+%22term+rewriting%22%29+-wikipedia&pg=PA436|year=1998|publisher=MIT Press|isbn=978-0-262-13341-8|pages=436–}}</ref> For example, the rules of such a system would be:

:<math>\neg\neg A \to A</math> ([[double negation elimination]])
:<math>\neg(A \land B) \to \neg A \lor \neg B</math> ([[De Morgan's laws]])
:<math>\neg(A \lor B)  \to \neg A \land\neg B</math>
:<math> (A \land B) \lor C \to (A \lor C) \land (B \lor C)</math> ([[distributivity]])
:<math> A \lor (B \land C) \to (A \lor B) \land (A \lor C),</math><ref group=note>This variant of the previous rule is needed since the commutative law ''A''∨''B'' = ''B''∨''A'' cannot be turned into a rewrite rule. A rule like ''A''∨''B'' → ''B''∨''A'' would cause the rewrite system to be nonterminating.</ref>
For each rule, each [[variable (mathematics)|variable]] denotes a subexpression, and the symbol (<math>\to</math>) indicates that an expression matching the left hand side of it can be rewritten to one matching the right hand side of it. In such a system, each rule is a [[logical equivalence]], so performing a rewrite on an expression by these rules does not change the truth value of it. Other useful rewriting systems in logic may not preserve truth values, see e.g. [[equisatisfiability]].

=== Arithmetic ===
Term rewriting systems can be employed to compute arithmetic operations on [[natural number]]s.
To this end, each such number has to be encoded as a [[term (logic)|term]].
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.<ref>{{cite book | author1=Jürgen Avenhaus | author2=Klaus Madlener | contribution=Term Rewriting and Equational Reasoning | pages=1&ndash;43 | title=Formal Techniques in Artificial Intelligence | editor=R.B. Banerji | publisher=Elsevier | series=Sourcebook | year=1990 }} Here: Example in sect.4.1, p.24.</ref>

: <math>\begin{align}
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{align}</math>

For example, the computation of 2+2 to result in 4 can be duplicated by term rewriting as follows:
:<math>S(S(0)) + S(S(0))</math> <math> 
\;\;\stackrel{(2)}{\to}\;\; </math> <math>S( \; S(S(0)) + S(0) \; ) </math> <math>
\;\;\stackrel{(2)}{\to}\;\; </math> <math>S(S( \; S(S(0)) + 0 \; )) </math> <math>
\;\;\stackrel{(1)}{\to}\;\; </math> <math>S(S( S(S(0)) )),</math>
where the notation above each arrow indicates the rule used for each rewrite.

As another example, the computation of 2⋅2 looks like:
:<math>S(S(0)) \cdot S(S(0))</math> <math> 
\;\;\stackrel{(4)}{\to}\;\; </math> <math>S(S(0)) + S(S(0)) \cdot S(0) </math> <math>
\;\;\stackrel{(4)}{\to}\;\; </math> <math>S(S(0)) + S(S(0)) + S(S(0)) \cdot 0</math> <math>
\;\;\stackrel{(3)}{\to}\;\; </math> <math>S(S(0)) + S(S(0)) + 0</math> <math>
\;\;\stackrel{(1)}{\to}\;\; </math> <math>S(S(0)) + S(S(0))</math> <math>
\;\;\stackrel{\textrm{s.a.}}{\to}\;\; </math> <math>S(S( S(S(0)) )),</math>
where the last step comprises the previous example computation.

=== Linguistics ===
In [[linguistics]], [[phrase structure rule]]s, also called '''rewrite rules''', are used in some systems of [[generative grammar]],<ref name="Freidin1992">{{cite book|author=Robert Freidin|title=Foundations of Generative Syntax|url=https://books.google.com/books?id=YPCVQxYmKsgC&q=%22rewrite+rules%22|year=1992|publisher=MIT Press|isbn=978-0-262-06144-5}}</ref> as a means of generating the grammatically correct sentences of a language. Such a rule typically takes the form <math>\rm A \rightarrow X</math>, where A is a [[syntactic category]] label, such as [[noun phrase]] or [[sentence (linguistics)|sentence]], and X is a sequence of such labels or [[morpheme]]s, expressing the fact that A can be replaced by X in generating the constituent structure of a sentence. For example, the rule <math>\rm S \rightarrow NP\ VP</math> means that a sentence can consist of a noun phrase (NP) followed by a [[verb phrase]] (VP); further rules will specify what sub-constituents a noun phrase and a verb phrase can consist of, and so on.

== Abstract rewriting systems ==
{{Main|Abstract rewriting system}}

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''<ref name="Book and Otto, p. 10">Book and Otto, p. 10</ref> or ''abstract rewriting system'' (abbreviated ''ARS'').<ref>Bezem et al., p. 7,</ref> An ARS is simply a set ''A'' of objects, together with a [[binary relation]] → on ''A'' called the ''reduction relation'', ''rewrite relation''<ref>Bezem et al., p. 7</ref> or just ''reduction''.<ref name="Book and Otto, p. 10"/>

Many notions and notations can be defined in the general setting of an ARS. <math>\overset{*}\rightarrow</math> is the [[reflexive transitive closure]] of <math>\rightarrow</math>. <math>\leftrightarrow</math> is the [[symmetric closure]] of <math>\rightarrow</math>. <math>\overset{*}{\leftrightarrow}</math> is the [[reflexive transitive symmetric closure]] of <math>\rightarrow</math>. The [[Word problem (mathematics)|word problem]] for an ARS is determining, given ''x'' and ''y'', whether <math>x \overset{*}{\leftrightarrow} y</math>. An object ''x'' in ''A'' is called ''reducible'' if there exists some other ''y'' in ''A'' such that <math>x \rightarrow y</math>; otherwise it is called ''irreducible'' or a [[Normal form (abstract rewriting)|normal form]]. An object ''y'' is called a "normal form of ''x''" if <math>x \stackrel{*}{\rightarrow} y</math>, and ''y'' is irreducible. If the normal form of ''x'' is unique, then this is usually denoted with <math>x{\downarrow}</math>. If every object has at least one normal form, the ARS is called ''normalizing''. <math>x \downarrow y</math> or ''x'' and ''y'' are said to be ''joinable'' if there exists some ''z'' with the property that <math>x \overset{*}{\rightarrow} z \overset{*}{\leftarrow} y</math>. An ARS is said to possess the [[Church–Rosser property]] if <math>x \overset{*}{\leftrightarrow} y</math> implies <math>x \downarrow y</math>. An ARS is [[Confluence (abstract rewriting)|confluent]] if for all ''w'', ''x'', and ''y'' in ''A'',  <math>x \overset{*}{\leftarrow} w \overset{*}{\rightarrow} y</math> implies <math>x \downarrow y</math>. An ARS is ''locally confluent'' if and only if for all ''w'', ''x'', and ''y'' in ''A'',  <math>x \leftarrow w \rightarrow y</math> implies <math>x\mathbin\downarrow y</math>. An ARS is said to be ''terminating'' or ''noetherian'' if there is no infinite chain <math>x_0 \rightarrow x_1 \rightarrow x_2 \rightarrow \cdots</math>. A confluent and terminating ARS is called ''convergent'' or ''canonical''.

Important theorems for abstract rewriting systems are that an ARS is [[Confluence (abstract rewriting)|confluent]] [[iff]] 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 (mathematics)|word problem]] for an ARS is [[undecidable problem|undecidable]] in general.

== String rewriting systems ==
{{Main|String rewriting system}}

A ''string rewriting system'' (SRS), also known as ''semi-Thue system'', exploits the [[free monoid]] structure of the [[String (computer science)|strings]] (words) over an [[Alphabet (computer science)|alphabet]] to extend a rewriting relation, <math>R</math>, to ''all'' strings in the alphabet that contain left- and respectively right-hand sides of some rules as [[substring]]s. Formally a semi-Thue system is a [[tuple]] <math>(\Sigma, R)</math> where <math>\Sigma</math> is a (usually finite) alphabet, and <math>R</math> is a binary relation between some (fixed) strings in the alphabet, called the set of ''rewrite rules''. The ''one-step rewriting relation'' <math>\underset{R}\rightarrow</math> induced by <math>R</math> on <math>\Sigma^*</math> is defined as: if <math>s, t \in \Sigma^*</math> are any strings, then <math>s \underset{R}\rightarrow t</math> if there exist <math>x, y, u, v \in \Sigma^*</math> such that <math>s = xuy</math>, <math>t = xvy</math>, and <math>u R v</math>. Since <math>\underset{R}\rightarrow</math> is a relation on <math>\Sigma^*</math>, the pair <math>(\Sigma^*, \underset{R}\rightarrow)</math> fits the definition of an abstract rewriting system. Since the empty string is in <math>\Sigma^*</math>, <math>R</math> is a subset of <math>\underset{R}\rightarrow</math>. If the relation <math>R</math> is [[symmetric relation|symmetric]], then the system is called a ''Thue system''.

In a SRS, the reduction relation <math>\overset{*}\underset{R}\rightarrow</math> is compatible with the monoid operation, meaning that <math>x \overset{*}\underset{R}\rightarrow y</math> implies <math>uxv \overset{*}\underset{R}\rightarrow uyv</math> for all strings <math>x, y, u, v \in \Sigma^*</math>. Similarly, the reflexive transitive symmetric closure of <math>\underset{R}\rightarrow</math>, denoted <math>\overset{*}{\underset R \leftrightarrow}</math>, is a [[Congruence relation|congruence]], meaning it is an [[equivalence relation]] (by definition) and it is also compatible with string concatenation. The relation <math>\overset{*}\underset{R} \leftrightarrow</math> is called the ''Thue congruence'' generated by <math>R</math>. In a Thue system, i.e. if <math>R</math> is symmetric, the rewrite relation <math>\overset{*}\underset{R}\rightarrow</math> coincides with the Thue congruence <math>\overset{*}{\underset R \leftrightarrow}</math>.

The notion of a semi-Thue system essentially coincides with the [[presentation of a monoid]]. Since <math>\overset{*}{\underset R \leftrightarrow}</math> is a congruence, we can define the [[factor monoid]] <math>\mathcal{M}_R = \Sigma^*/\overset{*}{\underset R \leftrightarrow}</math> of the free monoid <math>\Sigma^*</math> by the Thue congruence. If a monoid <math>\mathcal{M}</math> is [[isomorphic]] with <math>\mathcal{M}_R</math>, then the semi-Thue system <math>(\Sigma, R)</math> is called a [[monoid presentation]] of <math>\mathcal{M}</math>.

We immediately get some very useful connections with other areas of algebra. For example, the alphabet <math>\{ a,b \}</math> with the rules <math>\{ ab \rightarrow \varepsilon, ba \rightarrow \varepsilon \}</math>, where <math>\varepsilon</math> is the [[empty string]], is a presentation of the [[free group]] on one generator. If instead the rules are just <math>\{ ab \rightarrow \varepsilon \}</math>, then we obtain a presentation of the [[bicyclic monoid]]. Thus semi-Thue systems constitute a natural framework for solving the [[word problem (mathematics)|word problem]] for monoids and groups. In fact, every monoid has a presentation of the form <math>(\Sigma, R)</math>, i.e. it may always be presented by a semi-Thue system, possibly over an infinite alphabet.

The word problem for a semi-Thue system is undecidable in general; this result is sometimes known as the ''Post–Markov theorem''.<ref>Martin Davis et al. 1994, p.&nbsp;178</ref>

== Term rewriting systems ==

[[File:Triangle diagram of rewrite rule application svg.svg|thumb|'''Pic.1:''' Schematic triangle diagram of application of a rewrite rule <math>l \longrightarrow r</math> at position <math>p</math> in a term, with matching substitution <math>\sigma</math>]]
[[File:Example term for position, path, depth, match svg.svg|thumb|'''Pic.2:''' Rule lhs term <math>x*(y*z)</math> matching in term <math>\frac{a*((a+1)*(a+2))}{1*(2*3)}</math>]]
A '''term rewriting system''' ('''TRS''') is a rewriting system whose objects are ''[[term (logic)|terms]]'', which are expressions with nested sub-expressions. For example, the system shown under ''{{section link||Logic}}'' above is a term rewriting system. The terms in this system are composed of binary operators <math>(\vee)</math> and <math>(\wedge)</math> and the unary operator <math>(\neg)</math>. Also present in the rules are variables, which represent any possible term (though a single variable always represents the same term throughout a single rule).

In contrast to string rewriting systems, whose objects are sequences of symbols, the objects of a term rewriting system form a [[term algebra]]. A term can be visualized as a tree of symbols, the set of admitted symbols being fixed by a given [[signature (logic)|signature]]. As a formalism, term rewriting systems have the full power of [[Turing machine]]s, that is, every [[computable function]] can be defined by a term rewriting system.<ref>Dershowitz, Jouannaud (1990), sect.1, p.245</ref>

Some programming languages are based on term rewriting. One such example is Pure, a functional programming language for mathematical applications.<ref>{{Cite journal |last=Albert |first=Gräf |date=2009 |title=Signal Processing in the Pure Programming Language |url=https://archive.org/details/LAC2009SignalProcessingInThePureProgrammingLanguage_Paper |journal=Linux Audio Conference}}</ref><ref>{{Cite web |last=Riepe |first=Von Michael |date=November 18, 2009 |title=Pure – eine einfache funktionale Sprache |url=https://www.heise.de/hintergrund/Rein-ins-Vergnuegen-856225.html |archive-url=https://web.archive.org/web/20110319165239/http://www.heise.de/ix/artikel/Rein-ins-Vergnuegen-856225.html |archive-date=March 19, 2011}}</ref>

===Formal definition <span class="anchor" id="Redex"></span>===
{{Redirect|Redex|the medication|Tadalafil}}
A ''rewrite rule'' is a pair of [[Term (logic)|terms]], commonly written as <math>l \rightarrow r</math>, to indicate that the left-hand side {{math|''l''}} can be replaced by the right-hand side {{math|''r''}}. A ''term rewriting system'' is a set {{math|''R''}} of such rules. A rule <math>l \rightarrow r</math> can be ''applied'' to a term {{math|''s''}} if the left term {{math|l}} [[Term (logic)#Operations with terms|matches]] some [[Term (logic)#Operations with terms|subterm]] of {{math|''s''}}, that is, if there is some [[substitution (logic)|substitution]] <math>\sigma</math> such that the subterm of <math>s</math> rooted at some [[Term (logic)#Operations with terms|position]] {{math|''p''}} is the result of applying the substitution <math>\sigma</math> to the term {{math|l}}. The subterm matching the left hand side of the rule is called a '''redex''' or '''reducible expression'''.<ref name=Klop>{{cite web |last1=Klop |first1=J. W. |title=Term Rewriting Systems |url=http://www.cs.tau.ac.il/~nachum/papers/klop.pdf |website=Papers by Nachum Dershowitz and students |publisher=Tel Aviv University |access-date=14 August 2021 |page=12 |archive-date=15 August 2021 |archive-url=https://web.archive.org/web/20210815025906/http://www.cs.tau.ac.il/~nachum/papers/klop.pdf |url-status=live }}</ref> The result term {{math|''t''}} of this rule application is then the result of [[Term (logic)#Operations with terms|replacing the subterm]] at position {{math|''p''}} in {{math|''s''}} by the term  <math>r</math> with the substitution <math>\sigma</math> applied, see picture 1. In this case, <math>s</math> is said to be ''rewritten in one step'', or ''rewritten directly'', to <math>t</math> by the system <math>R</math>, formally denoted as <math>s \rightarrow_R t</math>, <math> s \underset{R}\rightarrow t</math>, or as <math>s \overset{R}\rightarrow t</math> by some authors.

If a term <math>t_1</math> can be rewritten in several steps into a term <math>t_n</math>, that is, if <math>t_1 \underset{R}\rightarrow t_2 \underset{R}\rightarrow \cdots \underset{R}\rightarrow t_n</math>, the term <math>t_1</math> is said to be ''rewritten'' to <math>t_n</math>, formally denoted as <math>t_1 \overset{+}\underset{R}\rightarrow t_n</math>. In other words, the relation <math>\overset{+}\underset{R}\rightarrow</math> is the [[transitive closure]] of the relation <math>\underset{R}\rightarrow</math>; often, also the notation <math>\overset{*}\underset{R}\rightarrow</math> is used to denote the [[Closure (mathematics)#Binary relation closures|reflexive-transitive closure]] of <math>\underset{R}\rightarrow</math>, that is, <math>s \overset{*}\underset{R}\rightarrow t</math> if <math>s = t</math> or {{nobreak|<math>s \overset{+}\underset{R}\rightarrow t</math>.<ref>{{cite book| author=N. Dershowitz, [[J.-P. Jouannaud]]| title=Rewrite Systems| year=1990| volume=B| pages=243–320| publisher=Elsevier| editor=Jan van Leeuwen| editor-link=Jan van Leeuwen| series=Handbook of Theoretical Computer Science}}; here: Sect.&nbsp;2.3</ref>}} A term rewriting given by a set <math>R</math> of rules can be viewed as an abstract rewriting system as defined [[#Abstract rewriting systems|above]], with terms as its objects and <math>\underset{R}\rightarrow</math> as its rewrite relation.

For example, <math>x*(y*z) \rightarrow (x*y)*z</math> is a rewrite rule, commonly used to establish a normal form with respect to the associativity of <math>*</math>.
That rule can be applied at the numerator in the term <math>\frac{a*((a+1)*(a+2))}{1*(2*3)}</math> with the matching substitution <math>\{ x \mapsto a, \; y \mapsto a+1, \; z \mapsto a+2 \}</math>, see picture 2.<ref group="note">since applying that substitution to the rule's left hand side <math>x*(y*z)</math> yields the numerator <math>a*((a+1)*(a+2))</math></ref> Applying that substitution to the rule's right-hand side yields the term <math>(a*(a+1))*(a+2)</math>, and replacing the numerator by that term yields <math>\frac{(a*(a+1))*(a+2)}{1*(2*3)}</math>, which is the result term of applying the rewrite rule. Altogether, applying the rewrite rule has achieved what is called "applying the associativity law for <math>*</math> to <math>\frac{a*((a+1)*(a+2))}{1*(2*3)}</math>" in elementary algebra. Alternately, the rule could have been applied to the denominator of the original term, yielding <math>\frac{a*((a+1)*(a+2))}{(1*2)*3}</math>.

===Termination===
Termination issues of rewrite systems in general are handled in ''[[Abstract rewriting system#Termination and convergence]]''. For term rewriting systems in particular, the following additional subtleties are to be considered.

Termination even of a system consisting of one rule with a [[Term (logic)#Ground and linear terms|linear]] left-hand side is undecidable.<ref>{{cite book| author=Max Dauchet|  chapter=Simulation of Turing Machines by a Left-Linear Rewrite Rule| title=Proc. 3rd Int. Conf. on [[Rewriting Techniques and Applications]]| year=1989|volume=355| pages=109–120| publisher=Springer|series=LNCS}}</ref><ref>{{cite journal | author=Max Dauchet | title=Simulation of Turing machines by a regular rewrite rule | journal=[[Theoretical Computer Science (journal)|Theoretical Computer Science]] | volume=103 | number=2 | pages=409&ndash;420 | date=Sep 1992 | doi=10.1016/0304-3975(92)90022-8 | doi-access=free }}</ref>  Termination is also undecidable for systems using only unary function symbols; however, it is decidable for finite [[Term (logic)#Ground and linear terms|ground]] systems.<ref>{{cite tech report| author=Gerard Huet, D.S. Lankford| title=On the Uniform Halting Problem for Term Rewriting Systems|date=Mar 1978| number=283| pages=8| institution=IRIA| url=https://www.ens-lyon.fr/LIP/REWRITING/TERMINATION/Huet_Lankford.pdf| access-date=16 June 2013}}</ref>

The following term rewrite system is normalizing,<ref group=note>i.e. for each term, some normal form exists, e.g. ''h''(''c'',''c'') has the normal forms ''b'' and ''g''(''b''), since ''h''(''c'',''c'') → ''f''(''h''(''c'',''c''),''h''(''c'',''c'')) → ''f''(''h''(''c'',''c''),''f''(''h''(''c'',''c''),''h''(''c'',''c''))) → ''f''(''h''(''c'',''c''),''g''(''h''(''c'',''c'')))  →  ''b'', and ''h''(''c'',''c'') → ''f''(''h''(''c'',''c''),''h''(''c'',''c'')) → ''g''(''h''(''c'',''c'')) → ... → ''g''(''b''); neither ''b'' nor ''g''(''b'') can be rewritten any further, therefore the system is not confluent</ref> but not terminating,<ref group=note>i.e., there are infinite derivations, e.g. ''h''(''c'',''c'') → ''f''(''h''(''c'',''c''),''h''(''c'',''c'')) → ''f''(''f''(''h''(''c'',''c''),''h''(''c'',''c'')) ,''h''(''c'',''c'')) → ''f''(''f''(''f''(''h''(''c'',''c''),''h''(''c'',''c'')),''h''(''c'',''c'')) ,''h''(''c'',''c'')) → ...</ref> and not confluent:<ref>{{cite book| author=Bernhard Gramlich| chapter=Relating Innermost, Weak, Uniform, and Modular Termination of Term Rewriting Systems| title=Proc. International Conference on Logic Programming and Automated Reasoning (LPAR)| date=Jun 1993| volume=624| pages=285–296| publisher=Springer| editor=Voronkov, Andrei| series=LNAI| chapter-url=http://www.logic.at/staff/gramlich/papers/lpar92.ps.gz| title-link=International Conference on Logic Programming and Automated Reasoning| access-date=2014-06-19| archive-date=2016-03-04| archive-url=https://web.archive.org/web/20160304185714/http://www.logic.at/staff/gramlich/papers/lpar92.ps.gz| url-status=live}} Here: Example 3.3</ref>
<math display="block">\begin{align}
f(x,x)    & \rightarrow g(x) , \\
f(x,g(x)) & \rightarrow b , \\
h(c,x)    & \rightarrow f(h(x,c),h(x,x)) . \\
\end{align}</math>

The following two examples of terminating term rewrite systems are due to Toyama:<ref>{{cite journal| author=Yoshihito Toyama| title=Counterexamples to Termination for the Direct Sum of Term Rewriting Systems| journal=Inf. Process. Lett.| year=1987| volume=25| issue=3| pages=141–143| url=http://www.nue.ie.niigata-u.ac.jp/toyama/user/toyama/research/paper/journal/counterexamples.pdf| doi=10.1016/0020-0190(87)90122-0| hdl=2433/99946| hdl-access=free| access-date=2019-11-13| archive-date=2019-11-13| archive-url=https://web.archive.org/web/20191113091157/http://www.nue.ie.niigata-u.ac.jp/toyama/user/toyama/research/paper/journal/counterexamples.pdf| url-status=live}}</ref> 
:<math>f(0,1,x) \rightarrow f(x,x,x)</math> 
and 
:<math>g(x,y) \rightarrow x,</math>
:<math>g(x,y) \rightarrow y.</math>

Their union is a non-terminating system, since

<math display="block">\begin{align}
& 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{align}</math>
This result disproves a conjecture of [[Nachum Dershowitz|Dershowitz]],<ref>{{cite book| author=N. Dershowitz| chapter=Termination| title=Proc. RTA| year=1985| volume=220| pages=180–224| publisher=Springer| editor=Jean-Pierre Jouannaud| editor-link=Jean-Pierre Jouannaud| series=LNCS| chapter-url=http://www.cs.tau.ac.il/~nachum/papers/LNCS/Termination.pdf| access-date=2013-06-16| archive-date=2013-11-12| archive-url=https://web.archive.org/web/20131112200935/http://www.cs.tau.ac.il/~nachum/papers/LNCS/Termination.pdf| url-status=live}}; here: p.210</ref> who claimed that the union of two terminating term rewrite systems <math>R_1</math> and <math>R_2</math> is again terminating if all left-hand sides of <math>R_1</math> and right-hand sides of <math>R_2</math> are [[Term (logic)#Ground and linear terms|linear]], and there are no "''overlaps''" between left-hand sides of <math>R_1</math> and right-hand sides of <math>R_2</math>. All these properties are satisfied by Toyama's examples.

See [[Rewrite order]] and [[Path ordering (term rewriting)]] for ordering relations used in termination proofs for term rewriting systems.

=== Higher-order rewriting systems ===

Higher-order rewriting systems are a generalization of first-order term rewriting systems to [[lambda term]]s, allowing higher order functions and bound variables.<ref name=Wolfram>{{cite book |first1=D. A. |last1=Wolfram |title=The Clausal Theory of Types |date=1993 |publisher=Cambridge University Press |pages=47–50 |doi=10.1017/CBO9780511569906|isbn=9780521395380 |s2cid=42331173 }}</ref> Various results about first-order TRSs can be reformulated for HRSs as well.<ref>{{cite book |last1=Nipkow |first1=Tobias |last2=Prehofer |first2=Christian |editor1-last=Bibel |editor1-first=W. |editor2-last=Schmitt |editor2-first=P. |title=Automated Deduction - A Basis for Applications. Volume I: Foundations |date=1998 |publisher=Kluwer |pages=399–430 |chapter=Higher-Order Rewriting and Equational Reasoning |chapter-url=https://www21.in.tum.de/~nipkow/pubs/ded-book.html |access-date=2021-08-16 |archive-date=2021-08-16 |archive-url=https://web.archive.org/web/20210816153129/https://www21.in.tum.de/~nipkow/pubs/ded-book.html |url-status=live }}</ref>

=== Graph rewriting systems ===

[[Graph rewriting|Graph rewrite systems]] are another generalization of term rewrite systems, operating on [[graph (graph theory)|graphs]] instead of ([[ground term|ground]]-) [[term (logic)|terms]] / their corresponding [[tree (graph theory)|tree]] representation.

== Trace rewriting systems ==
[[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.

==See also==
* [[Critical pair (logic)]]
*[[Compiler]]
* [[Knuth–Bendix completion algorithm]]
* [[L-system]]s specify rewriting that is done in parallel.
* [[Referential transparency]] in computer science
* [[Regulated rewriting]]
* [[Interaction nets|Interaction Nets]]

== Notes ==
{{NoteFoot}}

== Further reading ==
* {{cite book |first1=Franz|last1=Baader|author1-link=Franz Baader |first2=Tobias|last2=Nipkow|author2-link=Tobias Nipkow |title=Term rewriting and all that |publisher=Cambridge University Press |isbn = 978-0-521-77920-3 |year=1999 }} 316 pages.
* [[Marc Bezem]], [[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.
* [[Nachum Dershowitz]] and [[Jean-Pierre Jouannaud]] [http://citeseer.ist.psu.edu/dershowitz90rewrite.html "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.&nbsp;243&ndash;320. The [[preprint]] of this chapter is freely available from the authors, but it is missing the figures.
* Nachum Dershowitz and [[David Plaisted]]. [https://www.cs.tau.ac.il/~nachum/papers/hand-final.pdf "Rewriting"], Chapter 9 in [[John Alan Robinson]] and [[Andrei Voronkov]] (Eds.), ''[[Handbook of Automated Reasoning]], Volume 1''.
* [[Gérard Huet]] et Derek Oppen, [http://infolab.stanford.edu/pub/cstr/reports/cs/tr/80/785/CS-TR-80-785.pdf Equations and Rewrite Rules, A Survey] (1980) Stanford Verification Group, Report N° 15 Computer Science Department Report N° STAN-CS-80-785
* [[Jan Willem Klop]]. "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''.
* David Plaisted. [http://rewriting.loria.fr/documents/plaisted.ps.gz "Equational reasoning and term rewriting systems"], in [[Dov M. Gabbay]], [[C. J. Hogger]] and [[John Alan Robinson]] (Eds.), ''[[Handbook of Logic in Artificial Intelligence and Logic Programming]], Volume 1''.
* 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).
; String rewriting
* [[Ronald V. Book]] and Friedrich Otto, ''String-Rewriting Systems'', Springer (1993).
* Benjamin Benninghofen, Susanne Kemmerich and [[Michael M. Richter]], ''Systems of Reductions''. [[Lecture Notes in Computer Science|LNCS]] '''277''', Springer-Verlag (1987).
; Other
* [[Martin Davis (mathematician)|Martin Davis]], [[Ron Sigal]], [[Elaine J. Weyuker]], (1994) ''Computability, Complexity, and Languages: Fundamentals of Theoretical Computer Science – 2nd edition'', Academic Press, {{ISBN|0-12-206382-1}}.

== External links ==
{{Wiktionary}}
* The [http://rewriting.loria.fr/ Rewriting Home Page]
* [https://ifip-wg-rewriting.cs.ru.nl/ IFIP Working Group 1.6]
* [http://cl-informatik.uibk.ac.at/~ami/research/rr/index.php Researchers in rewriting] by [[Aart Middeldorp]], [[University of Innsbruck]]
* [https://www.termination-portal.org/ Termination Portal]
* [https://maude.cs.illinois.edu/w/index.php/The_Maude_System Maude System] &mdash; a software implementation of a generic term rewriting system.<ref name="Clavel.Duran.Eker.2002"/>

== References ==
{{Reflist}}

{{Authority control}}

[[Category:Formal languages]]
[[Category:Logic in computer science]]
[[Category:Mathematical logic]]
[[Category:Rewriting systems]]