Editing Rewriting (section)

== 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.