Infinitary Combinatory Reduction Systems: Confluence
Research output: Contribution to journal › Journal article › Research › peer-review
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.
Original language | English |
---|---|
Journal | Logical Methods in Computer Science |
Volume | 5 |
Issue number | 4:3 |
Pages (from-to) | 1-29 |
Number of pages | 29 |
ISSN | 1860-5974 |
Publication status | Published - 2009 |
ID: 16408467