Is there any ongoing project to formally verify the theorems and proofs of complexity theory using a proof assistant like Coq? Are there any boundaries to doing this?
$\begingroup$
$\endgroup$
7
asked Nov 13, 2017 at 16:25
-
3$\begingroup$ I think that some research is being done at University of Bologna with the Matita proof assistant. See for example Formalizing Turing Machines. $\endgroup$– Marzio De BiasiCommented Nov 13, 2017 at 17:22
-
$\begingroup$ Related: cstheory.stackexchange.com/q/4052/129. Some of the answers even talk about Coq, and others mention results that could be interpreted as theoretical barriers to this project, though likely they are not barriers in practice. $\endgroup$– Joshua GrochowCommented Nov 13, 2017 at 18:17
-
$\begingroup$ Thanks, that question was great @JoshuaGrochow, so glad I learned about that Hartmannis monograph. If I understand, the barrier would then be making sure that the complexity classes you define are what you think they are rather than the "provable in Coq" version. $\endgroup$– Samuel SchlesingerCommented Nov 14, 2017 at 17:44
-
1$\begingroup$ There's an answer to a similar question here, though it's more about proving specific complexity bounds than general complexity theory results $\endgroup$– Joey EremondiCommented Nov 14, 2017 at 17:47
-
$\begingroup$ Right that's relevant though. I'm curious about ways in which the underlying type system could help, like by including some notions of complexity in the types of functions. Of course this would lead to a wide range of equalities but I think that's what we have in complexity naturally anyways. $\endgroup$– Samuel SchlesingerCommented Nov 14, 2017 at 17:50
|
Show 2 more comments
2 Answers
$\begingroup$
$\endgroup$
1
In the following paper my colleague Uli Schöpp presents a formal verification (in Coq) of a nontrivial result by Cook and Rackoff on the computational power of graph automata. https://scholar.google.at/scholar?oi=bibs&cluster=4944920843669159892&btnI=1&hl=de (Schöpp, U. (2008). A formalised lower bound on undirected graph reachability. In Logic for Programming, Artificial Intelligence, and Reasoning (pp. 621-635). Springer Berlin/Heidelberg.)
-
1$\begingroup$ Could you please give the complete reference so that the answer does not depend on the validity of the link? $\endgroup$– holfCommented Nov 22, 2017 at 15:29
$\begingroup$
$\endgroup$
1
A nice example is Hugo Férée, Samuel Hym, Micaela Mayero, Jean-Yves Moyen, David Nowak: Formal proof of polynomial-time complexity with quasi-interpretations. CPP 2018: 146-157
Their abstract (my emphasis):
We present a Coq library that allows for readily proving that a function is computable in polynomial time. It is based on quasi-interpretations that, in combination with termination ordering, provide a characterisation of the class FP of functions computable in polynomial time. At the heart oft his formalisation is a proof of soundness and extensional completeness. Compared to the original paper proof, we had to fill a lot of not so trivial details that were left to the reader and fix a few glitches. To demonstrate the usability of our library, we apply it to the modular exponentiation.
-
1$\begingroup$ This work is also related to A Formalization of Polytime Functions. $\endgroup$– ClémentCommented Apr 28, 2021 at 12:53