<p>This is an entire field of research! In general, you cannot ensure termination of $R\cup\{l\rightarrow r\}$ by examining simply $l\rightarrow r$ and the knowledge that $R$ is terminating.</p>

<p>Indeed, even if $l\rightarrow r$ shares no function symbols with $R$ you may introduce non-termination! Here is a famous counter-example by Toyama. Take the following systems:</p>

<p>$$f(0,1,x) \rightarrow f(x,x,x)$$
and
$$p(x,y) \rightarrow x $$
$$p(x,y) \rightarrow y$$</p>

<p>each system individually is terminating, and you'll note that both systems do not share symbols, and are o̶r̶t̶h̶o̶g̶o̶n̶a̶l̶,̶ ̶a̶s̶ ̶i̶s̶ ̶t̶h̶e̶ ̶u̶n̶i̶o̶n̶ ̶o̶f̶ ̶t̶h̶e̶ ̶s̶y̶s̶t̶e̶m̶ <strong>not orthogonal at all!</strong> However, the combination is not terminating. The following term rewrites for ever: $f(p(0,1), p(0,1), p(0,1))$. </p>

<p>There is a further counter-example in which both systems are confluent. However orthogonality is a sufficient condition for modular termination (in addition to not sharing symbols). see <a href="https://ac.els-cdn.com/S0304397512008286/1-s2.0-S0304397512008286-main.pdf" rel="nofollow noreferrer">this</a> survey of modularity results by Gramlich.</p>

<p>However, there are ways to modularly add rules to a rewrite system <em>even with shared function symbols</em> without introducing non-termination. The most common is <a href="http://www.sciencedirect.com/science/article/pii/S0304397599002078" rel="nofollow noreferrer">dependency pairs</a>. There is a syntactic criterion that guarentees that you do not add cycles to the <em>dependency graph</em>, which captures possible sequences of rule applications.</p>

<p>The dependency graph is uncomputable, but there is a simple heuristic which allows to over-approximate it in an efficient way. If the rule does add a cycle to the graph, all is not lost! It becomes necessary to attempt to find an ordering that makes the rule safe to remove. <a href="https://verify.rwth-aachen.de/giesl/papers/Induction-Journal-distribute.pdf" rel="nofollow noreferrer">Here's</a> an overview of the <a href="http://aprove.informatik.rwth-aachen.de/index.asp?subform=termination_proofs.html" rel="nofollow noreferrer">AProVE</a> system which implements many many techniques to show termination of rewrite systems in general. You might want to check the associated references.</p>

CC BY-SA 3.0
2017-11-02T14:39:47.920Z
how is the second system orthogonal? doesn't $p(x,y)$ in the first rule overlap with $p(x,y)$ in the second rule?
Adam
CC BY-SA 3.0
2017-11-02T15:08:57.803Z
@Adam oh no that is an embarrassing mistake! Actually orthogonality is sufficient to exclude this kind of counter-example. I'll correct this and add a reference.
cody
CC BY-SA 3.0
2017-11-02T13:33:36.100Z
2017-11-02T15:38:02.473Z
2017-11-02T15:38:02.473Z
cody
<p>I have a terminating orthogonal first-order rewriting system with finite rule set $R$. </p>

<p><strong>Question:</strong> What would be an algorithmically verifiable sufficient condition on a new rule $l\to r$ such that for the rule set $R\cup \left\{l\to r\right\}$ the system also terminates? (How to extend the rule set maintaining the termination property?)</p>

<term-rewriting-systems>
Sufficient condition for termination of an orthogonal first-order rewriting system?
Adam
# Sufficient condition for termination of an orthogonal first-order rewriting system?

(Asked by: username_0 on 2017-11-02)

I have a terminating orthogonal first-order rewriting system with finite rule set $R$.

**Question:** What would be an algorithmically verifiable sufficient condition on a new rule $l\to r$ such that for the rule set $R\cup \left\{l\to r\right\}$ the system also terminates? (How to extend the rule set maintaining the termination property?)

**Tags:** term-rewriting-systems


---

## 1 answers

### Answer by username_1 on 2017-11-02. Score: 2

This is an entire field of research! In general, you cannot ensure termination of $R\cup\{l\rightarrow r\}$ by examining simply $l\rightarrow r$ and the knowledge that $R$ is terminating.

Indeed, even if $l\rightarrow r$ shares no function symbols with $R$ you may introduce non-termination! Here is a famous counter-example by Toyama. Take the following systems:

$$f(0,1,x) \rightarrow f(x,x,x)$$
and
$$p(x,y) \rightarrow x $$
$$p(x,y) \rightarrow y$$

each system individually is terminating, and you'll note that both systems do not share symbols, and are o̶r̶t̶h̶o̶g̶o̶n̶a̶l̶,̶ ̶a̶s̶ ̶i̶s̶ ̶t̶h̶e̶ ̶u̶n̶i̶o̶n̶ ̶o̶f̶ ̶t̶h̶e̶ ̶s̶y̶s̶t̶e̶m̶ **not orthogonal at all!** However, the combination is not terminating. The following term rewrites for ever: $f(p(0,1), p(0,1), p(0,1))$.

There is a further counter-example in which both systems are confluent. However orthogonality is a sufficient condition for modular termination (in addition to not sharing symbols). see [this](https://ac.els-cdn.com/S0304397512008286/1-s2.0-S0304397512008286-main.pdf) survey of modularity results by Gramlich.

However, there are ways to modularly add rules to a rewrite system *even with shared function symbols* without introducing non-termination. The most common is [dependency pairs](http://www.sciencedirect.com/science/article/pii/S0304397599002078). There is a syntactic criterion that guarentees that you do not add cycles to the *dependency graph*, which captures possible sequences of rule applications.

The dependency graph is uncomputable, but there is a simple heuristic which allows to over-approximate it in an efficient way. If the rule does add a cycle to the graph, all is not lost! It becomes necessary to attempt to find an ordering that makes the rule safe to remove. [Here's](https://verify.rwth-aachen.de/giesl/papers/Induction-Journal-distribute.pdf) an overview of the [AProVE](http://aprove.informatik.rwth-aachen.de/index.asp?subform=termination_proofs.html) system which implements many many techniques to show termination of rewrite systems in general. You might want to check the associated references.

> **Comments:**
> **username_0**: how is the second system orthogonal? doesn't $p(x,y)$ in the first rule overlap with $p(x,y)$ in the second rule?  
> **username_1**: @username_0 oh no that is an embarrassing mistake! Actually orthogonality is sufficient to exclude this kind of counter-example. I'll correct this and add a reference.  

---

