Infinitary Combinatory Reduction Systems: Confluence

J. Ketema; Jakob Grue Simonsen

doi:10.2168/LMCS-5(4:3)2009

Infinitary Combinatory Reduction Systems: Confluence

J. Ketema, Jakob Grue Simonsen

Research output: Contribution to journal › Article › Academic › peer-review

12 Citations (Scopus)

58 Downloads (Pure)

Abstract

We study confluence in the setting of higher-order infinitary rewriting, in particular for infinitary Combinatory Reduction Systems (iCRSs). We prove that fully-extended, 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.

Original language	Undefined
Article number	10.2168/LMCS-5(4:3)2009
Pages (from-to)	-
Number of pages	29
Journal	Logical methods in computer science
Volume	5
Issue number	4
DOIs	https://doi.org/10.2168/LMCS-5(4:3)2009
Publication status	Published - 20 Dec 2009

Keywords

CR-F.3.2
CR-F.4.1
EWI-16396
CR-F.4.2
CR-D.3.1
METIS-264431
IR-69174

Access to Document

10.2168/LMCS-5(4:3)2009

ketema-0910.4081
open
ketema-0910.4081
open

Cite this

Ketema, J., & Simonsen, J. G. (2009). Infinitary Combinatory Reduction Systems: Confluence. Logical methods in computer science, 5(4), -. [10.2168/LMCS-5(4:3)2009]. https://doi.org/10.2168/LMCS-5(4:3)2009

@article{b4d8cdf52733421ba06b2c85489a4eed,

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 fully-extended, 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.",

keywords = "CR-F.3.2, CR-F.4.1, EWI-16396, CR-F.4.2, CR-D.3.1, METIS-264431, IR-69174",

author = "J. Ketema and Simonsen, {Jakob Grue}",

note = "10.2168/LMCS-5(4:3)2009",

year = "2009",

month = "12",

day = "20",

doi = "10.2168/LMCS-5(4:3)2009",

language = "Undefined",

volume = "5",

pages = "--",

journal = "Logical methods in computer science",

issn = "1860-5974",

publisher = "Technische Universitat Braunschweig",

number = "4",

}

TY - JOUR

T1 - Infinitary Combinatory Reduction Systems: Confluence

AU - Ketema, J.

AU - Simonsen, Jakob Grue

N1 - 10.2168/LMCS-5(4:3)2009

PY - 2009/12/20

Y1 - 2009/12/20

N2 - We study confluence in the setting of higher-order infinitary rewriting, in particular for infinitary Combinatory Reduction Systems (iCRSs). We prove that fully-extended, 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 fully-extended, 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.

KW - CR-F.3.2

KW - CR-F.4.1

KW - EWI-16396

KW - CR-F.4.2

KW - CR-D.3.1

KW - METIS-264431

KW - IR-69174

U2 - 10.2168/LMCS-5(4:3)2009

DO - 10.2168/LMCS-5(4:3)2009

M3 - Article

VL - 5

SP - -

JO - Logical methods in computer science

JF - Logical methods in computer science

SN - 1860-5974

IS - 4

M1 - 10.2168/LMCS-5(4:3)2009

ER -