6 ms·

Having a decision algorithm does not make a computation free. It may take exponential time in the input size, doubly exponential time, some time involving Graha

by cvoss 1y ago

Having a decision algorithm does not make a computation free. It may take exponential time in the input size, doubly exponential time, some time involving Graham's number, ... etc. It may also take up an unreasonable amount of space. Indeed, some problems have such complex algorithms that you should expect the universe to end before the answer is determined and/or the computing device is doomed to collapse into a black hole, making the answer irretrievable. So the blog post's claims that a hypothetical halting algorithm would solve anything "overnight" are exaggerated and naive.

jonahx 1y ago
"Free" in the sense of thought, cleverness, insight. You have an "everything" calculator. That is the sense in which it might be intuitive that it couldn't exist. > So the blog post's claims that a hypothetical halting algorithm would solve anything "overnight" are exaggerated and naive. I agree "overnight" is misleading in this context. However, I am fairly sure the author is aware of the point you are making.
- Dylan16807 1y ago
  > "Free" in the sense of thought, cleverness, insight. You have an "everything" calculator. That is the sense in which it might be intuitive that it couldn't exist. Right. But brute force solvers for bcrypt and chess are already "free" in the sense of thought, cleverness, insight. We already have the "everything" algorithm: iterate through all possible solutions in O(2^n) time and pick the best one. A halting solver gains us nothing in these scenarios. (The code for scoring a solution is the same code that would need to go into the halting solver. For bcrypt it's checking if the input matches, for chess it's the number of turns until checkmate.)
  - jonahx 1y ago
    Yeah, I thought I already addressed that above. Can we do the same for a theorem prover? For proofs of some fixed finite length, I think the answer is yes, but without that constraint the answer is no. Whereas with a halting detector we could. It still seems to me your complaint (and the other poster's) are just about these specific examples rather than general argument Hillel is making. Please clarify if that's not the case, and why.
    - ummonk 1y ago
      The complaint is that Hillel is providing an intuitive explanation but that intuition is clearly faulty, as demonstrated by two of the examples he gave. P.S., you can run that proof finding algorithm (iterate through every candidate proof one by one and check for validity) for proofs of finite length in general, not just some fixed finite length. Where the halting oracle comes in is that you can use it to check whether the proof finding algorithm will ever halt, and thereby find out whether the theorem is provable or not.
      - jonahx 1y ago
        > for proofs of finite length in general, not just some fixed finite length. For a brute force proof finder, for your program to be guaranteed to finish in theory, you have to pick a length. So it is fixed. Ofc you can choose whatever length you want. But you don't have that constraint with the halting oracle. Perhaps we're saying the same thing?
        ummonk 1y ago
        For the program to be guaranteed to finish in theory, all that is required is that a valid proof exists. You don't have to pick a length in advance - the program just has to keep trying proofs of progressively longer lengths.
        jonahx 1y ago
        But it won't finish if there is no proof! A halting oracle will finish either way.
        Maxatar 1y ago
        Sure, but neither bcrypt or chess fall into the category of being unprovable, so having a halting detector doesn't help for those situations. The author is mixing up problems that are "hard" in the sense that we know in principle how to solve it but need a lot of resources, versus "hard" in the sense that we genuinely don't know how to solve the problem, even if we had access to infinite resources. Mixing these two up is very misleading and detracts from what is otherwise a well written article.

by cvoss 1y ago

jonahx 1y ago

"Free" in the sense of thought, cleverness, insight. You have an "everything" calculator. That is the sense in which it might be intuitive that it couldn't exist. > So the blog post's claims that a hypothetical halting algorithm would solve anything "overnight" are exaggerated and naive. I agree "overnight" is misleading in this context. However, I am fairly sure the author is aware of the point you are making.

Dylan16807 1y ago
> "Free" in the sense of thought, cleverness, insight. You have an "everything" calculator. That is the sense in which it might be intuitive that it couldn't exist. Right. But brute force solvers for bcrypt and chess are already "free" in the sense of thought, cleverness, insight. We already have the "everything" algorithm: iterate through all possible solutions in O(2^n) time and pick the best one. A halting solver gains us nothing in these scenarios. (The code for scoring a solution is the same code that would need to go into the halting solver. For bcrypt it's checking if the input matches, for chess it's the number of turns until checkmate.)
- jonahx 1y ago
  Yeah, I thought I already addressed that above. Can we do the same for a theorem prover? For proofs of some fixed finite length, I think the answer is yes, but without that constraint the answer is no. Whereas with a halting detector we could. It still seems to me your complaint (and the other poster's) are just about these specific examples rather than general argument Hillel is making. Please clarify if that's not the case, and why.
  - ummonk 1y ago
    The complaint is that Hillel is providing an intuitive explanation but that intuition is clearly faulty, as demonstrated by two of the examples he gave. P.S., you can run that proof finding algorithm (iterate through every candidate proof one by one and check for validity) for proofs of finite length in general, not just some fixed finite length. Where the halting oracle comes in is that you can use it to check whether the proof finding algorithm will ever halt, and thereby find out whether the theorem is provable or not.
    - jonahx 1y ago
      > for proofs of finite length in general, not just some fixed finite length. For a brute force proof finder, for your program to be guaranteed to finish in theory, you have to pick a length. So it is fixed. Ofc you can choose whatever length you want. But you don't have that constraint with the halting oracle. Perhaps we're saying the same thing?
      - ummonk 1y ago
        For the program to be guaranteed to finish in theory, all that is required is that a valid proof exists. You don't have to pick a length in advance - the program just has to keep trying proofs of progressively longer lengths.
        jonahx 1y ago
        But it won't finish if there is no proof! A halting oracle will finish either way.
        Maxatar 1y ago
        Sure, but neither bcrypt or chess fall into the category of being unprovable, so having a halting detector doesn't help for those situations. The author is mixing up problems that are "hard" in the sense that we know in principle how to solve it but need a lot of resources, versus "hard" in the sense that we genuinely don't know how to solve the problem, even if we had access to infinite resources. Mixing these two up is very misleading and detracts from what is otherwise a well written article.