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.