License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2021.20
URN: urn:nbn:de:0030-drops-139154
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/13915/
Gäher, Lennard ;
Kunze, Fabian
Mechanising Complexity Theory: The Cook-Levin Theorem in Coq
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.
BibTeX - Entry
@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/opus/volltexte/2021/13915},
URN = {urn:nbn:de:0030-drops-139154},
doi = {10.4230/LIPIcs.ITP.2021.20},
annote = {Keywords: computational model, NP completeness, Coq, Cook, Levin}
}
