Reduction Strategies and Acyclicity


In this paper we review some well-known theory about reduction strategies of various kinds: normalizing, outermost-fair, cofinal, Church-Rosser. A stumbling block in the definition of such strategies is the presence of reduction cycles that may `trap' a strategy as it is memory-free. We exploit a recently (re)discovered fact that there are no reduction cycles in orthogonal rewrite systems when each term has a normal form, in order to enhance some of the theorems on strategies, both with respect to their scope and the proof of their correctness.