A SEQUENTIAL REDUCTION STRATEGY

Kennaway proved the remarkable result that every (almost) orthogonal t erm rewriting system admits a computable sequential normalizing reduct ion strategy. In this paper we present a computable sequential reducti on strategy similar in scope, but simpler and more general. Our strate gy can be thought of as an outermost-fair-like strategy that is allowe d to be unfair to some redex of a term when contracting the redex is u seless for the normalization of the term. Unlike the strategy of Kenna way, our strategy does not rely on syntactic restrictions that imply c onfluence. On the contrary, it can easily be applied to any term rewri ting system, and we show that the class of term rewriting systems for which our strategy is normalizing properly includes all (almost) ortho gonal systems. Our strategy is more versatile; in case of (almost) ort hogonal term rewriting systems, it can be used to detect certain cases of non-termination, Our normalization proof is more accessible than K ennaway's. We also show that our sequential strategy sometimes succeed s where the parallel-outermost strategy fails.