3
$\begingroup$

Can complexity theoretic reductions that lead to proofs of say NP completeness be formalized using an existing theorem prover such as Coq?

If so, can you provide an outline of how to formalize a simple reduction argument? I’d also appreciate pointers to the literature.

$\endgroup$
  • $\begingroup$ The belief is that all mathematical arguments can be formalized in Coq. NP-hardness reductions are mathematical arguments. The only conclusion is... $\endgroup$ – Yuval Filmus Nov 10 '17 at 6:24
4
$\begingroup$

This is certainly possible, and the language of higher order functions makes this quite nice. If you're doing a Turing/Cook reduction, you can basically just write a function that takes an oracle as a parameter.

For example, to show that Graph Coloring is NP-hard, you could write something like this (pardon my terrible Coq-like pseudocode)

Theorem reduction: 
  (forall (k:Nat) (g:Graph), Decidable (Coloring g))
  -> (forall (f:BoolFormula), Decidable (Model f))

What gets tricky is proving that your reductions are polynomial-time. There are ways to do this, such as with a time-tracking monad. This example verifies the time complexity of a sorting algorithm, and gives some hints as to how to model this. Basically, for whatever operation you're counting as $O(1)$, you require that it be performed in the monad, as well as calls to your oracle. Then you write a proof of some polynomial bound on the number of operations performed in the monad (which can keep track of them by encapsulating state).

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.