Infinitary Combinatory Reduction Systems: Confluence

Research output: Contribution to journalJournal articleResearchpeer-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 languageEnglish
JournalLogical Methods in Computer Science
Volume5
Issue number4:3
Pages (from-to)1-29
Number of pages29
ISSN1860-5974
Publication statusPublished - 2009

ID: 16408467