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


Bernhard Gramlich
Fachbereich Informatik, Universitaet Kaiserslautern
Erwin-Schroedinger-Str., 67663 Kaiserslautern, Germany
E-mail: gramlich@informatik.uni-kl.de


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 {\em modular} approach.


Key Words
Term rewriting systems, confluence, termination, weak
termination, innermost termination, modularity, disjoint union,
combined systems with shared constructors, constructor systems,
hierarchical combinations.

Source
anonymous FTP server ftp.uni-kl.de [131.246.94.94]
path: /reports_uni-kl/computer_science/SEKI/1993/papers/
file: Gramlich.SR-93-09.ps.Z