RAIRO-Theor. Inf. Appl.
Volume 39, Number 3, July-September 2005Foundations of Software Science and Computer Structures (FOSSECAS'04)
|Page(s)||547 - 586|
|Published online||15 July 2005|
Polynomials over the reals in proofs of termination : from theory to practice
DSIC, Universidad Politécnica de Valencia.
Camino de Vera s/n, E-46022 Valencia, Spain; firstname.lastname@example.org
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
Current usage metrics show cumulative count of Article Views (full-text article views including HTML views, PDF and ePub downloads, according to the available data) and Abstracts Views on Vision4Press platform.
Data correspond to usage on the plateform after 2015. The current usage metrics is available 48-96 hours after online publication and is updated daily on week days.
Initial download of the metrics may take a while.