On the Modularity of Decidability of Completeness and Termination
Kai Salomaa · Universitätsbibliothek Gießen · 1996
We consider decision problems for direct sums of term rewriting systems where the components belong to classes for which the corresponding property is decidable. We show that decidability of termination is not a modular property for finite left-linear monadic term rewriting systems. It is known that termination is not modular [28]. Our result generalizes this nonmodularity result by establishing that for given two terminating finite left-linear term rewriting systems we cannot even decide algorithmically Whether or not their direct sum terminates Decidability of confluence and decidability of completeness of (left- or right-) linear term rewriting systems are shown to be modular. Decidability of completeness of general systems is shown to be nonmodular.