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.

• 03B44 - Temporal logic
• 03C07 - Basic properties of first-order languages and structures
• 03C13 - Model theory of finite structures
• 03D05 - Automata and formal grammars in connection with logical questions
• 68Q17 - Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
• 68Q19 - Descriptive complexity and finite models