Polynomials over the reals in proofs of
termination: from theory to practice
Author
Salvador Lucas
Abstract
This paper provides a framework to address termination problems
in term rewriting by using orderings induced by algebras over the reals.
The generation of such orderings is parameterized by concrete
monotonicity requirements which
are connected with different classes of termination problems:
termination of rewriting, termination of rewriting by using dependency
pairs, termination of innermost rewriting, top-termination of infinitary
rewriting, termination of context-sensitive rewriting, etc.
We show how to define term orderings based on algebraic interpretations
over the real numbers which can be used for these purposes. From a
practical point of view, we show how to automatically generate
polynomial algebras over the reals by using constraint-solving
systems to obtain the coefficients of a polynomial
in the domain of the real or rational numbers. Moreover, as a
consequence of our work, we argue that software systems which are
able to generate constraints for obtaining polynomial interpretations
over the naturals which prove termination of rewriting (e.g.,
AProVE, CiME, and TTT), are potentially able to obtain
suitable interpretations over the reals by just solving the
constraints in the domain of the real or rational numbers.
Keywords
Algebraic interpretations, polynomial orderings, term rewriting, termination.