Skip to main content
SpringerLink
Log in
Book cover

International Conference on Automated Deduction

CADE 2011: Automated Deduction – CADE-23 pp 422–438Cite as

A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 6803))

Abstract

We present a modular framework to analyze the innermost runtime complexity of term rewrite systems automatically. Our method is based on the dependency pair framework for termination analysis. In contrast to previous work, we developed a direct adaptation of successful termination techniques from the dependency pair framework in order to use them for complexity analysis. By extensive experimental results, we demonstrate the power of our method compared to existing techniques.

Supported by the DFG grant GI 274/5-3.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science 236, 133–178 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  2. Avanzini, M., Moser, G., Schnabl, A.: Automated Implicit Computational Complexity Analysis (System Description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 132–138. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  3. Avanzini, M., Moser, G.: Dependency Pairs and Polynomial Path Orders. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 48–62. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  4. Avanzini, M., Moser, G.: Closing the gap between runtime complexity and polytime computability. In: Proc. RTA 2010. LIPIcs, vol. 6, pp. 33–48 (2010)

    Google Scholar 

  5. Avanzini, M., Moser, G.: Complexity Analysis by Graph Rewriting. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol. 6009, pp. 257–271. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  6. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge U. Pr., Cambridge (1998)

    Book  MATH  Google Scholar 

  7. Bonfante, G., Cichon, A., Marion, J.-Y., Touzet, H.: Algorithms with polynomial interpretation termination proof. J. Functional Programming 11(1), 33–53 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  8. Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. J. Automated Reasoning 40(2-3), 195–220 (2008)

    Article  MATH  MathSciNet  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  10. Giesl, J., Thiemann, R., Schneider-Kamp, P.: The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol. 3452, pp. 301–331. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  11. Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. Journal of Automated Reasoning 37(3), 155–203 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  12. Giesl, J., Raffelsieper, M., Schneider-Kamp, P., Swiderski, S., Thiemann, R.: Automated termination proofs for Haskell by term rewriting. ACM Transactions on Programming Languages and Systems 33(2) (2011)

    Google Scholar 

  13. Givan, R., McAllester, D.A.: Polynomial-time computation via local inference relations. ACM Transactions on Computational Logic 3(4), 521–541 (2002)

    Article  MathSciNet  Google Scholar 

  14. Hirokawa, N., Middeldorp, A.: Automating the dependency pair method. Information and Computation 199(1,2), 172–199 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  15. Hirokawa, N., Moser, G.: Automated Complexity Analysis Based on the Dependency Pair Method. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 364–379. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  16. Hirokawa, N., Moser, G.: Complexity, Graphs, and the Dependency Pair Method. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 652–666. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  17. 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)

    Chapter  Google Scholar 

  18. Hofmann, M.: Linear types and non-size-increasing polynomial time computation. In: Proc. LICS 1999, pp. 464–473. IEEE Press, Los Alamitos (1999)

    Google Scholar 

  19. Koprowski, A., Waldmann, J.: Max/plus tree automata for termination of term rewriting. Acta Cybernetica 19(2), 357–392 (2009)

    MATH  MathSciNet  Google Scholar 

  20. Marion, J.-Y., Péchoux, R.: Characterizations of polynomial complexity classes with a better intensionality. In: Proc. PPDP 2008, pp. 79–88. ACM Press, New York (2008)

    Google Scholar 

  21. Moser, G., Schnabl, A., Waldmann, J.: Complexity analysis of term rewriting based on matrix and context dependent interpretations. In: Proc. FSTTCS 2008. LIPIcs, vol. 2, pp. 304–315 (2008)

    Google Scholar 

  22. Moser, G.: Personal communication (2010)

    Google Scholar 

  23. Neurauter, F., Zankl, H., Middeldorp, A.: Revisiting Matrix Interpretations for Polynomial Derivational Complexity of Term Rewriting. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 550–564. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  24. Noschinski, L., Emmes, F., Giesl, J.: A dependency pair framework for innermost complexity analysis of term rewrite systems. Technical Report AIB-2011-03, RWTH Aachen (2011), http://aib.informatik.rwth-aachen.de

  25. Otto, C., Brockschmidt, M., von Essen, C., Giesl, J.: Automated termination analysis of Java Bytecode by term rewriting. In: Proc. RTA 2010. LIPIcs, vol. 6, pp. 259–276 (2010)

    Google Scholar 

  26. Schneider-Kamp, P., Giesl, J., Ströder, T., Serebrenik, A., Thiemann, R.: Automated termination analysis for logic programs with cut. In: Proc. ICLP 2010, Theory and Practice of Logic Programming, vol.10(4-6), pp. 365–381 (2010)

    Google Scholar 

  27. Waldmann, J.: Polynomially bounded matrix interpretations. In: Proc. RTA 2010. LIPIcs, vol. 6, pp. 357–372 (2010)

    Google Scholar 

  28. Zankl, H., Korp, M.: Modular complexity analysis via relative complexity. In: Proc. RTA 2010. LIPIcs, vol. 6, pp. 385–400 (2010)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, TU Munich, Germany

    Lars Noschinski

  2. LuFG Informatik 2, RWTH Aachen University, Germany

    Fabian Emmes & Jürgen Giesl

Authors
  1. Lars Noschinski
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Fabian Emmes
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jürgen Giesl
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Microsoft Research, One Microsoft Way, 98052-6399, Redmond, WA, USA

    Nikolaj Bjørner

  2. Max-Planck-Institut für Informatik, Campus E 1.4, 66123, Saarbrücken, Germany

    Viorica Sofronie-Stokkermans

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Noschinski, L., Emmes, F., Giesl, J. (2011). A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems. In: Bjørner, N., Sofronie-Stokkermans, V. (eds) Automated Deduction – CADE-23. CADE 2011. Lecture Notes in Computer Science(), vol 6803. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22438-6_32

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-22438-6_32

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-22437-9

  • Online ISBN: 978-3-642-22438-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation