28

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?

Samuel Schlesinger
  • 1,572
  • 8
  • 20
  • 3
    I think that some research is being done at University of Bologna with the Matita proof assistant. See for example Formalizing Turing Machines. – Marzio De Biasi Nov 13 '17 at 17:22
  • Related: https://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. – Joshua Grochow Nov 13 '17 at 18:17
  • 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. – Samuel Schlesinger Nov 14 '17 at 17:44
  • 1
    There's an answer to a similar question here, though it's more about proving specific complexity bounds than general complexity theory results – Joey Eremondi Nov 14 '17 at 17:47
  • 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. – Samuel Schlesinger Nov 14 '17 at 17:50
  • In addition to jmite's answer on the question linked to, I think there's some way to formalize complexity bounds using so-called "implicit complexity theory," which might be more easily formalized in something like Coq (or whatever the current favorite is for computer implementations of univalent foundations). My starting reference for this line of work is dal Lago's papers, but @NeelKrishnaswami might have more to say on this. Been wanting to learn this stuff for a while... – Joshua Grochow Nov 14 '17 at 20:45
  • Right, with a brief look over the description of implicit complexity theory on Wikipedia it appears that this would be a cheap way for me to avoid a lot of minutia but I must read more and see if it is complete for what I want to do. – Samuel Schlesinger Nov 14 '17 at 20:52

2 Answers2

10

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.)

Martin Hofmann
  • 643
  • 6
  • 8
  • 1
    Could you please give the complete reference so that the answer does not depend on the validity of the link? – holf Nov 22 '17 at 15:29
6

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.

Clément
  • 161
  • 1
  • 4