Item

Abstract

In this paper, we study modular aspects of hierarchical combinations of term rewriting systems. System $\R_0 \cup \R_1$ is a hierarchical combination if the defined symbols of two subsystems, $\R_0$ and $\R_1$ are disjoint, some of the defined symbols of $\R_0$ are constructors in $\R_1$ and the defined symbols of $\R_1$ do not occur in $\R_0$. It is shown that in hierarchical combinations, a reduction can increase the rank of a term. Therefore, techniques employed in proving modularity results for direct sums and constructor sharing systems are not applicable for hierarchical combinations. We propose a set of sufficient conditions for modularity of completeness of hierarchical combinations. The sufficient conditions are syntactic ones (about recursion) based on constructor discipline. We prove our result by showing that hierarchical combination $\R_0 \cup \R_1$ satisfying our sufficient conditions is innermost normalizing and locally confluent, if $\R_0$ and $\R_1$ are complete constructor systems. The result generalizes Middeldorp and Toyama's result on modularity of completeness for shared constructor systems.