Document Open Access Logo

A Combination Framework for Complexity

Authors Martin Avanzini, Georg Moser

PDF

File

Thumbnail PDF
PDF
LIPIcs.RTA.2013.55.pdf
  • Filesize: 0.68 MB
  • 16 pages

Document Identifiers

Subject Classification

Keywords
  • program analysis
  • term rewriting
  • complexity analysis
  • automation

Metrics

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

Abstract

In this paper we present a combination framework for the automated polynomial complexity analysis of term rewrite systems. The framework covers both derivational and runtime complexity analysis, and is employed as theoretical foundation in the automated complexity tool TCT. We present generalisations of powerful complexity techniques, notably a generalisation of complexity pairs and (weak) dependency pairs. Finally, we also present a novel technique, called dependency graph decomposition, that in the dependency pair setting greatly increases modularity.

Cite As Get BibTex

Martin Avanzini and Georg Moser. A Combination Framework for Complexity. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 55-70, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013) https://doi.org/10.4230/LIPIcs.RTA.2013.55

Author Details

Martin Avanzini
Georg Moser

References

  1. T. Arts and J. Giesl. Termination of Term Rewriting using Dependency Pairs. TCS, 236(1-2):133-178, 2000. Google Scholar
  2. M. Avanzini. POP* and Semantic Labeling using SAT. In Proc. of ESSLLI 2008/2009 Student Session, volume 6211 of LNCS, pages 155-166. Springer, 2010. Google Scholar
  3. M. Avanzini, N. Eguchi, and G. Moser. New Order-theoretic Characterisation of the Polytime Computable Functions. 2012. Submitted to TCS. Google Scholar
  4. M. Avanzini and G. Moser. Closing the Gap Between Runtime Complexity and Polytime Computability. In Proc. of \nst21 RTA, volume 6 of LIPIcs, pages 33-48, 2010. Google Scholar
  5. M. Avanzini and G. Moser. Polynomial Path Orders: A Maximal Model. 2012. Submitted to LMCS. Technical Report available at URL: http://arxiv.org/abs/1209.3793.
  6. M. Avanzini and G. Moser. A Combination Framework for Complexity, Technical Report. CoRR, cs/CC/1302.0973, 2013. Available at URL: http://www.arxiv.org/abs/1302.0973.
  7. M. Avanzini and G. Moser. Tyrolean Complexity Tool: Features and Usage. In Proc. of \nth24 RTA. LIPIcs, 2013. Google Scholar
  8. F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. Google Scholar
  9. G. Bonfante, A. Cichon, J.-Y. Marion, and H. Touzet. Algorithms with Polynomial Interpretation Termination Proof. JFP, 11(1):33-53, 2001. Google Scholar
  10. U. Dal Lago and S. Martini. On Constructor Rewrite Systems and the Lambda-Calculus. In Proc. of \nth36 ICALP, volume 5556 of LNCS, pages 163-174. Springer, 2009. Google Scholar
  11. J. Giesl, T. Arts, and E. Ohlebusch. Modular Termination Proofs for Rewriting Using Dependency Pairs. JSC, 34:21-58, 2002. Google Scholar
  12. N. Hirokawa and G. Moser. Automated Complexity Analysis Based on the Dependency Pair Method. In Proc. of \nth4 IJCAR, volume 5195 of LNAI, pages 364-380, 2008. Google Scholar
  13. N. Hirokawa and G. Moser. Complexity, Graphs, and the Dependency Pair Method. In Proc. of \nth15 LPAR, pages 652-666, 2008. Google Scholar
  14. N. Hirokawa and G. Moser. Automated Complexity Analysis Based on the Dependency Pair Method. 2012. Submitted to IC, available at URL: http://arxiv.org/abs/1102.3129.
  15. D. Hofbauer and C. Lautemann. Termination Proofs and the Length of Derivations. In Proc. of \nrd3 RTA, volume 355 of LNCS, pages 167-177. Springer, 1989. Google Scholar
  16. D. Hofbauer and J. Waldmann. Termination of String Rewriting with Matrix Interpretations. In Proc. of \nth17 RTA, volume 4098 of LNCS, pages 328-342. Springer, 2011. Google Scholar
  17. S. Lucas. Fundamentals of Context-Sensitive Rewriting. In Proc. of \nth22 SOFSEM, LNCS, pages 405 - 412. Springer, 1995. Google Scholar
  18. A. Middeldorp, G. Moser, F. Neurauter, J. Waldmann, and H. Zankl. Joint Spectral Radius Theory for Automated Complexity Analysis of Rewrite Systems. In Proc. of \nth4 CAI, volume 6742 of LNCS, pages 1-20. Springer, 2011. Google Scholar
  19. G. Moser. Proof Theory at Work: Complexity Analysis of Term Rewrite Systems. CoRR, abs/0907.5527, 2009. Habilitation Thesis. Google Scholar
  20. G. Moser, A. Schnabl, and J. Waldmann. Complexity Analysis of Term Rewriting Based on Matrix and Context Dependent Interpretations. In Proc. of the 28th FSTTCS, LIPIcs, pages 304-315, 2008. Google Scholar
  21. L. Noschinski, F. Emmes, and J. Giesl. A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems. In Proc. of \nrd23 CADE, LNAI, pages 422-438. Springer, 2011. Google Scholar
  22. A. Schnabl. Derivational Complexity Analysis Revisited. PhD thesis, University of Innsbruck, 2012. Available at http://cl-informatik.uibk.ac.at/research/.
  23. R. Thiemann. The DP Framework for Proving Termination of Term Rewriting. PhD thesis, University of Aachen, 2007. Available as Technical Report AIB-2007-17. Google Scholar
  24. H. Zankl and M. Korp. Modular Complexity Analysis via Relative Complexity. In Proc. of \nst21 RTA, volume 6 of LIPIcs, pages 385-400, 2010. Google Scholar
  25. H. Zantema. Termination of Context-Sensitive Rewriting. In Proc. of \nth8 RTA, volume 1232 of LNCS, pages 172-186. Springer, 1997. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact