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

Issue		RAIRO-Theor. Inf. 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?

The OpenURL standard is a protocol for transmission of metadata describing the resource that you wish to access. An OpenURL link contains article metadata and directs it to the OpenURL server of your choice. The OpenURL server can provide access to the resource and also offer complementary services (specific search engine, export of references...). The OpenURL link can be generated by different means.

If your librarian has set up your subscription with an OpenURL resolver, OpenURL links appear automatically on the abstract pages.
You can define your own OpenURL resolver with your EDPS Account. In this case your choice will be given priority over that of your library.
You can use an add-on for your browser (Firefox or I.E.) to display OpenURL links on a page (see http://www.openly.com/openurlref/). You should disable this module if you wish to use the OpenURL server that you or your library have defined.