Document Open Access Logo

A Verified Cost Model for Call-By-Push-Value

Authors Zhuo Zoey Chen , Johannes Åman Pohjola , Christine Rizkallah

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2025.7.pdf
  • Filesize: 0.81 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
Keywords
  • lambda calculus
  • formalizations of computational models
  • computability theory
  • HOL
  • call-by-push-value reduction
  • time and space complexity
  • abstract machines

Metrics

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

Abstract

The call-by-push-value λ-calculus allows for syntactically specifying the order of evaluation as part of the term language. Hence, it serves as a unifying language for embedding various evaluation strategies including call-by-value and call-by-name. Given the impact of call-by-push-value, it is remarkable that its adequacy as a model for computational complexity theory has not yet been studied. In this paper, we show that the call-by-push-value λ-calculus is reasonable for both time and space complexity. A reasonable cost model can encode other reasonable cost models with polynomial overhead in time and constant factor overhead in space. We achieve this by encoding call-by-push-value λ-calculus into Turing machines, following a simulation strategy by Forster et al.; for the converse direction, we prove that Levy’s encoding of the call-by-value λ-calculus has reasonable complexity bounds. The main results have been formalised in the HOL4 theorem prover.

Cite As Get BibTex

Zhuo Zoey Chen, Johannes Åman Pohjola, and Christine Rizkallah. A Verified Cost Model for Call-By-Push-Value. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ITP.2025.7

Author Details

Zhuo Zoey Chen
  • University of Melbourne, Australia
Johannes Åman Pohjola
  • University of Gothenburg, Sweden
Christine Rizkallah
  • University of Melbourne, Australia

Acknowledgements

We thank Yannick and Fabian for taking the time to meet with us and discuss their work on the weak call-by-value λ-calculus. We are also grateful to the anonymous reviewers for their valuable feedback.

Supplementary Materials

References

  1. Beniamino Accattoli. (in)efficiency and reasonable cost models. In Sandra Alves and Renata Wasserman, editors, 12th Workshop on Logical and Semantic Frameworks, with Applications, LSFA 2017, Brasília, Brazil, September 23-24, 2017, volume 338 of Electronic Notes in Theoretical Computer Science, pages 23-43. Elsevier, 2017. URL: https://doi.org/10.1016/j.entcs.2018.10.003.
  2. Beniamino Accattoli and Ugo dal Lago. (leftmost-outermost) beta reduction is invariant, indeed. Log. Methods Comput. Sci., 12(1), 2016. URL: https://doi.org/10.2168/LMCS-12(1:4)2016.
  3. Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. Reasonable space for the λ-calculus, logarithmically. In Christel Baier and Dana Fisman, editors, LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022, pages 47:1-47:13. ACM, 2022. URL: https://doi.org/10.1145/3531130.3533362.
  4. Zhuo Chen. cbpv-reasonable-hol, June 2025. URL: https://github.com/ZhuoZoeyChen/cbpv-reasonable-HOL.
  5. Zhuo Zoey Chen, Johannes Åman Pohjola, and Christine Rizkallah. cbpv-reasonable-HOL. Software, (visited on 2025-09-11). URL: https://github.com/ZhuoZoeyChen/cbpv-reasonable-HOL/
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.24718
  6. Jules Chouquet and Christine Tasson. Taylor expansion for call-by-push-value. In Maribel Fernández and Anca Muscholl, editors, 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020, Barcelona, Spain, volume 152 of LIPIcs, pages 16:1-16:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPICS.CSL.2020.16.
  7. Alonzo Church. A set of postulates for the foundation of logic. Annals of Mathematics, 33(2):346-366, 1932. URL: http://www.jstor.org/stable/1968337.
  8. Ugo dal Lago and Simone Martini. The weak lambda calculus as a reasonable machine. Theor. Comput. Sci., 398(1-3):32-50, 2008. URL: https://doi.org/10.1016/j.tcs.2008.01.044.
  9. Thomas Ehrhard and Giulio Guerrieri. The bang calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value. In James Cheney and Germán Vidal, editors, Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, Edinburgh, United Kingdom, September 5-7, 2016, pages 174-187. ACM, 2016. URL: https://doi.org/10.1145/2967973.2968608.
  10. Thomas Ehrhard and Christine Tasson. Probabilistic call by push value. CoRR, abs/1607.04690, 2016. URL: https://arxiv.org/abs/1607.04690.
  11. Yannick Forster, Fabian Kunze, and Marc Roth. The weak call-by-value λ-calculus is reasonable for both time and space. Proc. ACM Program. Lang., 4(POPL):27:1-27:23, 2020. URL: https://doi.org/10.1145/3371095.
  12. Yannick Forster, Fabian Kunze, Gert Smolka, and Maximilian Wuttke. A mechanised proof of the time invariance thesis for the weak call-by-value λ-calculus. In Liron Cohen and Cezary Kaliszyk, editors, 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference), volume 193 of LIPIcs, pages 19:1-19:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.19.
  13. Yannick Forster, Steven Schäfer, Simon Spies, and Kathrin Stark. Call-by-push-value in coq: Operational, equational, and denotational theory. In Assia Mahboubi and Magnus O. Myreen, editors, Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, pages 118-131. ACM, 2019. URL: https://doi.org/10.1145/3293880.3294097.
  14. Dmitri Garbuzov, William Mansky, Christine Rizkallah, and Steve Zdancewic. Structural operational semantics for control flow graph machines. CoRR, abs/1805.05400, 2018. URL: https://arxiv.org/abs/1805.05400.
  15. G. A. Kavvos, Edward Morehouse, Daniel R. Licata, and Norman Danner. Recurrence extraction for functional programs through call-by-push-value. Proc. ACM Program. Lang., 4(POPL):15:1-15:31, 2020. URL: https://doi.org/10.1145/3371083.
  16. Delia Kesner and Andrés Viso. The power of tightness for call-by-push-value. CoRR, abs/2105.00564, 2021. URL: https://arxiv.org/abs/2105.00564.
  17. Fabian Kunze, Gert Smolka, and Yannick Forster. Formal small-step verification of a call-by-value lambda calculus machine. In Sukyoung Ryu, editor, Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 2-6, 2018, Proceedings, volume 11275 of Lecture Notes in Computer Science, pages 264-283. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-02768-1_15.
  18. Julia L. Lawall and Harry G. Mairson. Optimality and inefficiency: What isn't a cost model of the lambda calculus? In Robert Harper and Richard L. Wexelblat, editors, Proceedings of the 1996 ACM SIGPLAN International Conference on Functional Programming, ICFP 1996, Philadelphia, Pennsylvania, USA, May 24-26, 1996, pages 92-101. ACM, 1996. URL: https://doi.org/10.1145/232627.232639.
  19. Paul Blain Levy. Call-by-push-value: A subsuming paradigm. In Jean-Yves Girard, editor, Typed Lambda Calculi and Applications, 4th International Conference, TLCA'99, L'Aquila, Italy, April 7-9, 1999, Proceedings, volume 1581 of Lecture Notes in Computer Science, pages 228-242. Springer, 1999. URL: https://doi.org/10.1007/3-540-48959-2_17.
  20. Paul Blain Levy. Call-by-Push-Value. PhD thesis, Queen Mary University of London, UK, 2001. URL: https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.369233.
  21. Paul Blain Levy. Adjunction models for call-by-push-value with stacks. In Richard Blute and Peter Selinger, editors, Category Theory and Computer Science, CTCS 2002, Ottawa, Canada, August 15-17, 2002, volume 69 of Electronic Notes in Theoretical Computer Science, pages 248-271. Elsevier, 2002. URL: https://doi.org/10.1016/S1571-0661(04)80568-1.
  22. Dylan McDermott and Alan Mycroft. Extended call-by-push-value: Reasoning about effectful programs and evaluation order. In Luís Caires, editor, Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, volume 11423 of Lecture Notes in Computer Science, pages 235-262. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17184-1_9.
  23. Robin Milner, Mads Tofte, and Robert Harper. Definition of standard ML. MIT Press, 1990. Google Scholar
  24. Christine Rizkallah, Dmitri Garbuzov, and Steve Zdancewic. A formal equational theory for call-by-push-value. In Jeremy Avigad and Assia Mahboubi, editors, Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, volume 10895 of Lecture Notes in Computer Science, pages 523-541. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94821-8_31.
  25. Konrad Slind and Michael Norrish. A brief overview of HOL4. In Otmane Aït Mohamed, César A. Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, volume 5170 of Lecture Notes in Computer Science, pages 28-32. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-71067-7_6.
  26. Cees F. Slot and Peter van Emde Boas. On tape versus core; an application of space efficient perfect hash functions to the invariance of space. In Richard A. DeMillo, editor, Proceedings of the 16th Annual ACM Symposium on Theory of Computing, April 30 - May 2, 1984, Washington, DC, USA, pages 391-400. ACM, 1984. URL: https://doi.org/10.1145/800057.808705.
  27. Cassia Torczon, Emmanuel Suárez Acevedo, Shubh Agrawal, Joey Velez-Ginorio, and Stephanie Weirich. Effects and coeffects in call-by-push-value (extended version). CoRR, abs/2311.11795, 2023. URL: https://doi.org/10.48550/arXiv.2311.11795.
  28. Peter van Emde Boas. Chapter 1 - machine models and simulations. In Jan Van Leeuwen, editor, Algorithms and Complexity, Handbook of Theoretical Computer Science, pages 1-66. Elsevier, Amsterdam, 1990. URL: https://doi.org/10.1016/B978-0-444-88071-0.50006-0.
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