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.