3
$\begingroup$

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?)

$\endgroup$
2
$\begingroup$

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 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. 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 an overview of the AProVE system which implements many many techniques to show termination of rewrite systems in general. You might want to check the associated references.

$\endgroup$
  • $\begingroup$ how is the second system orthogonal? doesn't $p(x,y)$ in the first rule overlap with $p(x,y)$ in the second rule? $\endgroup$ – Adam Nov 2 '17 at 14:39
  • $\begingroup$ @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. $\endgroup$ – cody Nov 2 '17 at 15:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.