An actual implementation of a procedure that mechanically proves termination of rewriting systems based on inequalities between polynomial interpretations

Abstract

A method based on polynomial interpretations is currently implemented in REVE. Though this termination check procedure is absolutely necessary in order to run some of the examples we know, like Associativity+Endomorphism, we do not think it will replace the current methods based on recursive path ordering [Dersh82] or recursive decomposition ordering [Jouan.etal.82], since they have shown to have a large scope and to be really easy to use in many practical cases [Forg&Det185], and Dershowitz has exhibited examples where polynomial interpretation fail [Dersh83]. So, we think we will keep both methods in REVE and let the user choose the method he or she wants to use. However in the case of associative-commutative operators, the methods based on extensions of the recursive path ordering either fail or are not ready for being incorporated in a rewrite rule laboratory like REVE. So, it is the only method currently available and we are incorporating it into REVE-3 (the general equational rewriting laboratory) as the mechanism for proving termination in the associative-commutative case.

In conclusion, we would like to mention a limit of our criterion. It cannot prove the positiveness of the polynomial x ²₁ +x ²₂ −2x₁x₂+1=(x₁−x₂)²+1. Since we never encountered such a polynomial in termination proofs we feel that would not be an obstacle for using it.