Document Open Access Logo

A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus

Authors Yannick Forster , Fabian Kunze, Gert Smolka, Maximilian Wuttke

PDF
Thumbnail PDF

File

LIPIcs.ITP.2021.19.pdf
  • Filesize: 0.97 MB
  • 20 pages

Document Identifiers

Author Details

Yannick Forster
  • Saarland University, Saarland Informatics Campus, Saarbrücken, Germany
Fabian Kunze
  • Saarland University, Saarland Informatics Campus, Saarbrücken, Germany
Gert Smolka
  • Saarland University, Saarland Informatics Campus, Saarbrücken, Germany
Maximilian Wuttke
  • Saarland University, Saarland Informatics Campus, Saarbrücken, Germany

Acknowledgements

We want to thank Lennard Gäher and Dominik Kirst for valuable feedback on drafts of this paper.

Cite As Get BibTex

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 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 19:1-19:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.ITP.2021.19

Abstract

The weak call-by-value λ-calculus Łand Turing machines can simulate each other with a polynomial overhead in time. This time invariance thesis for L, where the number of β-reductions of a computation is taken as its time complexity, is the culmination of a 25-years line of research, combining work by Blelloch, Greiner, Dal Lago, Martini, Accattoli, Forster, Kunze, Roth, and Smolka. The present paper presents a mechanised proof of the time invariance thesis for L, constituting the first mechanised equivalence proof between two standard models of computation covering time complexity.
The mechanisation builds on an existing framework for the extraction of Coq functions to L and contributes a novel Hoare logic framework for the verification of Turing machines.
The mechanised proof of the time invariance thesis establishes Łas model for future developments of mechanised computational complexity theory regarding time. It can also be seen as a non-trivial but elementary case study of time-complexity-preserving translations between a functional language and a sequential machine model. As a by-product, we obtain a mechanised many-one equivalence proof of the halting problems for Łand Turing machines, which we contribute to the Coq Library of Undecidability Proofs.

Subject Classification

ACM Subject Classification
  • Theory of computation → Computability
  • Theory of computation → Type theory
Keywords
  • formalizations of computational models
  • computability theory
  • Coq
  • time complexity
  • Turing machines
  • lambda calculus
  • Hoare logic

Metrics

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

Supplementary Materials

References

  1. Beniamino Accattoli and Ugo Dal Lago. (Leftmost-Outermost) Beta Reduction is Invariant, Indeed. Logical Methods in Computer Science, 12(1), 2016. URL: https://doi.org/10.2168/LMCS-12(1:4)2016.
  2. Andrea Asperti and Wilmer Ricciotti. Formalizing Turing Machines. In Logic, Language, Information and Computation, pages 1-25. Springer, 2012. Google Scholar
  3. Guy E. Blelloch and John Greiner. Parallelism in Sequential Functional Languages. In Proceedings of the seventh international conference on Functional programming languages and computer architecture, FPCA 1995, La Jolla, California, USA, June 25-28, 1995, pages 226-237, 1995. URL: https://doi.org/10.1145/224164.224210.
  4. Alonzo Church. A set of postulates for the foundation of logic. Annals of mathematics, pages 346-366, 1932. Google Scholar
  5. Alonzo Church. An unsolvable problem of elementary number theory. American journal of mathematics, 58(2):345-363, 1936. Google Scholar
  6. Yannick Forster and Fabian Kunze. A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus. In John Harrison, John O'Leary, and Andrew Tolmach, editors, 10th International Conference on Interactive Theorem Proving (ITP 2019), volume 141 of Leibniz International Proceedings in Informatics (LIPIcs), pages 17:1-17:19, Dagstuhl, Germany, 2019. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2019.17.
  7. Yannick Forster, Fabian Kunze, and Marc Roth. The weak call-by-value λ-calculus is reasonable for both time and space. Proceedings of the ACM on Programming Languages, 4(POPL):1-23, 2019. Google Scholar
  8. Yannick Forster, Fabian Kunze, Gert Smolka, and Maximilian Wuttke. Appendix b: A mechanised proof of the time invariance thesis for the weak call-by-value λ-calculus. Technical report, Saarland University, 2021. URL: https://www.ps.uni-saarland.de/Publications/documents/AppendixB_ForsterEtAl_2021_Mechanised-Time-Invariance-L.pdf.
  9. Yannick Forster, Fabian Kunze, and Maximilian Wuttke. Verified programming of Turing machines in Coq. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 114-128, 2020. Google Scholar
  10. Yannick Forster and Dominique Larchey-Wendling. Certified undecidability of intuitionistic linear logic via binary stack machines and minsky machines. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 104-117, 2019. Google Scholar
  11. Yannick Forster, Dominique Larchey-Wendling, Andrej Dudenhefner, Edith Heiter, Dominik Kirst, Fabian Kunze, Gert Smolka, Simon Spies, Dominik Wehr, and Maximilian Wuttke. A Coq library of undecidable problems. In The Sixth International Workshop on Coq for Programming Languages (CoqPL 2020)., 2020. URL: https://github.com/uds-psl/coq-library-undecidability.
  12. Yannick Forster and Gert Smolka. Weak call-by-value lambda calculus as a model of computation in Coq. In International Conference on Interactive Theorem Proving, pages 189-206. Springer, 2017. Google Scholar
  13. John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman. Introduction to Automata Theory, Languages, and Computation (3rd Edition). Addison-Wesley Longman Publishing Co., Inc., USA, 2006. Google Scholar
  14. Jan Martin Jansen. Programming in the λ-Calculus: From Church to Scott and Back, pages 168-180. Springer Berlin Heidelberg, Berlin, Heidelberg, 2013. URL: https://doi.org/10.1007/978-3-642-40355-2_12.
  15. Fabian Kunze, Gert Smolka, and Yannick Forster. Formal small-step verification of a call-by-value lambda calculus machine. In Asian Symposium on Programming Languages and Systems, pages 264-283. Springer, 2018. Google Scholar
  16. Ugo Dal Lago and Beniamino Accattoli. Encoding Turing machines into the deterministic lambda-calculus. arXiv preprint arXiv:1711.10078, 2017. Google Scholar
  17. 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.
  18. Dominique Larchey-Wendling and Yannick Forster. Hilbert’s tenth problem in Coq. arXiv preprint arXiv:2003.04604, 2020. Google Scholar
  19. Torben Æ. Mogensen. Efficient self-interpretation in lambda calculus. JOURNAL OF FUNCTIONAL PROGRAMMING, 2:345-364, 1994. Google Scholar
  20. Joachim Niehren. Uniform confluence in concurrent computation. Journal on Functional Programming, 10(5):453-499, 2000. Google Scholar
  21. Gordon D. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical computer science, 1(2):125-159, 1975. Google Scholar
  22. Damien Pous. A certified compiler from recursive functions to minski machines. Technical report, Université Paris-Diderot, PPS, 2004. URL: http://perso.ens-lyon.fr/damien.pous/recursive-minski/.
  23. 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 Proceedings of the 16th Annual ACM Symposium on Theory of Computing, April 30 - May 2, 1984, Washington, DC, USA, pages 391-400, 1984. URL: https://doi.org/10.1145/800057.808705.
  24. Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, and Théo Winterhalter. The MetaCoq Project. Journal of Automated Reasoning, 2020. URL: https://doi.org/10.1007/s10817-019-09540-0.
  25. Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Théo Winterhalter. Coq Coq correct! verification of type checking and erasure for Coq, in Coq. Proceedings of the ACM on Programming Languages, 4(POPL):1-28, 2019. Google Scholar
  26. The Coq Development Team. The coq proof assistant, version 8.12.0, July 2020. URL: https://doi.org/10.5281/zenodo.4021912.
  27. Alan Mathison Turing. On computable numbers, with an application to the Entscheidungsproblem. J. of Math, 58(345-363):5, 1936. Google Scholar
  28. Maximilian Wuttke. Verified programming of Turing machines in Coq. Bachelor’s thesis, Saarland University, 2018. Google Scholar
  29. Jian Xu, Xingyuan Zhang, and Christian Urban. Mechanising Turing machines and computability theory in Isabelle/HOL. In International Conference on Interactive Theorem Proving, pages 147-162. Springer, 2013. 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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact