Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
427518 | Information and Computation | 2006 | 32 Pages |
We study modular properties in strongly convergent infinitary term rewriting. In particular, we show that:•Confluence is not preserved across direct sum of a finite number of systems, even when these are non-collapsing.•Confluence modulo equality of hypercollapsing subterms is not preserved across direct sum of a finite number of systems.•Normalization is not preserved across direct sum of an infinite number of left-linear systems.•Unique normalization with respect to reduction is not preserved across direct sum of a finite number of left-linear systems.Together, these facts constitute a radical departure from the situation in finitary term rewriting. Positive results are:•Confluence is preserved under the direct sum of an infinite number of left-linear systems iff at most one system contains a collapsing rule.•Confluence is preserved under the direct sum of a finite number of non-collapsing systems if only terms of finite rank are considered.•Top-termination is preserved under the direct sum of a finite number of left-linear systems.•Normalization is preserved under the direct sum of a finite number of left-linear systems.All of the negative results above hold in the setting of weakly convergent rewriting as well, as do the positive results concerning modularity of top-termination and normalization for left-linear systems.