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

Salvador Lucas

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications (2005)

  • Volume: 39, Issue: 3, page 547-586
  • ISSN: 0988-3754

Abstract

top
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, C i ME, 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.

How to cite

top

Lucas, Salvador. "Polynomials over the reals in proofs of termination : from theory to practice." RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications 39.3 (2005): 547-586. <http://eudml.org/doc/245973>.

@article{Lucas2005,
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, C$i$ME, 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.},
author = {Lucas, Salvador},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications},
keywords = {algebraic interpretations; polynomial orderings; rewriting; termination; term rewriting; polynomial algebras; constraint-solving systems},
language = {eng},
number = {3},
pages = {547-586},
publisher = {EDP-Sciences},
title = {Polynomials over the reals in proofs of termination : from theory to practice},
url = {http://eudml.org/doc/245973},
volume = {39},
year = {2005},
}

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
PB - EDP-Sciences
VL - 39
IS - 3
SP - 547
EP - 586
AB - 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, C$i$ME, 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.
LA - eng
KW - algebraic interpretations; polynomial orderings; rewriting; termination; term rewriting; polynomial algebras; constraint-solving systems
UR - http://eudml.org/doc/245973
ER -

References

top
  1. [1] T. Arts and J. Giesl, Termination of Term Rewriting Using Dependency Pairs. Theor. Comput. Sci. 236 (2000) 133–178. Zbl0938.68051
  2. [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). Zbl0938.68051MR1759734
  3. [3] J. Bochnak, M. Coste and M-F. Roy, Géométrie algébraique réelle. Springer-Verlag, Berlin (1987). Zbl0633.14016MR949442
  4. [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. Zbl1072.68537
  5. [5] F. Baader and T. Nipkow, Term Rewriting and All That. Cambridge University Press (1998). Zbl0948.68098MR1629216
  6. [6] A. ben Cherifa and P. Lescanne, Termination of rewriting systems by polynomial interpretations and its implementation. Sci. Comput. Program. 9 (1987) 137–160. Zbl0625.68036
  7. [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. Zbl0925.68266
  8. [8] E. Contejean and C. Marché, B. Monate and X. Urbain, Proving termination of rewriting with C i ME, in Proc. of 6th International Workshop on Termination, WST’03, edited by A. Rubio, Technical Report DSIC II/15/03, Valencia, Spain (2003) 71–73. Available at http://cime.lri.fr 
  9. [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). Zbl1108.03017MR2270343
  10. [10] M. Dauchet, Simulation of turing machines by a regular rewrite rule. Theor. Comput. Sci. 103 (1992) 409–420. Zbl0753.68052
  11. [11] N. Dershowitz, A note on simplification orderings. Inform. Proc. Lett. 9 (1979) 212–215. Zbl0433.68044
  12. [12] N. Dershowitz, Orderings for term rewriting systems. Theor. Comput. Sci. 17 (1982) 279–301. Zbl0525.68054
  13. [13] N. Dershowitz, Termination of rewriting. J. Symbol. Comput. 3 (1987) 69–115. Zbl0637.68035
  14. [14] N. Dershowitz, S. Kaplan and D. Plaisted, Rewrite, rewrite, rewrite, rewrite, rewrite. Theor. Comput. Sci. 83 (1991) 71–96. Zbl0759.68044
  15. [15] M.-L. Fernández, Relaxing monotonicity for innermost termination. Inform. Proc. Lett. 93 (2005) 117–123. Zbl1173.68543
  16. [16] J. Giesl, T. Arts and E. Ohlebusch, Modular Termination Proofs for Rewriting Using Dependency Pairs. J. Symbol. Comput. 38 (2002) 21–58. Zbl1010.68073
  17. [17] A. Geser, Relative Termination. Ph.D. Thesis. Fakultät für Mathematik und Informatik. Universität Passau (1990). 
  18. [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. [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. [20] J. Giesl and A. Middeldorp, Transformation Techniques for Context-Sensitive Rewrite Systems. J. Funct. Program. 14 (2004) 379–427. Zbl1104.68056
  21. [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. [22] H. Hong and D. Jakuš, Testing Positiveness of Polynomials. J. Automated Reasoning 21 (1998) 23–38. Zbl0916.68084
  23. [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. [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. Zbl1187.68275
  25. [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. Zbl1109.68501
  26. [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 Zbl1078.68656
  27. [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. Zbl0981.68068
  28. [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. Zbl0188.04902
  29. [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. Zbl0953.68068
  30. [30] D.S. Lankford, On proving term rewriting systems are noetherian. Technical Report, Louisiana Technological University, Ruston, LA (1979). 
  31. [31] S. Lang, Algebra. Springer-Verlag, Berlin (2004). Zbl0984.00001
  32. [32] S. Lucas, Context-sensitive computations in functional and functional logic programs. J. Funct. Logic Program. 1998 (1998) 1–61. Zbl0924.68106
  33. [33] S. Lucas, Context-Sensitive Rewriting Strategies. Inform. Comput. 178 (2002) 293–343. Zbl1012.68095
  34. [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. Zbl1045.68074
  35. [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. [36] S. Lucas, Proving Termination of Context-Sensitive Rewriting by Transformation. Technical Report DSIC-II/18/04, DSIC, Universidad Politécnica de Valencia (2004). Zbl1171.68514
  37. [37] E. Ohlebusch, Advanced Topics in Term Rewriting. Springer-Verlag, Berlin (2002). Zbl0999.68095MR1934138
  38. [38] J.P. Rellier, CON’FLEX. INRA, France, 1996. Main URL: http://www.inra.fr/bia/T/rellier/Logiciels/conflex/welcome.html 
  39. [39] J. Steinbach, Generating Polynomial Orderings. Inform. Proc. Lett. 49 (1994) 85–93. Zbl0791.68092
  40. [40] J. Steinbach, Simplification orderings: History of results. Fundamenta Informaticae 24 (1995) 47–88. Zbl0839.68049
  41. [41] A. Tarski, A Decision Method for Elementary Algebra and Geometry. Second Edition. University of California Press, Berkeley (1951). Zbl0044.25102MR44472
  42. [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. Zbl1126.68582
  43. [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. [44] H. Zantema, Termination, in Term Rewriting Systems, Chap. 6. edited by TeReSe, Cambridge University Press (2003). Zbl1030.68053MR2007192

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.