6 ms·

You assume that the proof for P = NP would be constructive.

by tyilo 7y ago

pascal_cuoq 7y ago
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.
- saagarjha 7y ago
  > Algorithms can be enumerated. Proofs can be enumerated. How exactly do you do this?
  - jcranmer 7y ago
    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.
    - saagarjha 7y ago
      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”.
      - jcranmer 7y ago
        If you know that such a proof exists, then it's guaranteed to terminate.
      - kd0amg 7y ago
        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!
    - andrewla 7y 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 7y ago
        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.
      - YorkshireSeason 7y ago
        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.
        lostmsu 7y ago
        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.
      - dlubarov 7y ago
        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.
- memling 7y ago
  > 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?
  - rrobukef 7y ago
    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.
    - memling 7y ago
      > 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?
- opportune 7y ago
  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.
- YorkshireSeason 7y ago
  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.

You assume that the proof for P = NP would be constructive.

by tyilo 7y ago

You assume that the proof for P = NP would be constructive.

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.

saagarjha 7y ago
> Algorithms can be enumerated. Proofs can be enumerated. How exactly do you do this?
- jcranmer 7y ago
  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.
  - saagarjha 7y ago
    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”.
    - jcranmer 7y ago
      If you know that such a proof exists, then it's guaranteed to terminate.
    - kd0amg 7y ago
      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!
  - andrewla 7y 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 7y ago
      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.
    - YorkshireSeason 7y ago
      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.
      - lostmsu 7y ago
        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.
    - dlubarov 7y ago
      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.
memling 7y ago
> 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?
- rrobukef 7y ago
  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.
  - memling 7y ago
    > 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?
opportune 7y ago
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.
YorkshireSeason 7y ago
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.