Polynomials over the reals in proofs of termination

Authors

Salvador Lucas

Abstract

Polynomials over the real numbers were proposed as an alternative to polynomials over the naturals in termination proofs. We have recently shown how to use an arbitrary polynomial interpretation over the reals to generate well-founded and stable term orderings. Monotonicity can, then, be gradually introduced in the interpretations to deal with different applications. The first one is the generation of reduction orderings. We can also take advantage of non-fully monotonic polynomial interpretations in some remarkable cases. The dependency pairs method for proving termination of rewriting is an interesting one.