INFINITARY COMBINATORY REDUCTION SYSTEMS: NORMALISING REDUCTION STRATEGIES
We study normalising reduction strategies for infinitary Combinatory Reduction Systems (iCRSs). We prove that all fair, outermost-fair, and needed-fair strategies are normalising for orthogonal, fully-extended iCRSs. These facts properly generalise a number of results on normalising strategies in first-order infinitary rewriting and provide the first examples of normalising strategies for infinitary lambda-calculus.
combinatory reduction systems reduction strategies term rewriting higher-order computation lambda-calculus infinite computation normal forms