Editing Rewriting (section)

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