Infinitary Combinatory Reduction Systems: Confluence
Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › fagfællebedømt
Standard
Infinitary Combinatory Reduction Systems: Confluence. / Ketema, Jeroen; Simonsen, Jakob Grue.
I: Logical Methods in Computer Science, Bind 5, Nr. 4:3, 2009, s. 1-29.Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › fagfællebedømt
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - JOUR
T1 - Infinitary Combinatory Reduction Systems: Confluence
AU - Ketema, Jeroen
AU - Simonsen, Jakob Grue
PY - 2009
Y1 - 2009
N2 - We study confluence in the setting of higher-order infinitary rewriting, in particular for infinitary Combinatory Reduction Systems (iCRSs). We prove that fullyextended, orthogonal iCRSs are confluent modulo identification of hypercollapsing subterms. As a corollary, we obtain that fully-extended, orthogonal iCRSs have the normal form property and the unique normal form property (with respect to reduction). We also show that, unlike the case in first-order infinitary rewriting, almost non-collapsing iCRSs are not necessarily confluent.
AB - We study confluence in the setting of higher-order infinitary rewriting, in particular for infinitary Combinatory Reduction Systems (iCRSs). We prove that fullyextended, orthogonal iCRSs are confluent modulo identification of hypercollapsing subterms. As a corollary, we obtain that fully-extended, orthogonal iCRSs have the normal form property and the unique normal form property (with respect to reduction). We also show that, unlike the case in first-order infinitary rewriting, almost non-collapsing iCRSs are not necessarily confluent.
M3 - Journal article
VL - 5
SP - 1
EP - 29
JO - Logical Methods in Computer Science
JF - Logical Methods in Computer Science
SN - 1860-5974
IS - 4:3
ER -
ID: 16408467