A New Decidability Technique for Ground Term Rewriting Systems with Applications

摘要

Programming language interpreters, proving equations (e.g. x~3 = x implies the ring is Abelian), abstract data types, program transformation and optimization, and even computation itself (e.g., turing machine) can all be specified by a set of rules, called a rewrite system. Two fundamental properties of a rewrite system are the confluence or Church—Rosser property and the unique normalization property. In this article, we develop a standard form for ground rewrite systems and the concept of standard rewriting. These concepts are then used to: prove a pumping lemma for them, and to derive a new and direct decidability technique for decision problems of ground rewrite systems. To illustrate the usefulness of these concepts, we apply them to prove: (ⅰ) polynomial size bounds for witnesses to violations of unique normalization and confluence for ground rewrite systems containing unary symbols and constants, and (ⅱ) polynomial height bounds for witnesses to violations of unique normalization and confluence for arbitrary ground systems. Apart from the fact that our technique is direct in contrast to previous decidability results for both problems, which were indirectly obtained using tree automata techniques, this approach also yields tighter bounds for rewrite systems with unary symbols than the ones that can be derived with the indirect approach. Finally, as part of our results, we give a polynomial-time algorithm for checking whether a rewrite system has the unique normalization property for all subterms in the rules of the system.