Vicious circles in rewriting systems

Abstract

We continue our study of the difference between Weak Normalisation (WN) and Strong Normalisation (SN). We extend our earlier result that orthogonal TRSs with the property WN do not admit cyclic reductions, into three distinct directions: (i) to the higher-order case, where terms may contain bound variables, (ii) to the weakly orthogonal case, where rules may have (trivial) conflicts, and (iii) to weak head normalisation (WHN), where terms have head normal forms. By adapting the techniques introduced for each of the three extensions separately, we even are able to show the result generalises to each pair of combinations and to various λ-calculi. The combination of all three extensions remains open however.