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

RAIRO - Theoretical Informatics and Applications (2010)

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

## Access Full Article

top## Abstract

top## How to cite

topLucas, Salvador. "Polynomials over the reals in proofs of termination : from theory to practice." RAIRO - Theoretical Informatics and Applications 39.3 (2010): 547-586. <http://eudml.org/doc/92778>.

@article{Lucas2010,

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.
},

author = {Lucas, Salvador},

journal = {RAIRO - Theoretical Informatics and Applications},

keywords = {Algebraic interpretations; polynomial orderings; rewriting; termination.; term rewriting; polynomial algebras; constraint-solving systems},

language = {eng},

month = {3},

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/92778},

volume = {39},

year = {2010},

}

TY - JOUR

AU - Lucas, Salvador

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

JO - RAIRO - Theoretical Informatics and Applications

DA - 2010/3//

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, 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.

LA - eng

KW - Algebraic interpretations; polynomial orderings; rewriting; termination.; term rewriting; polynomial algebras; constraint-solving systems

UR - http://eudml.org/doc/92778

ER -

## References

top- T. Arts and J. Giesl, Termination of Term Rewriting Using Dependency Pairs. Theor. Comput. Sci.236 (2000) 133–178.
- 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).
- J. Bochnak, M. Coste and M-F. Roy, Géométrie algébraique réelle. Springer-Verlag, Berlin (1987).
- 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. LNAI2392 (2002) 314–331.
- F. Baader and T. Nipkow, Term Rewriting and All That. Cambridge University Press (1998).
- A. ben Cherifa and P. Lescanne, Termination of rewriting systems by polynomial interpretations and its implementation. Sci. Comput. Program.9 (1987) 137–160.
- 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.
- E. Contejean and C. Marché, B. Monate and X. Urbain, Proving termination of rewriting with CiME, 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 URIhttp://cime.lri.fr
- 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).
- M. Dauchet, Simulation of turing machines by a regular rewrite rule. Theor. Comput. Sci.103 (1992) 409–420.
- N. Dershowitz, A note on simplification orderings. Inform. Proc. Lett.9 (1979) 212–215.
- N. Dershowitz, Orderings for term rewriting systems. Theor. Comput. Sci.17 (1982) 279–301.
- N. Dershowitz, Termination of rewriting. J. Symbol. Comput.3 (1987) 69–115.
- N. Dershowitz, S. Kaplan and D. Plaisted, Rewrite, rewrite, rewrite, rewrite, rewrite. Theor. Comput. Sci.83 (1991) 71–96.
- M.-L. Fernández, Relaxing monotonicity for innermost termination. Inform. Proc. Lett.93 (2005) 117–123.
- J. Giesl, T. Arts and E. Ohlebusch, Modular Termination Proofs for Rewriting Using Dependency Pairs. J. Symbol. Comput.38 (2002) 21–58.
- A. Geser, Relative Termination. Ph.D. Thesis. Fakultät für Mathematik und Informatik. Universität Passau (1990).
- 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.
- 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.
- J. Giesl and A. Middeldorp, Transformation Techniques for Context-Sensitive Rewrite Systems. J. Funct. Program.14 (2004) 379–427.
- 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 URIhttp://www-i2.informatik.rwth-aachen.de/AProVE
- H. Hong and D. Jakuš, Testing Positiveness of Polynomials. J. Automated Reasoning21 (1998) 23–38.
- 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.
- 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.
- 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. LNAI3249 (2004) 185–198.
- 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 URIhttp://cl2-informatik.uibk.ac.at
- 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.
- 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.
- 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.
- D.S. Lankford, On proving term rewriting systems are noetherian. Technical Report, Louisiana Technological University, Ruston, LA (1979).
- S. Lang, Algebra. Springer-Verlag, Berlin (2004).
- S. Lucas, Context-sensitive computations in functional and functional logic programs. J. Funct. Logic Program.1998 (1998) 1–61.
- S. Lucas, Context-Sensitive Rewriting Strategies. Inform. Comput.178 (2002) 293–343.
- 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.
- 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 URIhttp://www.dsic.upv.es/~slucas/csr/termination/muterm
- S. Lucas, Proving Termination of Context-Sensitive Rewriting by Transformation. Technical Report DSIC-II/18/04, DSIC, Universidad Politécnica de Valencia (2004).
- E. Ohlebusch, Advanced Topics in Term Rewriting. Springer-Verlag, Berlin (2002).
- J.P. Rellier, CON'FLEX. INRA, France, 1996. Main URL: URIhttp://www.inra.fr/bia/T/rellier/Logiciels/conflex/welcome.html
- J. Steinbach, Generating Polynomial Orderings. Inform. Proc. Lett.49 (1994) 85–93.
- J. Steinbach, Simplification orderings: History of results. Fundamenta Informaticae24 (1995) 47–88.
- A. Tarski, A Decision Method for Elementary Algebra and Geometry. Second Edition. University of California Press, Berkeley (1951).
- 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.
- 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.
- H. Zantema, Termination, in Term Rewriting Systems, Chap. 6. edited by TeReSe, Cambridge University Press (2003).

## NotesEmbed ?

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