Skip to main content
SpringerLink
Log in

Proving Quadratic Derivational Complexities Using Context Dependent Interpretations

  • Conference paper
Rewriting Techniques and Applications (RTA 2008)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5117))

Included in the following conference series:

Abstract

In this paper we study context dependent interpretations, a semantic termination method extending interpretations over the natural numbers, introduced by Hofbauer. We present two subclasses of context dependent interpretations and establish tight upper bounds on the induced derivational complexities. In particular we delineate a class of interpretations that induces quadratic derivational complexity. Furthermore, we present an algorithm for mechanically proving termination of rewrite systems with context dependent interpretations. This algorithm has been implemented and we present ample numerical data for the assessment of the viability of the method.

This research is supported by FWF (Austrian Science Fund) project P20133.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Hofbauer, D., Lautemann, C.: Termination proofs and the length of derivations. In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol. 355, pp. 167–177. Springer, Heidelberg (1989)

    Google Scholar 

  2. Hofbauer, D.: Termination proofs by multiset path orderings imply primitive recursive derivation lengths. TCS 105, 129–140 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  3. Weiermann, A.: Termination proofs for term rewriting systems with lexicographic path orderings imply multiply recursive derivation lengths. TCS 139, 355–362 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  4. Moser, G.: Derivational complexity of Knuth Bendix orders revisited. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 75–89. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  5. Geser, A., Hofbauer, D., Waldmann, J., Zantema, H.: On tree automata that certify termination of left-linear term rewriting systems. IC 205, 512–534 (2007)

    MATH  MathSciNet  Google Scholar 

  6. Hirokawa, N., Moser, G.: Automated complexity analysis based on the dependency pair method. In: Proc. 4th IJCAR. Springer, Heidelberg (accepted for publication, 2008)

    Google Scholar 

  7. Hofbauer, D.: Termination proofs by context-dependent interpretations. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol. 2051, pp. 108–121. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  8. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)

    Google Scholar 

  9. Terese: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press, Cambridge (2003)

    Google Scholar 

  10. Schnabl, A.: Context Dependent Interpretations. Master’s thesis, Universität Innsbruck (2007), http://cl-informatik.uibk.ac.at/~aschnabl/

  11. Contejean, E., Marché, C., Tomás, A.P., Urbain, X.: Mechanically proving termination using polynomial interpretations. JAR 34, 325–363 (2005)

    Article  MATH  Google Scholar 

  12. Matiyasevich, Y.: Enumerable sets are diophantine. Soviet Mathematics (Dokladi) 11, 354–357 (1970)

    MATH  Google Scholar 

  13. Steinbach, J., Kühler, U.: Check your ordering - termination proofs and open problems. Technical Report SEKI-Report SR-90-25, University of Kaiserslautern (1990)

    Google Scholar 

  14. Fuhs, C., Giesl, J., Middeldorp, A., Schneider-Kamp, P., Thiemann, R., Zankl, H.: SAT solving for termination analysis with polynomial interpretations. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 340–354. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  15. Korp, M., Middeldorp, A.: Proving termination of rewrite systems using bounds. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 273–287. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  16. Hofbauer, D., Waldmann, J.: Deleting string rewriting systems preserve regularity. TCS 327, 301–317 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  17. Bonfante, G., Cichon, A., Marion, J.Y., Touzet, H.: Algorithms with polynomial interpretation termination proof. JFP 11, 33–53 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  18. Marion, J.Y.: Analysing the implicit complexity of programs. IC 183, 2–18 (2003)

    MATH  MathSciNet  Google Scholar 

  19. Bonfante, G., Marion, J.Y., Moyen, J.Y.: Quasi-intepretations and small space bounds. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 150–164. Springer, Heidelberg (2005)

    Google Scholar 

  20. Marion, J.Y., Péchoux, R.: Resource analysis by sup-interpretation. In: Hagiya, M., Wadler, P. (eds.) FLOPS 2006. LNCS, vol. 3945, pp. 163–176. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  21. Avanzini, M., Moser, G.: Complexity analysis by rewriting. In: Proc.9th FLOPS. LNCS, vol. 4989, pp. 130–146 (2008)

    Google Scholar 

  22. Caviness, B., Johnson, J. (eds.): Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer, Heidelberg (2004)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Computer Science, University of Innsbruck, Austria

    Georg Moser & Andreas Schnabl

Authors
  1. Georg Moser
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andreas Schnabl
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Moser, G., Schnabl, A. (2008). Proving Quadratic Derivational Complexities Using Context Dependent Interpretations. In: Voronkov, A. (eds) Rewriting Techniques and Applications. RTA 2008. Lecture Notes in Computer Science, vol 5117. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70590-1_19

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-70590-1_19

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-70588-8

  • Online ISBN: 978-3-540-70590-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation