RELATING INNERMOST, WEAK, UNIFORM AND MODULAR TERMINATION OF TERM REWRITING-SYSTEMS

Term rewriting systems play an important role in various areas, e.g. in abstract data type specifications, for automated theorem proving and as a basic computation model for functional programming languages. In theory and practice, one of the most important properties of term rewriting systems is the strong normalization or (finite or uniform) termination property which is undecidable in general. For ensuring this property many sufficient criteria and methods based on well-founded term orderings have been developed. In this paper we follow another line of research and study restricted termination 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. 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 locally confluent overlay systems. As an easy consequence this result also entails a simplified proof of the fact that completeness is a decomposable property of so-called constructor systems. Interestingly, these modularity results are obtained by means of a proof technique which itself constitutes a modular approach.