We study confluence in the setting of higher-order infinitary rewriting, inparticular for infinitary Combinatory Reduction Systems (iCRSs). We prove thatfully-extended, orthogonal iCRSs are confluent modulo identification ofhypercollapsing subterms. As a corollary, we obtain that fully-extended,orthogonal iCRSs have the normal form property and the unique normal formproperty (with respect to reduction). We also show that, unlike the case infirst-order infinitary rewriting, almost non-collapsing iCRSs are notnecessarily confluent.
展开▼
