On modularity in infinitary term rewriting

Research output: Contribution to journalJournal articleResearchpeer-review

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 noncollapsing. • 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.

Original languageEnglish
JournalInformation and Computation
Volume204
Issue number6
Pages (from-to)957-988
Number of pages32
ISSN0890-5401
DOIs
Publication statusPublished - 1 Jan 2006

    Research areas

  • Church-Rosser property, Confluence, Infinitary rewriting, Modularity, Normalization, Strong convergence, Term rewriting

ID: 224020714