Document Open Access Logo

Inferring Lower Bounds for Runtime Complexity

Authors Florian Frohn, Jürgen Giesl, Jera Hensel, Cornelius Aschermann, Thomas Ströder

PDF
Thumbnail PDF

File

LIPIcs.RTA.2015.334.pdf
  • Filesize: 0.69 MB
  • 16 pages

Document Identifiers

Author Details

Florian Frohn
Jürgen Giesl
Jera Hensel
Cornelius Aschermann
Thomas Ströder

Cite As Get BibTex

Florian Frohn, Jürgen Giesl, Jera Hensel, Cornelius Aschermann, and Thomas Ströder. Inferring Lower Bounds for Runtime Complexity. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 334-349, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.RTA.2015.334

Abstract

We present the first approach to deduce lower bounds for innermost runtime complexity of term rewrite systems (TRSs) automatically. Inferring lower runtime bounds is useful to detect bugs and to complement existing techniques that compute upper complexity
bounds. The key idea of our approach is to generate suitable families of rewrite sequences of a TRS and to find a relation between the length of such a rewrite sequence and the size of the first term in the sequence. We implemented our approach in
the tool AProVE and evaluated it by extensive experiments.

Subject Classification

Keywords
  • Term Rewriting
  • Runtime Complexity
  • Lower Bounds
  • Induction

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. AProVE: URL: http://aprove.informatik.rwth-aachen.de/eval/lowerbounds/.
  2. T. Arts and J. Giesl. Termination of term rewriting using dependency pairs. Theoretical Computer Science, 236:133-178, 2000. Google Scholar
  3. M. Avanzini and G. Moser. A combination framework for complexity. In Proc. RTA '13, LIPIcs 21, pages 55-70, 2013. Google Scholar
  4. M. Avanzini and G. Moser. Tyrolean Complexity Tool: Features and usage. In Proc. RTA '13, LIPIcs 21, pages 71-80, 2013. Google Scholar
  5. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. Google Scholar
  6. L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In Proc. TACAS '08, LNCS 4963, pages 337-340, 2008. Google Scholar
  7. F. Emmes, T. Enger, and J. Giesl. Proving non-looping non-termination automatically. In Proc. IJCAR '12, LNAI 7364, pages 225-240, 2012. Google Scholar
  8. F. Frohn, J. Giesl, F. Emmes, T. Ströder, C. Aschermann, and J. Hensel. Inferring lower bounds for runtime complexity. Technical Report AIB 2015-15, RWTH Aachen, 2015. Available from [1] and from URL: http://aib.informatik.rwth-aachen.de.
  9. C. Fuhs, J. Giesl, M. Parting, P. Schneider-Kamp, S. Swiderski. Proving termination by dependency pairs and inductive theorem proving. Journal of Automated Reasoning, 47(2):133-160, 2011. Google Scholar
  10. J. Giesl, M. Raffelsieper, P. Schneider-Kamp, S. Swiderski, and R. Thiemann. Automated termination proofs for Haskell by term rewriting. ACM Transactions on Programming Languages and Systems, 33(2), 2011. Google Scholar
  11. J. Giesl, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, C. Otto, M. Plücker, P. Schneider-Kamp, T. Ströder, S. Swiderski, and R. Thiemann. Proving termination of programs automatically with AProVE. In Proc. IJCAR '14, LNAI 8562, pages 184-191, 2014. Google Scholar
  12. N. Hirokawa and G. Moser. Automated complexity analysis based on the dependency pair method. In Proc. IJCAR '08, LNAI 5195, pages 364-379, 2008. Google Scholar
  13. D. Hofbauer and C. Lautemann. Termination proofs and the length of derivations. In Proc. RTA '89, LNCS 355, pages 167-177, 1989. Google Scholar
  14. M. Hofmann and G. Moser. Amortised resource analysis and typed polynomial interpretations. In Proc. RTA-TLCA '14, LNCS 8560, pages 272-286, 2014. Google Scholar
  15. D. Knuth. Johann Faulhaber and sums of powers. Mathematics of Computation, 61(203):277-294, 1993. Google Scholar
  16. G. Moser and A. Schnabl. The derivational complexity induced by the dependency pair method. Logical Methods in Computer Science, 7(3), 2011. Google Scholar
  17. L. Noschinski, F. Emmes, and J. Giesl. Analyzing innermost runtime complexity of term rewriting by dependency pairs. Journal of Automated Reasoning, 51(1):27-56, 2013. Google Scholar
  18. C. Otto, M. Brockschmidt, C. von Essen, and J. Giesl. Automated termination analysis of Java Bytecode by term rewriting. In Proc. RTA '10, LIPIcs 6, pages 259-276, 2010. Google Scholar
  19. J. Waldmann. Matchbox: A tool for match-bounded string rewriting. In Proc. RTA '04, LNCS 3091, pages 85-94, 2004. Google Scholar
  20. J. Waldmann. Automatic termination. In Proc. RTA '09, LNCS 5595, pages 1-16, 2009. Google Scholar
  21. H. Zankl and M. Korp. Modular complexity analysis for term rewriting. Logical Methods in Computer Science, 10(1), 2014. Google Scholar
  22. H. Zantema. Termination of term rewriting: Interpretation and type elimination. Journal of Symbolic Computation, 17(1):23-50, 1994. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact