Some reduction strategies for algebraic term rewriting

A general algorithm for reduction with algebraic term rewriting systems is presented and several aspects of rewriting are discussed.It turns out that the well known strategies of innermost and outermost rewriting, which are special cases of the general algorithm, exhibit good performance under different aspects. The general rewriting algorithm suggests improvements for naive reduction algorithms with specific strategies, which in some cases give them better asymptotic behaviour. Empirical results with an algebraic axiomatization of natural numbers show considerably faster runtimes for the improved algorithms.The algorithms presented here do not impose any restrictions on the rewriting systems. They are currently used both within an implementation of the Knuth-Bendix completion algorithm and in a separate term reduction system, whenever sufficiently large terms are involved.