Infinitary Combinatory Reduction Systems: Confluence

J. Ketema, Jakob Grue Simonsen

    Research output: Contribution to journalArticleAcademicpeer-review

    12 Citations (Scopus)
    82 Downloads (Pure)


    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 languageUndefined
    Article number10.2168/LMCS-5(4:3)2009
    Pages (from-to)-
    Number of pages29
    JournalLogical methods in computer science
    Issue number4
    Publication statusPublished - 20 Dec 2009


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

    Cite this