Document Open Access Logo

Tuple Interpretations for Higher-Order Complexity

Authors Cynthia Kop , Deivid Vale

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2021.31.pdf
  • Filesize: 0.86 MB
  • 22 pages

Document Identifiers

Author Details

Cynthia Kop
  • Department of Software Science, Radboud University Nijmegen, The Netherlands
Deivid Vale
  • Department of Software Science, Radboud University Nijmegen, The Netherlands

Funding

The authors are supported by the NWO TOP project "ICHOR", NWO 612.001.803/7571 and the NWO VIDI project "CHORPE", NWO VI.Vidi.193.075.

Cite AsGet BibTex

Cynthia Kop and Deivid Vale. Tuple Interpretations for Higher-Order Complexity. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 31:1-31:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.FSCD.2021.31

Abstract

We develop a class of algebraic interpretations for many-sorted and higher-order term rewriting systems that takes type information into account. Specifically, base-type terms are mapped to tuples of natural numbers and higher-order terms to functions between those tuples. Tuples may carry information relevant to the type; for instance, a term of type nat may be associated to a pair ⟨ cost, size ⟩ representing its evaluation cost and size. This class of interpretations results in a more fine-grained notion of complexity than runtime or derivational complexity, which makes it particularly useful to obtain complexity bounds for higher-order rewriting systems. We show that rewriting systems compatible with tuple interpretations admit finite bounds on derivation height. Furthermore, we demonstrate how to mechanically construct tuple interpretations and how to orient β and η reductions within our technique. Finally, we relate our method to runtime complexity and prove that specific interpretation shapes imply certain runtime complexity bounds.

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
Keywords
  • Complexity
  • higher-order term rewriting
  • many-sorted term rewriting
  • polynomial interpretations
  • weakly monotonic algebras

Metrics

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

Related Versions

References

  1. B. Accatoli and U. Dal Lago. (leftmost-outermost) beta reduction is invariant, indeed. LMCS, 2016. URL: https://doi.org/10.2168/LMCS-12(1:4)2016.
  2. S. Alves, D. Kesner, and D. Ventura. A quantitative understanding of pattern matching. In Proc. TYPES, LIPIcs, 2020. URL: https://doi.org/10.4230/LIPIcs.TYPES.2019.3.
  3. T. Arai and G. Moser. Proofs of termination of rewrite systems for polytime functions. In Proc. FSTTCS, 2005. URL: https://doi.org/10.1007/11590156_4.
  4. T. Arts and J. Giesl. Termination of term rewriting using dependency pairs. TCS, 2000. URL: https://doi.org/10.1016/S0304-3975(99)00207-8.
  5. M. Avanzini and U. Dal Lago. Automating sized-type inference for complexity analysis. In Proc. ICFP, 2017. URL: https://doi.org/10.1145/3110287.
  6. M. Avanzini, U. Dal Lago, and G. Moser. Analysing the complexity of functional programs: Higher-order meets first-order. In Proc. ICFP, 2015. URL: https://doi.org/10.1145/2784731.2784753.
  7. M. Avanzini and G. Moser. Complexity analysis by rewriting. In Proc. FLOPS, 2008. URL: https://doi.org/10.1007/978-3-540-78969-7_11.
  8. M. Avanzini and G. Moser. Closing the gap between runtime complexity and polytime computability. In Proc. RTA, 2010. URL: https://doi.org/10.4230/LIPIcs.RTA.2010.33.
  9. Ralph B. Automated higher-order complexity analysis. TCS, 2004. URL: https://doi.org/10.1016/j.tcs.2003.10.022.
  10. P. Baillot and U. Dal Lago. Higher-order interpretations and program complexity. IC, 2016. URL: https://doi.org/10.1016/j.ic.2015.12.008.
  11. G. Bonfante, A. Cichon, J. Marion, and H. Touzet. Complexity classes and rewrite systems with polynomial interpretation. In Proc. CSL, 1998. URL: https://doi.org/10.1007/10703163_25.
  12. G. Bonfante, J. Marion, and J. Moyen. On lexicographic termination ordering with space bound certifications. In Proc. PSI, 2001. URL: https://doi.org/10.1007/3-540-45575-2_46.
  13. M. Brockschmidt, F. Emmes, S. Falke, C. Fuhs, and J. Giesl. Alternating runtime and size complexity analysis of integer programs. In Proc. TACAS, 2014. URL: https://doi.org/10.1007/978-3-642-54862-8_10.
  14. Q. Carbonneaux, J. Hoffmann, T. Ramananandro, and Z. Shao. End-to-end verification of stack-space bounds for C programs. SIGPLAN Not., 2014. URL: https://doi.org/10.1145/2666356.2594301.
  15. E. Çiçek, D. Garg, and U. Acar. Refinement types for incremental computational complexity. In Proc. ESOP, 2015. URL: https://doi.org/10.1007/978-3-662-46669-8_17.
  16. Community. Termination problem database, version 11.0. Directory Higher_Order_ Rewriting_Union_Beta/Mixed_HO_10/, 2019. URL: http://termination-portal.org/wiki/TPDB.
  17. U. Dal Lago and M. Gaboardi. Linear dependent types and relative completeness. In Proc. LICS, 2011. URL: https://doi.org/10.1109/LICS.2011.22.
  18. U. Dal Lago and S. Martini. Derivational complexity is an invariant cost model. In Proc. FOPARA, 2010. URL: https://doi.org/10.1007/978-3-642-15331-0_7.
  19. N. Danner, D.R. Licata, and R. Ramyaa. Denotational cost semantics for functional languages with inductive types. In Proc. ICFP, 2015. URL: https://doi.org/10.1145/2784731.2784749.
  20. A. Das, S. Balzer, J. Hoffman, F. Pfenning, and I. Santurkar. Resource-aware session types for digital contracts, 2019. URL: http://arxiv.org/abs/1902.06056.
  21. J. Endrullis, J. Waldmann, and H. Zantema. Matrix interpretations for proving termination of term rewriting. JAR, 2008. URL: https://doi.org/10.1007/11814771_47.
  22. C. Fuhs and C. Kop. Polynomial interpretations for higher-order rewriting. In Proc. RTA, 2012. URL: https://doi.org/10.4230/LIPIcs.RTA.2012.176.
  23. M. A. T. Handley, N. Vazou, and G. Hutton. Liquidate your assets: Reasoning about resource usage in liquid haskell. ACM POPL, 2019. URL: https://doi.org/10.1145/3371092.
  24. N. Hirokawa and G. Moser. Automated complexity analysis based on the dependency pair method. In Proc. IJCAR, 2008. URL: https://doi.org/10.1007/978-3-540-71070-7_32.
  25. D. Hofbauer. Termination proofs by multiset path orderings imply primitive recursive derivation lengths. TCS, 1992. URL: https://doi.org/10.1007/3-540-53162-9_50.
  26. D. Hofbauer. Termination proofs by context-dependent interpretations. In Proc. RTA, 2001. URL: https://doi.org/10.1007/3-540-45127-7_10.
  27. D. Hofbauer and C. Lautemann. Termination proofs and the length of derivations. In Proc. RTA, 1989. URL: https://doi.org/10.1007/3-540-51081-8_107.
  28. J. Hoffmann, K. Aehlig, and M. Hofmann. Resource aware ml. In Proc. CAV, 2012. URL: https://doi.org/10.1007/978-3-642-31424-7_64.
  29. J. Jouannaud and M. Okada. A computation model for executable higher-order algebraic specification languages. In Proc. LICS, 1991. URL: https://doi.org/10.1109/LICS.1991.151659.
  30. D. M. Kahn and J. Hoffmann. Exponential automatic amortized resource analysis. In Proc. FoSSaCS, 2020. URL: https://doi.org/10.1007/978-3-030-45231-5_19.
  31. C. Kop, A. Middeldorp, and T. Sternagel. Complexity of conditional term rewriting. LMCS, 2017. URL: https://doi.org/10.23638/LMCS-13(1:6)2017.
  32. C. Kop and D. Vale. Tuple interpretations for higher-order complexity (extended), 2021. URL: http://arxiv.org/abs/2105.01112.
  33. K. Kusakari and M. Sakai. Enhancing dependency pair method using strong computability in simply-typed term rewriting. AAECC, 2007. URL: https://doi.org/10.1007/s00200-007-0046-9.
  34. G. Moser. Derivational complexity of knuth-bendix orders revisited. In Proc. LPAR, 2006. URL: https://doi.org/10.1007/11916277_6.
  35. G. Moser, A. Schnabl, and J. Waldmann. Complexity analysis of term rewriting based on matrix and context dependent interpretations. In Proc. FSTTCS, 2008. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2008.1762.
  36. T. Nipkow. Higher-order critical pairs. In Proc. LICS, 1991. URL: https://doi.org/10.1109/LICS.1991.151658.
  37. Y. Niu and J. Hoffmann. Automatic space bound analysis for functional programs with garbage collection. In Proc. LPAR, 2018. URL: https://doi.org/10.29007/xkwx.
  38. E. Ohlebusch. Advanced Topics in Term Rewriting. Springer, 2002. URL: https://doi.org/10.1007/978-1-4757-3661-8.
  39. J.C. van de Pol. Termination of Higher-order Rewrite Systems. PhD thesis, University of Utrecht, 1996. URL: https://www.cs.au.dk/~jaco/papers/thesis.pdf.
  40. V. Rajani, M. Gaboardi, D. Garg, and J. Hoffmann. A unifying type-theory for higher-order (amortized) cost analysis. ACM POPL, 2021. URL: https://doi.org/10.1145/3434308.
  41. P. M. Rondon, M. Kawaguci, and R. Jhala. Liquid types. SIGPLAN Not., 2008. URL: https://doi.org/10.1145/1379022.1375602.
  42. M. Sinn, F. Zuleger, and H. Veith. A simple and scalable static analysis for bound analysis and amortized complexity analysis. In Proc. CAV, 2014. URL: https://doi.org/10.1007/978-3-319-08867-9_50.
  43. R. E. Tarjan. Amortized computational complexity. ADM, 1985. URL: https://doi.org/10.1137/0606031.
  44. N. Vazou, P. M. Rondon, and R. Jhala. Abstract refinement types. In Proc. ESOP, 2013. URL: https://doi.org/10.1007/978-3-642-37036-6_13.
  45. P. Wang, D. Wang, and A. Chlipala. Timl: A functional language for practical complexity analysis with invariants. ACM POPL, 2017. URL: https://doi.org/10.1145/3133903.
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 Imprint Privacy Contact