Complexity of Acyclic Term Graph Rewriting

Authors Martin Avanzini, Georg Moser



PDF
Thumbnail PDF

File

LIPIcs.FSCD.2016.10.pdf
  • Filesize: 0.63 MB
  • 18 pages

Document Identifiers

Author Details

Martin Avanzini
Georg Moser

Cite AsGet BibTex

Martin Avanzini and Georg Moser. Complexity of Acyclic Term Graph Rewriting. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.FSCD.2016.10

Abstract

Term rewriting has been used as a formal model to reason about the complexity of logic, functional, and imperative programs. In contrast to term rewriting, term graph rewriting permits sharing of common sub-expressions, and consequently is able to capture more closely reasonable implementations of rule based languages. However, the automated complexity analysis of term graph rewriting has received little to no attention. With this work, we provide first steps towards overcoming this situation. We present adaptions of two prominent complexity techniques from term rewriting, viz, the interpretation method and dependency tuples. Our adaptions are non-trivial, in the sense that they can observe not only term but also graph structures, i.e. take sharing into account. In turn, the developed methods allow us to more precisely estimate the runtime complexity of programs where sharing of sub-expressions is essential.
Keywords
  • Program Analysis
  • Graph Rewriting
  • Complexity Analysis

Metrics

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

References

  1. M. Avanzini and U. Dal Lago. On Sharing, Memoization, and Polynomial Time. IC, 2015. Google Scholar
  2. M. Avanzini, U. Dal Lago, and G. Moser. Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order. In Proc. of \nth20 ICFP, pages 152-164. ACM, 2015. Google Scholar
  3. M. Avanzini, N. Eguchi, and G. Moser. A new Order-theoretic Characterisation of the Polytime Computable Functions. TCS, 585:3-24, 2015. Google Scholar
  4. M. Avanzini and G. Moser. A Combination Framework for Complexity. IC, 2015. Google Scholar
  5. M. Avanzini, G. Moser, and M. Schaper. TcT: Tyrolean Complexity Tool. In Proc. of \nnd22 TACAS, LNCS, 2016. Google Scholar
  6. M. Avanzini, C. Sternagel, and R. Thiemann. Certification of Complexity Proofs using CeTA. In Proc. of \nth26 RTA, volume 36 of LIPIcs, pages 23-39, 2015. Google Scholar
  7. E. Barendsen. Term Graph Rewriting. In Term Rewriting Systems, volume 55 of CTTCS, chapter 13, pages 712-743. Cambridge University Press, 2003. Google Scholar
  8. G. Bonfante, A. Cichon, J.-Y. Marion, and H. Touzet. Algorithms with Polynomial Interpretation Termination Proof. JFP, 11(1):33-53, 2001. Google Scholar
  9. G. Bonfante and B. Guillaume. Non-simplifying Graph Rewriting Termination. In Proc. of \nth7 TERMGRAPH, EPTCS, pages 4-16, 2013. Google Scholar
  10. G. Bonfante, J.-Y. Marion, and J.-Y. Moyen. Quasi-interpretations: A Way to Control Resources. TCS, 412(25):2776-2796, 2011. Google Scholar
  11. M. Brockschmidt, F. Emmes, S. Falke, C. Fuhs, and J. Giesl. Alternating Runtime and Size Complexity Analysis of Integer Programs. In Proc. of \nth20 TACAS, volume 8413 of LNCS, pages 140-155, 2014. Google Scholar
  12. H. J. Sander Bruggink, B. König, and H. Zantema. Termination Analysis for Graph Transformation Systems. In Proc. of \nth8 IFIP TC 1/WG 2.2, TCS, volume 8705 of LNCS, pages 179-194, 2014. Google Scholar
  13. H.J.S. Bruggink, B. König, D. Nolte, and H. Zantema. Proving Termination of Graph Transformation Systems Using Weighted Type Graphs over Semirings. In Proc. of \nth8 ICGT, volume 9151 of LNCS, pages 52-68, 2015. Google Scholar
  14. N. Dershowitz. Termination Dependencies. In Proc. of \nth6 WST, pages 28-30. Universidad Politécnica de Valencia, 2003. Technical Report DSIC-II 03. Google Scholar
  15. F. Frohn, J. Giesl, J. Hensel, C. Aschermann, and T. Ströder. Inferring Lower Bounds for Runtime Complexity. In Proc. of \nth26 RTA, LIPIcs, pages 334-349, 2015. Google Scholar
  16. J. Giesl, T. Ströder, P. Schneider-Kamp, F. Emmes, and C. Fuhs. Symbolic Evaluation Graphs and Term Rewriting: A General Methodology for Analyzing Logic Programs. In Proc. of \nth14 PPDP, pages 1-12. ACM, 2012. Google Scholar
  17. S. Gimenez and G. Moser. The Complexity of Interaction. In Proc. of \nrd43 POPL, pages 243-255. ACM, 2016. Google Scholar
  18. Y. Lafont. Interaction nets. In Proc. of \nth17 POPL, pages 95-108. ACM, 1990. Google Scholar
  19. 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, 2011. Google Scholar
  20. G. Moser. Proof Theory at Work: Complexity Analysis of Term Rewrite Systems. CoRR, abs/0907.5527, 2009. Habilitation Thesis. Google Scholar
  21. G. Moser. KBOs, Ordinals, Subrecursive Hierarchies and All That. JLC, 2014. advance access. Google Scholar
  22. G. Moser and A. Schnabl. Proving Quadratic Derivational Complexities using Context Dependent Interpretations. In Proc. of \nth19 RTA, volume 5117 of LNCS, pages 276-290, 2008. Google Scholar
  23. L. Noschinski, F. Emmes, and J. Giesl. Analyzing Innermost Runtime Complexity of Term Rewriting by Dependency Pairs. JAR, 51(1):27-56, 2013. Google Scholar
  24. M. Perrinel. On Context Semantics and Interaction Nets. In Proc. of Joint \nrd23 CSL and \nth29 LICS, page 73. ACM, 2014. Google Scholar
  25. D. Plump. Simplification orders for term graph rewriting. In Proc. 22nd MFCS, volume 1295 of LNCS, pages 458-467, 1997. Google Scholar
  26. D. Plump. Essentials of Term Graph Rewriting. ENTCS, 51:277-289, 2001. Google Scholar
  27. S. L. Peyton Jones. The Implementation of Functional Languages. Prentice-Hall International, 1987. Google Scholar
  28. M. Schaper. A Complexity Preserving Transformation from Jinja Bytecode to Rewrite Systems. Master’s thesis, University of Innsbruck, Austria, 2014. URL: http://cl-informatik.uibk.ac.at/users/c7031025/publications/masterthesis.pdf.
  29. J. Waldmann. Matrix Interpretations on Polyhedral Domains. In Proc. of \nth26 RTA, volume 36 of LIPIcs, pages 318-333, 2015. Google Scholar
  30. H. Zankl and M. Korp. Modular Complexity Analysis for Term Rewriting. LMCS, 10(1:19):1-33, 2014. 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