Hacker News Reader

Comment by pascal_cuoq | Hacker News Reader

It's automatically constructive.

Algorithms can be enumerated. Proofs can be enumerated. For any formalized problem Q in NP, you can always simply enumerate algorithms A and candidate proofs P until you stumble on a pair (A, P) where P is a proof that A answers Q in polynomial time.

If P=NP, this first step takes constant time (long but independent on the input).

If P!=NP, this first step takes forever.

In other words, if you have a non-constructive proof that P=NP, just make “search for the polynomial algorithm” the first step of the algorithm, and now you have a constructive proof.

View on HN

> For any formalized problem Q in NP, you can always simply enumerate algorithms A and candidate proofs P until you stumble on a pair (A, P) where P is a proof that A answers Q in polynomial time.

I'm curious: does this run afoul of the halting problem?

No, since a proof is finite. When you enumerate Turing machines to generate a proof you execute the first n machines for n steps. At some point some machine must decide something, so some n is the bound.

> No, since a proof is finite. When you enumerate Turing machines to generate a proof you execute the first n machines for n steps. At some point some machine must decide something, so some n is the bound.

Thanks. It's been awhile for me, so if you could bear with the perhaps simple question: do we avoid undecidability here by the finitude of the proof or by only running a finite number of steps? It seems to me like there are three states for any solver: (1) it responds in the negative (this is not a proof), (2) it responds in the positive (this is a proof, you're done), or (3) I'm still trying figure it out.

Do we fold the 3d case into the 1st by saying that we'll only iterate n steps before terminating? Or am I missing the point entirely?

How do you ensure that the proof system you are enumerating over is strong enough to prove that the program witnessing P=NP is indeed polynomial? Prima facie polynomialness of this program can be independent from the ambient logic.

Sure, it's trivially constructive but if it turns out NP problems can be solved at minimum with like O(n^1000000000) complexity, your search could take unfathomable amounts of time to terminate.

> Algorithms can be enumerated. Proofs can be enumerated.

How exactly do you do this?

Checking whether a string is a valid proof can be done in polynomial time. So, enumerate all possible strings, and check if each string is a valid proof of what you're trying to find.

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

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

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

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

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

But enumerating all the possible strings takes infinite time? Or, wait, is this saying that since there is some algorithm you can spend some constant amount of time to find it that doesn’t affect the time complexity of your algorithm? I’m not sure I’d call that “constructive”.

If you know that such a proof exists, then it's guaranteed to terminate.

is this saying that since there is some algorithm you can spend some constant amount of time to find it

Yes.

I’m not sure I’d call that “constructive”.

The method for constructing the algorithm is given!

Reply on news.ycombinator.com