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.

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.

DOI : https://doi.org/10.1051/ita:2005029
Classification : 12Y05
Mots clés : algebraic interpretations, polynomial orderings, rewriting, termination
@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},
     zbl = {1085.68076},
     mrnumber = {2157047},
     language = {en},
     url = {http://www.numdam.org/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
DA  - 2005///
SP  - 547
EP  - 586
VL  - 39
IS  - 3
PB  - EDP-Sciences
UR  - http://www.numdam.org/articles/10.1051/ita:2005029/
UR  - https://zbmath.org/?q=an%3A1085.68076
UR  - https://www.ams.org/mathscinet-getitem?mr=2157047
UR  - https://doi.org/10.1051/ita:2005029
DO  - 10.1051/ita:2005029
LA  - en
ID  - ITA_2005__39_3_547_0
ER  - 
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. http://www.numdam.org/articles/10.1051/ita:2005029/

[1] T. Arts and J. Giesl, Termination of Term Rewriting Using Dependency Pairs. Theor. Comput. Sci. 236 (2000) 133-178. | Zbl 0938.68051

[2] T. Arts and J. Giesl, A collection of examples for termination of term rewriting using dependency pairs. Technical report, AIB-2001-09, RWTH Aachen, Germany (2001). | MR 1759734

[3] J. Bochnak, M. Coste and M-F. Roy, Géométrie algébraique réelle. Springer-Verlag, Berlin (1987). | MR 949442 | Zbl 0633.14016

[4] C. Borralleras, S. Lucas and A. Rubio, Recursive Path Orderings can be Context-Sensitive, in Proc. of 18th International Conference on Automated Deduction, CADE'02, edited by A. Voronkov, Springer-Verlag, Berlin. LNAI 2392 (2002) 314-331. | Zbl 1072.68537

[5] F. Baader and T. Nipkow, Term Rewriting and All That. Cambridge University Press (1998). | MR 1629216 | Zbl 0948.68098

[6] A. ben Cherifa and P. Lescanne, Termination of rewriting systems by polynomial interpretations and its implementation. Sci. Comput. Program. 9 (1987) 137-160. | Zbl 0625.68036

[7] A. Cichon and P. Lescanne, Polynomial interpretations and the complexity of algorithms, in Proc. of 11th International Conference on Automated Deduction, CADE'92, edited by D. Kapur, Springer-Verlag, Berlin. LNAI 607 (1992) 139-147. | Zbl 0925.68266

[8] E. Contejean and C. Marché, B2003) 71-73. Available at http://cime.lri.fr

[9] E. Contejean, C. Marché, A.-P. Tomás and X. Urbain, Mechanically proving termination using polynomial interpretations. Research Report 1382, LRI, Université de Paris-Sud (2004). | MR 2270343 | Zbl 1108.03017

[10] M. Dauchet, Simulation of turing machines by a regular rewrite rule. Theor. Comput. Sci. 103 (1992) 409-420. | Zbl 0753.68052

[11] N. Dershowitz, A note on simplification orderings. Inform. Proc. Lett. 9 (1979) 212-215. | Zbl 0433.68044

[12] N. Dershowitz, Orderings for term rewriting systems. Theor. Comput. Sci. 17 (1982) 279-301. | Zbl 0525.68054

[13] N. Dershowitz, Termination of rewriting. J. Symbol. Comput. 3 (1987) 69-115. | Zbl 0637.68035

[14] N. Dershowitz, S. Kaplan and D. Plaisted, Rewrite, rewrite, rewrite, rewrite, rewrite. Theor. Comput. Sci. 83 (1991) 71-96. | Zbl 0759.68044

[15] M.-L. Fernández, Relaxing monotonicity for innermost termination. Inform. Proc. Lett. 93 (2005) 117-123.

[16] J. Giesl, T. Arts and E. Ohlebusch, Modular Termination Proofs for Rewriting Using Dependency Pairs. J. Symbol. Comput. 38 (2002) 21-58. | Zbl 1010.68073

[17] A. Geser, Relative Termination. Ph.D. Thesis. Fakultät für Mathematik und Informatik. Universität Passau (1990).

[18] J. Giesl, Generating Polynomial Orderings for Termination Proofs, in Proc. of 6th International Conference on Rewriting Techniques and Applications, RTA'95, edited by J. Hsiang, Springer-Verlag, Berlin. Lect. Notes Comput. Sci. 914 (1995) 426-431.

[19] B. Gramlich and S. Lucas, Simple termination of context-sensitive rewriting, in Proc. of 3rd ACM SIGPLAN Workshop on Rule-based Programming, RULE'02 ACM Press, New York (2002) 29-41.

[20] J. Giesl and A. Middeldorp, Transformation Techniques for Context-Sensitive Rewrite Systems. J. Funct. Program. 14 (2004) 379-427. | Zbl 1104.68056

[21] J. Giesl, R. Thiemann, P. Schneider-Kamp and S. Falke, Automated Termination Proofs with AProVE, in Proc. of 15h International Conference on Rewriting Techniques and Applications, RTA'04, edited by V. van Oostrom, Springer-Verlag, Berlin. Lect. Notes. Comput. Sci. 3091 (2004) 210-220. Available at http://www-i2.informatik.rwth-aachen.de/AProVE

[22] H. Hong and D. Jakuš, Testing Positiveness of Polynomials. J. Automated Reasoning 21 (1998) 23-38. | Zbl 0916.68084

[23] D. Hofbauer and C. Lautemann, Termination proofs and the length of derivations, in Proc. of the 3rd International Conference on Rewriting Techniques and Applications, RTA'89, edited by N. Dershowitz, Springer-Verlag, Berlin. Lect. Notes Comput. Sci. 355 (1989) 167-177.

[24] N. Hirokawa and A. Middeldorp, Dependency Pairs Revisited, in Proc. of 15h International Conference on Rewriting Techniques and Applications, RTA'04, edited by V. van Oostrom, Springer-Verlag, Berlin. Lect. Notes. Comput. Sci. 3091 (2004) 249-268.

[25] N. Hirokawa and A. Middeldorp, Polynomial Interpretations with Negative Coefficients, in Proc. of the 7th International Conference on Artificial Intelligence and Symbolic Computation, AISC'04, edited by B. Buchberger and J.A. Campbell, Springer-Verlag, Berlin. LNAI 3249 (2004) 185-198. | Zbl 1109.68501

[26] N. Hirokawa and A. Middeldorp, Tyrolean Termination Tool, in Proc. of 16th International Conference on Rewriting Techniques and Applications, RTA'05, edited by J. Giesl. Lect. Notes. Comput. Sci., to appear (2005). Available at http://cl2-informatik.uibk.ac.at | Zbl 1078.68656

[27] D. Hofbauer, Termination Proofs by Context-Dependent Interpretations, in Proc. of 12th International Conference on Rewriting Techniques and Applications, RTA'01, edited by A. Middeldorp, Springer-Verlag, Berlin. Lect. Notes Comput. Sci. 2051 (2001) 108-121. | Zbl 0981.68068

[28] D.E. Knuth and P.E. Bendix, Simple Word Problems in Universal Algebra, in Computational Problems in Abstract Algebra, edited by J. Leech, Pergamon Press (1970) 263-297. | Zbl 0188.04902

[29] K. Kusakari, M. Nakamura and Y. Toyama, Argument Filtering Transformation, in International Conference on Principles and Practice of Declarative Programming, PPDP'99, edited by G. Nadathur, Springer-Verlag, Berlin. Lect. Notes Comput. Sci. 1702 (1999) 47-61. | Zbl 0953.68068

[30] D.S. Lankford, On proving term rewriting systems are noetherian. Technical Report, Louisiana Technological University, Ruston, LA (1979).

[31] S. Lang, Algebra. Springer-Verlag, Berlin (2004). | Zbl 0984.00001

[32] S. Lucas, Context-sensitive computations in functional and functional logic programs. J. Funct. Logic Program. 1998 (1998) 1-61. | Zbl 0924.68106

[33] S. Lucas, Context-Sensitive Rewriting Strategies. Inform. Comput. 178 (2002) 293-343. | Zbl 1012.68095

[34] S. Lucas, Termination of (Canonical) Context-Sensitive Rewriting, in Proc. 13th International Conference on Rewriting Techniques and Applications, RTA'02, edited by S. Tison, Springer-Verlag, Berlin. Lect. Notes Comput. Sci. 2378 (2002) 296-310. | Zbl 1045.68074

[35] S. Lucas, MU-TERM: A Tool for Proving Termination of Context-Sensitive Rewriting, in Proc. of 15h International Conference on Rewriting Techniques and Applications, RTA'04, edited by V. van Oostrom, Springer-Verlag, Berlin. Lect. Notes Comput. Sci. 3091 (2004) 200-209. Available at http://www.dsic.upv.es/~slucas/csr/termination/muterm

[36] S. Lucas, Proving Termination of Context-Sensitive Rewriting by Transformation. Technical Report DSIC-II/18/04, DSIC, Universidad Politécnica de Valencia (2004).

[37] E. Ohlebusch, Advanced Topics in Term Rewriting. Springer-Verlag, Berlin (2002). | MR 1934138 | Zbl 0999.68095

[38] J.P. Rellier, CON'FLEX. INRA, France, 1996. Main URL: http://www.inra.fr/bia/T/rellier/Logiciels/conflex/welcome.html

[39] J. Steinbach, Generating Polynomial Orderings. Inform. Proc. Lett. 49 (1994) 85-93. | Zbl 0791.68092

[40] J. Steinbach, Simplification orderings: History of results. Fundamenta Informaticae 24 (1995) 47-88. | Zbl 0839.68049

[41] A. Tarski, A Decision Method for Elementary Algebra and Geometry. Second Edition. University of California Press, Berkeley (1951). | MR 44472 | Zbl 0044.25102

[42] R. Thiemann, J. Giesl and P. Schneider-Kamp, Improved Modular Termination Proofs Using Dependency Pairs, in Proc. of 2nd International Joint Conference on Automated Reasoning, IJCAR'04, edited by D.A. Basin and M. Rusinowitch, Springer-Verlag, Berlin. Lect. Notes Comput. Sci. 3097 (2004) 75-90. | Zbl 1126.68582

[43] H. Zantema, Termination of Context-Sensitive Rewriting, in Proc. of 8th International Conference on Rewriting Techniques and Applications, RTA'97, edited by H. Comon, Springer-Verlag, Berlin. Lect. Notes Comput. Sci. 1232 (1997) 172-186.

[44] H. Zantema, Termination, in Term Rewriting Systems, Chap. 6. edited by TeReSe, Cambridge University Press (2003). | MR 2007192

Cité par Sources :