ON THE MODULARITY OF TERMINATION OF TERM REWRITING-SYSTEMS

It is well-known that termination is not a modular property of term rewriting systems, i.e., it is not preserved under disjoint union. The objective of this paper is to provide a ''uniform framework'' for sufficient coditions which ensure the modularity of termination. We will prove the following result. Whenever the disjoint union of two terminating term rewriting systems is nonterminating, then one of the systems is not C-E-terminating (i.e., it loses its termination property when extended with the rules Cons(x, y)--> x and Cons(x, y)--> y) and the other is collapsing. This result has already been achieved by Gramlich [7] for finitely branching term rewriting systems. A more sophisticated approach is necessary, however, to prove it in full generality. Most of the known sufficient criteria for the preservation of termination [24,.15, 13, 7] follow as corollaries from our result, and new criteria are derived. This paper particularly settles the open question whether simple termination is modular in general. We will moreover shed some light on modular properties of combined systems with shared constructors. For instance, it will be shown that the above result does not carry over to constructor-sharing systems.