Issue Theoret. Informatics Appl. Volume 39, Number 3, July-September 2005 Foundations of Software Science and Computer Structures (FOSSACS'04) Page(s) 547 - 586 DOI 10.1051/ita:2005029

Theoret. Informatics Appl. 39, 547-586 (2005)
DOI: 10.1051/ita:2005029

Polynomials over the reals in proofs of termination: from theory to practice

Salvador Lucas

DSIC, Universidad Politécnica de Valencia. Camino de Vera s/n, E-46022 Valencia, Spain; slucas@dsic.upv.es

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.

Mathematics Subject Classification. 12Y05.

Key words: Algebraic interpretations -- polynomial orderings -- rewriting -- termination.


© EDP Sciences 2005

What is OpenURL?