Document Open Access Logo

Mechanising Complexity Theory: The Cook-Levin Theorem in Coq

Authors Lennard Gäher, Fabian Kunze

PDF
Thumbnail PDF

File

LIPIcs.ITP.2021.20.pdf
  • Filesize: 0.83 MB
  • 18 pages

Document Identifiers

Author Details

Lennard Gäher
  • Universität des Saarlandes, Saarland Informatics Campus, Saarbrücken, Germany
Fabian Kunze
  • Universität des Saarlandes, Saarland Informatics Campus, Saarbrücken, Germany

Funding

  • Gäher, Lennard: was supported in part by the International Max-Planck Research School on Trusted Computing (IMPRS-TRUST).

Cite As Get BibTex

Lennard Gäher and Fabian Kunze. Mechanising Complexity Theory: The Cook-Levin Theorem in Coq. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.ITP.2021.20

Abstract

We mechanise the Cook-Levin theorem, i.e. the NP-completeness of SAT, in the proof assistant Coq. We use the call-by-value λ-calculus L as the model of computation to formalise time complexity, the class NP, and polynomial-time reductions. The latter two notions agree with the usual characterisations via Turing machines (TMs), as L and TMs are polynomial-time equivalent.
The use of L as the computational model, as opposed to TMs, significantly eases program verification and the derivation of resource bounds. However, for showing the NP-hardness of SAT, computations of L need to be encoded in SAT, which is complicated by L’s more complex computational structure. Thus, the polynomial-time reduction chain to SAT employs TMs as an intermediate problem, for which we neatly factor out a known textbook reduction from TMs to SAT. Still, all reduction functions are implemented and analysed in L.
To the best of our knowledge, this is the first result in computational complexity theory that has been mechanised with respect to any concrete computational model. 
We discuss what makes this area of computer science hard to mechanise and highlight the design choices which enable our mechanisations.

Subject Classification

ACM Subject Classification
  • Theory of computation → Problems, reductions and completeness
  • Theory of computation → Complexity classes
  • Theory of computation → Lambda calculus
  • Theory of computation → Logic and verification
  • Theory of computation → Constructive mathematics
Keywords
  • computational model
  • NP completeness
  • Coq
  • Cook
  • Levin

Metrics

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

Supplementary Materials

References

  1. Andrea Asperti. A formal proof of borodin-trakhtenbrot’s gap theorem. In Georges Gonthier and Michael Norrish, editors, Certified Programs and Proofs, pages 163-177, Cham, 2013. Springer International Publishing. Google Scholar
  2. Andrea Asperti. Reverse complexity. Journal of Automated Reasoning, 55:373-388, 2015. Google Scholar
  3. Andrea Asperti and Wilmer Ricciotti. A formalization of multi-tape Turing machines. Theoretical Computer Science, 603:23-42, 2015. Google Scholar
  4. Andrej Bauer. First steps in synthetic computability theory. Electron. Notes Theor. Comput. Sci., 155:5–31, 2006. URL: https://doi.org/10.1016/j.entcs.2005.11.049.
  5. 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.
  6. Mario M. Carneiro. Formalizing computability theory via partial recursive functions. In John Harrison, John O'Leary, and Andrew Tolmach, editors, 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA, volume 141 of LIPIcs, pages 12:1-12:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.ITP.2019.12.
  7. Stephen A. Cook. The complexity of theorem-proving procedures. In Proceedings of the Third Annual ACM Symposium on Theory of Computing, STOC ’71, page 151–158, New York, NY, USA, 1971. Association for Computing Machinery. URL: https://doi.org/10.1145/800157.805047.
  8. Ronald Fagin. Generalized first-order spectra, and polynomial. time recognizable sets. SIAM-AMS Proc., 7, January 1974. Google Scholar
  9. Yannick Forster, Dominik Kirst, and Gert Smolka. On synthetic undecidability in Coq, with an application to the Entscheidungsproblem. In 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, New York, NY, USA, January 2019. ACM. Google Scholar
  10. 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. Google Scholar
  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, and Maximilian Wuttke. Verified programming of Turing machines in Coq. In 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20–21, 2020, New York, NY, USA, 2020. ACM. Google Scholar
  13. Yannick Forster, Fabian Kunze, 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), volume 193 of Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany, 2021. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. Google Scholar
  14. 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.
  15. 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
  16. Ruben Gamboa and John Cowles. A mechanical proof of the Cook-Levin theorem. In Konrad Slind, Annette Bunker, and Ganesh Gopalakrishnan, editors, Theorem Proving in Higher Order Logics, pages 99-116, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. Google Scholar
  17. Armaël Guéneau, Arthur Charguéraud, and François Pottier. A fistful of dollars: Formalizing asymptotic complexity claims via deductive program verification. In Amal Ahmed, editor, Programming Languages and Systems, pages 533-560, Cham, 2018. Springer International Publishing. Google Scholar
  18. Martin Hofmann. Linear types and non size-increasing polynomial time computation. In Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, LICS '99, page 464, USA, 1999. IEEE Computer Society. Google Scholar
  19. 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.
  20. Richard M. Karp. Reducibility among Combinatorial Problems, pages 85-103. Springer US, Boston, MA, 1972. URL: https://doi.org/10.1007/978-1-4684-2001-2_9.
  21. L. A. Levin. Universal sequential search problems. Problems Inform. Transmission, 9:265-266, 1973. [Probl. Peredachi Inf., 9,3:115-116, 1973]. Google Scholar
  22. Torben Æ. Mogensen. Efficient self-interpretation in lambda calculus. JOURNAL OF FUNCTIONAL PROGRAMMING, 2:345-364, 1994. Google Scholar
  23. Michael Norrish. Mechanised computability theory. In Marko van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk, editors, Interactive Theorem Proving, pages 297-311, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. Google Scholar
  24. Christos H. Papadimitriou. Computational Complexity, page 260–265. John Wiley and Sons Ltd., GBR, 2003. Google Scholar
  25. Michael Sipser. Introduction to the Theory of Computation. International Thomson Publishing, 1st edition, 1996. Google Scholar
  26. C. Slot and P. van Emde Boas. On tape versus core an application of space efficient perfect hash functions to the invariance of space. In Proceedings of the Sixteenth Annual ACM Symposium on Theory of Computing, STOC '84, page 391–400, New York, NY, USA, 1984. Association for Computing Machinery. URL: https://doi.org/10.1145/800057.808705.
  27. G. S. Tseitin. On the Complexity of Derivation in Propositional Calculus, pages 466-483. Springer Berlin Heidelberg, Berlin, Heidelberg, 1983. URL: https://doi.org/10.1007/978-3-642-81955-1_28.
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