For fully-extended, orthogonal infinitary Combinatory Reduction Systems, we prove that terms with perpetual reductions starting from them do not have (head) normal forms. Using this, we show that 1. needed reduction strategies are normalising for fully-extended, orthogonal infinitary Combinatory Reduction Systems, and that 2. weak and strong normalisation coincide for such systems as a whole and, in case reductions are non-erasing, also for terms.
展开▼
