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 | |
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