Fairness in term rewriting systems

Abstract

The notion of fair derivation in a term-rewriting system is introduced, whereby every rewrite rule enabled infinitely often along a derivation is infinitely-often applied. A term-rewriting system is fairly-terminating iff all its fair derivations are finite. The paper presents the following question: is it decidable, for an arbitrary ground term rewriting system, whether it fairly terminates or not? A positive answer is given for several subcases. The general case remains open.