Search Results

Documents authored by Gäher, Lennard


Document
Mechanising Complexity Theory: The Cook-Levin Theorem in Coq

Authors: Lennard Gäher and Fabian Kunze

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)


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.

Cite as

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)


Copy BibTex To Clipboard

@InProceedings{gaher_et_al:LIPIcs.ITP.2021.20,
  author =	{G\"{a}her, Lennard and Kunze, Fabian},
  title =	{{Mechanising Complexity Theory: The Cook-Levin Theorem in Coq}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{20:1--20:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.20},
  URN =		{urn:nbn:de:0030-drops-139154},
  doi =		{10.4230/LIPIcs.ITP.2021.20},
  annote =	{Keywords: computational model, NP completeness, Coq, Cook, Levin}
}
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