Infinitary Combinatory Reduction Systems: Confluence

Research output: Contribution to journal › Journal article › Research › peer-review

Standard

Infinitary Combinatory Reduction Systems: Confluence. / Ketema, Jeroen; Simonsen, Jakob Grue.

In: Logical Methods in Computer Science, Vol. 5, No. 4:3, 2009, p. 1-29.

Research output: Contribution to journal › Journal article › Research › peer-review

Harvard

Ketema, J & Simonsen, JG 2009, 'Infinitary Combinatory Reduction Systems: Confluence', Logical Methods in Computer Science, vol. 5, no. 4:3, pp. 1-29.

APA

Ketema, J., & Simonsen, J. G. (2009). Infinitary Combinatory Reduction Systems: Confluence. Logical Methods in Computer Science, 5(4:3), 1-29.

Vancouver

Ketema J, Simonsen JG. Infinitary Combinatory Reduction Systems: Confluence. Logical Methods in Computer Science. 2009;5(4:3):1-29.

Author

Ketema, Jeroen ; Simonsen, Jakob Grue. / Infinitary Combinatory Reduction Systems: Confluence. In: Logical Methods in Computer Science. 2009 ; Vol. 5, No. 4:3. pp. 1-29.

Bibtex

@article{56998020ee2311deba73000ea68e967b,
title = "Infinitary Combinatory Reduction Systems: Confluence",
abstract = "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.",
author = "Jeroen Ketema and Simonsen, {Jakob Grue}",
year = "2009",
language = "English",
volume = "5",
pages = "1--29",
journal = "Logical Methods in Computer Science",
issn = "1860-5974",
publisher = "International Federation for Computational Logic",
number = "4:3",

}

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