Document Open Access Logo

Cost-Size Semantics for Call-By-Value Higher-Order Rewriting

Authors Cynthia Kop , Deivid Vale

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2023.15.pdf
  • Filesize: 0.84 MB
  • 19 pages

Document Identifiers

Author Details

Cynthia Kop
  • Institute for Computing and Information Sciences, Radboud University, Nijmegen, The Netherlands
Deivid Vale
  • Institute for Computing and Information Sciences, Radboud University, Nijmegen, The Netherlands

Funding

This work is supported by the NWO TOP project "Implicit Complexity through Higher-Order Rewriting", NWO 612.001.803/7571 and the NWO VIDI project "Constrained Higher-Order Rewriting and Program Equivalence", NWO VI.Vidi.193.075.

Cite AsGet BibTex

Cynthia Kop and Deivid Vale. Cost-Size Semantics for Call-By-Value Higher-Order Rewriting. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 15:1-15:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.FSCD.2023.15

Abstract

Higher-order rewriting is a framework in which higher-order programs can be described by transformation rules on expressions. A computation occurs by transforming an expression into another using such rules. This step-by-step computation model induced by rewriting naturally gives rise to a notion of complexity as the number of steps needed to reduce expressions to a normal form, i.e., an expression that cannot be reduced further. The study of complexity analysis focuses on the development of automatable techniques to provide bounds to this number. In this paper, we consider a form of higher-order rewriting with a call-by-value evaluation strategy, so as to model call-by-value programs. We provide a cost-size semantics: a class of algebraic interpretations to map terms to tuples which bound both the reduction cost and the size of normal forms.

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
Keywords
  • Call-by-Value Evaluation
  • Complexity Theory
  • Higher-Order Rewriting

Metrics

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

References

  1. 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.
  2. M. Avanzini and U. Dal Lago. Automating sized-type inference for complexity analysis. In Proc. ICFP, 2017. URL: https://doi.org/10.1145/3110287.
  3. 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.
  4. 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.
  5. H. Barendregt, W. Dekkers, and R. Statman. Lambda Calculus with Types. Perspectives in Logic. Cambridge University Press, 2013. URL: https://doi.org/10.1017/CBO9781139032636.
  6. A. Ben Cherifa and P. Lescanne. Termination of rewriting systems by polynomial interpretations and its implementation. Science of Computer Programming, 9(2):137-159, 1987. URL: https://doi.org/10.1016/0167-6423(87)90030-X.
  7. G. Bonfante, A. Cichon, J.-Y. Marion, and H. Touzet. Algorithms with polynomial interpretation termination proof. Journal of Functional Programming, 11(1):33-53, 2001. URL: https://doi.org/10.1017/S0956796800003877.
  8. 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.
  9. A. Cichon and P. Lescanne. Polynomial interpretations and the complexity of algorithms. In CADE, pages 139-147, 1992. URL: https://doi.org/10.1007/3-540-55602-8_161.
  10. M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Marti-Oliet, J. Meseguer, and J.F. Quesada. Maude: specification and programming in rewriting logic. Theoretical Computer Science, 285(2):187-243, 2002. Rewriting Logic and its Applications. URL: https://doi.org/10.1016/S0304-3975(01)00359-0.
  11. M. Codish, I. Gonopolskiy, A. M. Ben-Amram, C. Fuhs, and J. Giesl. Sat-based termination analysis using monotonicity constraints over the integers. Theory and Practice of Logic Programming, 11(4-5):503-520, 2011. URL: https://doi.org/https://doi.org10.1017/S1471068411000147.
  12. E. Contejan, C. Marché, A. P. Tomás, and X. Urbain. Mechanically proving termination using polynomial interpretations. JAR, 34, 2005. URL: https://doi.org/10.1007/s10817-005-9022-x.
  13. 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.
  14. 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.
  15. Jürgen Giesl, Christoph Walther, and Jürgen Brauburger. Termination analysis for functional programs. In Wolfgang Bibel and Peter H. Schmitt, editors, Automated Deduction - A Basis for Applications: Volume III Applications, pages 135-164. Springer Netherlands, Dordrecht, 1998. URL: https://doi.org/10.1007/978-94-017-0437-3_6.
  16. 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.
  17. 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.
  18. D. Hofbauer. Termination proofs by context-dependent interpretations. In Proc. RTA, 2001. URL: https://doi.org/10.1007/3-540-45127-7_10.
  19. 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.
  20. 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.
  21. C. Kop and D. Vale. Tuple interpretations for higher-order complexity. In Proc. FSCD, 2021. URL: https://doi.org/10.4230/LIPIcs.FSCD.2021.31.
  22. Cynthia Kop. Cutting a Proof into Bite-Sized Chunks: Incrementally proving termination in higher-order term rewriting. In Proc. FSCD22, pages 1:1-1:17, 2022. URL: https://doi.org/10.4230/LIPIcs.FSCD.2022.1.
  23. F. Mitterwallner and A. Middeldorp. Polynomial Termination Over ℕ Is Undecidable. In Proc. FSCD, pages 27:1-27:17, 2022. URL: https://doi.org/10.4230/LIPIcs.FSCD.2022.27.
  24. G. Moser. Uniform Resource Analysis by Rewriting: Strengths and Weaknesses (Invited Talk). In Proc. FSCD, pages 2:1-2:10, 2017. URL: https://doi.org/10.4230/LIPIcs.FSCD.2017.2.
  25. G. Moser, A. Schnabl, and J. Waldmann. Complexity Analysis of Term Rewriting Based on Matrix and Context Dependent Interpretations. In Proc. IARCS, pages 304-315, 2008. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2008.1762.
  26. 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.
  27. L. Noschinski, F. Emmes, and J. Giesel. Analysing innermost runtime complexity of term rewriting by dependency pairs. JAR, 2013. URL: https://doi.org/10.1007/s10817-013-9277-6.
  28. L. Noschinski, F. Emmes, and J. Giesl. A dependency pair framework for innermost complexity analysis of term rewrite systems. In CADE-23, pages 422-438, 2011. URL: https://doi.org/10.1007/978-3-642-22438-6_32.
  29. 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.
  30. Yoshihito T. Counterexamples to termination for the direct sum of term rewriting systems. Information Processing Letters, 25(3):141-143, 1987. URL: https://doi.org/10.1016/0020-0190(87)90122-0.
  31. A. Weiermann. Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths. TCS, 1995. URL: https://doi.org/10.1016/0304-3975(94)00135-6.
  32. Wiki. The International Termination Competition (TermComp). Annual International Termination Competition, 2018. URL: http://termination-portal.org/wiki/Termination_Competition.
  33. A. Yamada. Multi-dimensional interpretations for termination of term rewriting. In In. Proc. CADE28, volume 12699 of Lecture Notes in Computer Science, pages 273-290, 2021. URL: https://doi.org/10.1007/978-3-030-79876-5_16.
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