Voir la notice de l'article provenant de la source Numdam
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, CME, 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.
@article{ITA_2005__39_3_547_0,
author = {Lucas, Salvador},
title = {Polynomials over the reals in proofs of termination : from theory to practice},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
pages = {547--586},
publisher = {EDP-Sciences},
volume = {39},
number = {3},
year = {2005},
doi = {10.1051/ita:2005029},
mrnumber = {2157047},
zbl = {1085.68076},
language = {en},
url = {http://geodesic.mathdoc.fr/articles/10.1051/ita:2005029/}
}
TY - JOUR AU - Lucas, Salvador TI - Polynomials over the reals in proofs of termination : from theory to practice JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications PY - 2005 SP - 547 EP - 586 VL - 39 IS - 3 PB - EDP-Sciences UR - http://geodesic.mathdoc.fr/articles/10.1051/ita:2005029/ DO - 10.1051/ita:2005029 LA - en ID - ITA_2005__39_3_547_0 ER -
%0 Journal Article %A Lucas, Salvador %T Polynomials over the reals in proofs of termination : from theory to practice %J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications %D 2005 %P 547-586 %V 39 %N 3 %I EDP-Sciences %U http://geodesic.mathdoc.fr/articles/10.1051/ita:2005029/ %R 10.1051/ita:2005029 %G en %F ITA_2005__39_3_547_0
Lucas, Salvador. Polynomials over the reals in proofs of termination : from theory to practice. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 39 (2005) no. 3, pp. 547-586. doi: 10.1051/ita:2005029
Cité par Sources :