3 ms·
> Checking whether a string is a valid proof can be done in polynomial time. That's not true. Curry-Howard says that determining if a proof is correct has the
by andrewla 8y ago
> Checking whether a string is a valid proof can be done in polynomial time.
That's not true. Curry-Howard says that determining if a proof is correct has the same complexity as programs in general. Even if P=NP, there are still complexity classes strictly larger than P; say EXP, that would result in a proof requiring exponential time to check for validity. That's assuming that "validity" here means true/false-ness, rather than syntactical validity, which is much less useful.
- rrobukef 8y agoOP probably meant within the current context. An NP problem is defined to have a (polynomial sized) proof that can be checked in polynomial time by definition.
- YorkshireSeason 8y agoThat is misleading. Simplifying a great deal, the Curry-Howard correspondence asserts the following identities between intuitionistic logic and pure functional programming: * Types = formulae * Programs = proofs * Beta-reduction = cut-elimination Checking whether a string is a proof in a given logic is a simple computation.
- lostmsu 8y agoJust an addition to this comment: Point is that, according to Curry-Howard, validating a proof is equivalent to type checking the program, not actually running it to halting. Type checking (<-> validating a proof) is polynomial.
- dlubarov 8y agoI think pascal_cuoq's argument still works though. As I understood it, his construction was Given an instance x of some NP relation R: 1. Enumerate all (TM, π) pairs until we encounter a π which proves that TM is a correct polynomial time solution to R. 2. Simulate TM on the given instance x. The first step depends only on R, not x, so it takes constant time with respect to the instance size.