Generalized sufficient conditions for modular termination of rewriting (Q1328180): Difference between revisions

Since rewrite systems can be seen as programs of a functional programming language, there is some interest in the following question: Given two rewrite systems \(R_ 1\) and \(R_ 2\), both having property \(P\), under which conditions does the union \(R_ 1 \cup R_ 2\) have property \(P\)? In the paper, this problem is studied for \(P\) meaning ``terminating''. This problem is nontrivial since an example of Toyama shows that \(R_ 1 \cup R_ 2\) need not be terminating even if \(R_ 1\) and \(R_ 2\) are terminating and disjoint (i.e. are defined over disjoint signatures). The property \(P\) is called modular, if \(R_ 1 \cup R_ 2\) has property \(P\) whenever \(R_ 1\) and \(R_ 2\) are disjoint and have property \(P\). It is known that termination is modular on some restricted classes of rewrite systems, e.g. on the classes of (a) non-duplicating, (b) non-collapsing, (c) left-linear and confluent, and (d) confluent overlay systems. The paper generalizes these results by classifying exactly those cases where \(R_ 1 \cup R_ 2\) is non-terminating: \(R\) is called ``termination preserving under non-deterministic collapses'' if termination of \(R\) implies termination of \(R \cup \{G(x,y) \to x\), \(G(x,y) \to y\}\), where \(G\) is a new function symbol. Now the main result of the paper is: ``If \(R_ 1\) and \(R_ 2\) are disjoint terminating rewrite systems and \(R_ 1 \cup R_ 2\) is non-terminating, then one of the systems is not termination preserving under non-deterministic collapses and the other one is collapsing''. Unfortunately, it is undecidable whether \(R\) is termination preserving under non-deterministic collapses. The main result is generalized in several directions. For example, the assumption that \(R_ 1\) and \(R_ 2\) are disjoint can be weakend to the assumption that \(R_ 1\) and \(R_ 2\) share only constructor symbols.