Abstract

A property of term rewriting systems is called modular if it is preserved under disjoint union. For unconditional term rewriting systems several modularity results are known. The aim of this paper is to analyze and extend these results to conditional term rewriting systems. It turns out that conditional term rewriting is much more complicated than unconditional rewriting from a modularity point of view. For instance, we will show that the modularity of weak normalization for unconditional term rewriting systems does not extend to conditional term rewriting systems. On the positive side, we mention the extension of Toyama's confluence result for disjoint unions of term rewriting systems to conditional term rewriting systems.

BibTeX Entry

@article{M-IC93,
 author    = "Aart Middeldorp",
 title     = "Modular Properties of Conditional Term Rewriting Systems",
 journal   = "Information and Computation",
 volume    = 104,
 number    = 1,
 pages     = "110--158",
 year      = 1993,
 doi       = "10.1006/inco.1993.1027"
}

Erratum

Bernhard Gramlich (On Modularity of Termination and Confluence Properties of Conditional Rewrite Systems, Proceedings of the 4th International Conference on Algebraic and Logic Programming, LNCS 850, pp. 186-203, 1994) provided a counterexample to Theorem 5.2. By a complicated analysis he showed that its two main consequences, Corollary 5.4 and Theorem 5.6, remain valid.