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