On modularity in infinitary term rewriting
Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › fagfællebedømt
Standard
On modularity in infinitary term rewriting. / Simonsen, Jakob Grue.
I: Information and Computation, Bind 204, Nr. 6, 01.01.2006, s. 957-988.Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › fagfællebedømt
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - JOUR
T1 - On modularity in infinitary term rewriting
AU - Simonsen, Jakob Grue
PY - 2006/1/1
Y1 - 2006/1/1
N2 - 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.
AB - 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.
KW - Church-Rosser property
KW - Confluence
KW - Infinitary rewriting
KW - Modularity
KW - Normalization
KW - Strong convergence
KW - Term rewriting
UR - http://www.scopus.com/inward/record.url?scp=84855194957&partnerID=8YFLogxK
U2 - 10.1016/j.ic.2006.02.005
DO - 10.1016/j.ic.2006.02.005
M3 - Journal article
AN - SCOPUS:84855194957
VL - 204
SP - 957
EP - 988
JO - Information and Computation
JF - Information and Computation
SN - 0890-5401
IS - 6
ER -
ID: 224020714