Relating Innermost, Weak, Uniform and Modular Termination of Term Rewriting Systems

Abstract

We investigate restricted termination and confluence properties of term rewriting systems, in particular weak termination and innermost termination, and their interrelation. New criteria are provided which are sufficient for the equivalence of innermost / weak termination and uniform termination of term rewriting systems. These criteria provide interesting possibilities to infer completeness, i.e. termination plus confluence, from restricted termination and confluence properties. Using these basic results we are also able to prove some new results about modular termination of rewriting. In particular, we show that termination is modular for some classes of innermost terminating and locally confluent term rewriting systems, namely for non-overlapping and even for overlay systems. As an easy consequence this latter result also entails a simplified proof of the fact that completeness is a decomposable property of so-called constructor systems. Furthermore we show how to obtain similar results for even more general cases of (non-disjoint) combined systems with shared constructors and of certain hierarchical combinations of systems with constructors. Interestingly, these modularity results are obtained by means of a proof technique which itself constitutes a modular approach.