Note: [] This research was supported by the ‘Deutsche Forschungsgemeinschaft, SFB 314 (D4-Projekt)’.
Abstract: We investigate restricted termination and confluence properties of term rewriting systems, in particular weak termination, weak innermost termination, (strong) innermost termination, (strong) termination, and their interrelations. New criteria are provided which are sufficient for the equivalence of these properties. These criteria provide interesting possibilities to infer completeness, i.e. termination plus confluence, from restricted termination and confluence properties. Our main result states that any (strongly) innermost terminating, locally confluent overlay system is terminating, and hence confluent and complete. 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 constructor systems. Similarly, a combined overlay system with shared constructors is complete if and only if its component sytems are complete overlay systems. Interestingly, these modularity results are obtained by means of a proof technique which itself constitutes a modular approach.
Keywords: Term rewriting systems, confluence, termination, weak termination, innermost termination, modularity, disjoint union, constructor systems, combination of constructor systems, combined systems with shared constructors
