Practical use of polynomials over the reals in
proofs of termination
Author
Salvador Lucas
Abstract
Nowadays, polynomial interpretations are an essential ingredient
in the development of tools for proving termination.
We have recently proven that polynomial interpretations over
the reals are strictly better for proving polynomial termination of
rewriting than those which only use integer coefficients.
Some essential aspects of their practical use, though, remain
unexplored or underdeveloped.
In this paper, we compare the two current frameworks for using
polynomial intepretations over the reals and show that one of
them is strictly better than the other, thus making a suitable choice
for implementations.
We also prove that the use of algebraic real coefficients in the
interpretations suffice for termination proofs.
We also discuss the use of algorithms and techniques from Tarski's
first-order logic of the real closed fields for implementing
their use in proofs of termination.
We argue that more standard constraint-solving techniques are
better suited for this.
We propose an algorithm to solve the polynomial constraints which
arise when specific finite subsets of rational (or even algebraic real) numbers are
considered for giving value to the coefficients.
We provide a preliminary experimental evaluation of the algorithm
which has been implemented as part of the termination tool \muterm.
Keywords
Polynomial orderings, program analysis, term rewriting, termination.