6 ms·

This is a rant I’ve had in my head forever, so thanks for posting this. A lot of people use the proof that the halting problem is undesirable to make some deep

by johnfn 2y ago

This is a rant I’ve had in my head forever, so thanks for posting this. A lot of people use the proof that the halting problem is undesirable to make some deep philosophical point, like this one. But the actual proof is so disappointing and non-philosophical that I wonder if anyone making these grand statements has ever read it. It just invents a program which outwits the halting detector by doing the opposite of what it would otherwise say. Its like, if you met the smartest person in the world, and you asked them “will you answer no to this question” and then no matter what they said you laughed in their face and said hah, guess you’re not so smart, are you? And THAT is why you think we don’t live in heaven? Like, OP says that because of this proof we can’t run HALT() on a program that assets the Goldbach conjecture. What? That’s entirely orthogonal from the proof of the undecidability of the halting program, unless one of the primes has embedded a trick logic question into itself somehow. There’s nothing stopping there from being a “HALT_FOR_EVERY_PROGRAM_EVER_EXCEPT_THAT_ONE_TRICK_PROGRAM”. There you go, you’re back in heaven again!

jerf 2y ago
The halting problem is more than that. While the proof constructs a relatively trivial Turing machine that basically puts the toddler's "Nuh-uh!" on solid mathematical ground, that's just the proof that there exists at least one Turing machine for a given halting oracle that can not be predicted by that halting oracle. To get to where you're complaining about people going, it needs to be paired with Rice's Theorem, as mentioned in the article: https://en.wikipedia.org/wiki/Rice%27s_theorem https://en.wikipedia.org/wiki/Rice%27s_theorem It is true that the halting problem itself is perhaps not directly what people seem to think it is, but people turn out to be right anyhow, because Rice's Theorem can be largely summed up as "It can be proven that we can not have nice things", if you'll allow me a bit of mathematician-style humor, which corresponds more-or-less to the way people talk about the Halting Problem. This also explains why the Goldbach conjecture is in fact directly related to the halting problem and not orthogonal at all. Through Rice's theorem we can extend the halting problem quite easily to the solution to that and a lot of other problems. By computer science standards, Rice's theorem is relatively basic stuff. I don't recall if the sophomore-level class I learned about this stuff did a full proof of Rice's theorem but I certainly recall several homework problems around applying the idea of the theorem to several specific problems by proving reductions of those problems to the halting problem. I also recall they really weren't particularly difficult problems. It's not hard to reduce that sort of interesting question to the halting problem. Low-level undergrad stuff, stuff down in the very basics of computer science qua computer science suitable for making up several problems in the weekly homework assignment for the intro to (real) computer science course, not complicated abtruse stuff that can't be applied by anyone less than a doctoral candidate with a few months to burn. All sorts of problems are reducible like this. And that is why the "halting problem" in fact is the reason why we can't have certain nice things we'd really like. For example, the mentioned ability to prove that two functions really are equivalent would have practical utility in a wide variety of places (assuming somewhat reasonable efficiency), like compiler optimizations. Your intuition is correct in one respect though; there is a sense in which it isn't really "The Halting Problem (TM)". You could take a wide variety of other problems and call them "the" fundamental problem, and reduce the halting problem to those problems. The Halting Problem just turns out to be a particularly concise specific expression of the general problem that is easy to express for Turing Machines. It just makes for nicer proofs than the alternatives. "The" core problem could arguably be something more like Rice's Theorem proved on its own as a fundamental proof without reference to the halting problem. You could call the Halting Problem a historical accident that we hold on to due to a path dependency in how math happened to develop in our history. An alien race might have a reasonably different view on the "fundamental problem", but then they'd have a something fairly similar to Rice's Theorem sitting on top of it that we'd all recognize.
russdill 2y ago
The philosophical issue is there are questions which seem "simple" and have answers, but even if given the answer you could not know whether it was the right answer.
yongjik 2y ago
> There’s nothing stopping there from being a “HALT_FOR_EVERY_PROGRAM_EVER_EXCEPT_THAT_ONE_TRICK_PROGRAM”. Doesn't work that way. If we have "HALT_FOR_...EXCEPT_THAT_ONE_TRICK_PROGRAM", then we can simply create "HALT_FOR_ACTUALLY_EVERY_PROGRAM" by: if (is this that one trick program?) then return THE CORRECT ANSWER FOR THAT TRICK QUESTION, HARD-CODED else answer = HALT_FOR_EVERY_PROGRAM_EVER_EXCEPT_THAT_ONE_TRICK_PROGRAM() return answer ...but this is impossible, because then it would actually solve the full halting program, and we know it's impossible. So the best you can have is "Solve the halting problem for a bunch of programs, but not for a bunch of others, but that's okay because will call the latter as 'trick programs.'" And the problem is that you can't give a mathematically satisfying definition of what is a trick program, and whatever you try, you'll likely end up defining a lot of actually interesting programs as trick programs. So it's actually "Solve the halting problem for some programs, but not others." And that's not terribly interesting, because we already know it's possible.
- musicale 2y ago
  I am probably not the only one who finds the above as pointless as trying to determine whether the sentence "this sentence is false" is true or false. It is neither, but most of the time we're interested in problems that have answers, and that problem space turns out to be huge and extremely useful. What are some good examples of practical programs that aren't trying to create a chain of computation that is ultimately circular and self-referential yet still run into trouble with the halting problem?
  - lmm 2y ago
    > What are some good examples of practical programs that aren't trying to create a chain of computation that is ultimately circular and self-referential yet still run into trouble with the halting problem? Almost any unproven mathematical conjecture, e.g. a program that searches for counterexamples to the Riemann hypothesis. More practically, a lot of problems reduce to SAT, so these days quite a lot of systems work by just running a SAT solver on the problem (e.g. dependency resolution in some build systems), and it's fast most of the time but you can never be sure it's not going to get stuck.
rf15 2y ago
Yeah, it's fundamentally a "if god can create anything, can he create a rock that he himself cannot lift?" kind of deal - a meaningless philosophical debate because the parameters were constructed to make the problem possible in the first place. An "intellectual trap", if you will. Alternatively: We know that the earth is not perfectly flat, so why are our spherical cows not rolling off the meadow?
- influx 2y ago
  Your comment helped me get this: function HALT(program, input): # This is a "magic" function for our proof - we assume it exists for all programs # In reality, this function cannot exist because of the paradox we're about to create # Returns True if `program(input)` halts, False if it runs forever ... # Program D: Creates the paradox function D(self): if HALT(D, self) == True: loop_forever() else: halt()
benlivengood 2y ago
Kolmogorov complexity is undecidable because the halting problem is undecidable. If we could solve Kolmogorov complexity we could do Solomonoff induction and build AIXI and solve (at least one formulation of) decision theory. The real problem (imo) is that proof search is also undecidable (either directly from halting problem or similar argument) and so there isn't a procedure we can write that identifies trick programs to exclude as special cases. There are an infinite number of various trick programs for which halting is undecidable and recognizing them is undecidable.

by johnfn 2y ago

jerf 2y ago

The halting problem is more than that. While the proof constructs a relatively trivial Turing machine that basically puts the toddler's "Nuh-uh!" on solid mathematical ground, that's just the proof that there exists at least one Turing machine for a given halting oracle that can not be predicted by that halting oracle. To get to where you're complaining about people going, it needs to be paired with Rice's Theorem, as mentioned in the article: https://en.wikipedia.org/wiki/Rice%27s_theorem https://en.wikipedia.org/wiki/Rice%27s_theorem It is true that the halting problem itself is perhaps not directly what people seem to think it is, but people turn out to be right anyhow, because Rice's Theorem can be largely summed up as "It can be proven that we can not have nice things", if you'll allow me a bit of mathematician-style humor, which corresponds more-or-less to the way people talk about the Halting Problem. This also explains why the Goldbach conjecture is in fact directly related to the halting problem and not orthogonal at all. Through Rice's theorem we can extend the halting problem quite easily to the solution to that and a lot of other problems. By computer science standards, Rice's theorem is relatively basic stuff. I don't recall if the sophomore-level class I learned about this stuff did a full proof of Rice's theorem but I certainly recall several homework problems around applying the idea of the theorem to several specific problems by proving reductions of those problems to the halting problem. I also recall they really weren't particularly difficult problems. It's not hard to reduce that sort of interesting question to the halting problem. Low-level undergrad stuff, stuff down in the very basics of computer science qua computer science suitable for making up several problems in the weekly homework assignment for the intro to (real) computer science course, not complicated abtruse stuff that can't be applied by anyone less than a doctoral candidate with a few months to burn. All sorts of problems are reducible like this. And that is why the "halting problem" in fact is the reason why we can't have certain nice things we'd really like. For example, the mentioned ability to prove that two functions really are equivalent would have practical utility in a wide variety of places (assuming somewhat reasonable efficiency), like compiler optimizations. Your intuition is correct in one respect though; there is a sense in which it isn't really "The Halting Problem (TM)". You could take a wide variety of other problems and call them "the" fundamental problem, and reduce the halting problem to those problems. The Halting Problem just turns out to be a particularly concise specific expression of the general problem that is easy to express for Turing Machines. It just makes for nicer proofs than the alternatives. "The" core problem could arguably be something more like Rice's Theorem proved on its own as a fundamental proof without reference to the halting problem. You could call the Halting Problem a historical accident that we hold on to due to a path dependency in how math happened to develop in our history. An alien race might have a reasonably different view on the "fundamental problem", but then they'd have a something fairly similar to Rice's Theorem sitting on top of it that we'd all recognize.

russdill 2y ago

The philosophical issue is there are questions which seem "simple" and have answers, but even if given the answer you could not know whether it was the right answer.

yongjik 2y ago

> There’s nothing stopping there from being a “HALT_FOR_EVERY_PROGRAM_EVER_EXCEPT_THAT_ONE_TRICK_PROGRAM”. Doesn't work that way. If we have "HALT_FOR_...EXCEPT_THAT_ONE_TRICK_PROGRAM", then we can simply create "HALT_FOR_ACTUALLY_EVERY_PROGRAM" by: if (is this that one trick program?) then return THE CORRECT ANSWER FOR THAT TRICK QUESTION, HARD-CODED else answer = HALT_FOR_EVERY_PROGRAM_EVER_EXCEPT_THAT_ONE_TRICK_PROGRAM() return answer ...but this is impossible, because then it would actually solve the full halting program, and we know it's impossible. So the best you can have is "Solve the halting problem for a bunch of programs, but not for a bunch of others, but that's okay because will call the latter as 'trick programs.'" And the problem is that you can't give a mathematically satisfying definition of what is a trick program, and whatever you try, you'll likely end up defining a lot of actually interesting programs as trick programs. So it's actually "Solve the halting problem for some programs, but not others." And that's not terribly interesting, because we already know it's possible.

musicale 2y ago
I am probably not the only one who finds the above as pointless as trying to determine whether the sentence "this sentence is false" is true or false. It is neither, but most of the time we're interested in problems that have answers, and that problem space turns out to be huge and extremely useful. What are some good examples of practical programs that aren't trying to create a chain of computation that is ultimately circular and self-referential yet still run into trouble with the halting problem?
- lmm 2y ago
  > What are some good examples of practical programs that aren't trying to create a chain of computation that is ultimately circular and self-referential yet still run into trouble with the halting problem? Almost any unproven mathematical conjecture, e.g. a program that searches for counterexamples to the Riemann hypothesis. More practically, a lot of problems reduce to SAT, so these days quite a lot of systems work by just running a SAT solver on the problem (e.g. dependency resolution in some build systems), and it's fast most of the time but you can never be sure it's not going to get stuck.

rf15 2y ago

Yeah, it's fundamentally a "if god can create anything, can he create a rock that he himself cannot lift?" kind of deal - a meaningless philosophical debate because the parameters were constructed to make the problem possible in the first place. An "intellectual trap", if you will. Alternatively: We know that the earth is not perfectly flat, so why are our spherical cows not rolling off the meadow?

influx 2y ago
Your comment helped me get this: function HALT(program, input): # This is a "magic" function for our proof - we assume it exists for all programs # In reality, this function cannot exist because of the paradox we're about to create # Returns True if `program(input)` halts, False if it runs forever ... # Program D: Creates the paradox function D(self): if HALT(D, self) == True: loop_forever() else: halt()

benlivengood 2y ago

Kolmogorov complexity is undecidable because the halting problem is undecidable. If we could solve Kolmogorov complexity we could do Solomonoff induction and build AIXI and solve (at least one formulation of) decision theory. The real problem (imo) is that proof search is also undecidable (either directly from halting problem or similar argument) and so there isn't a procedure we can write that identifies trick programs to exclude as special cases. There are an infinite number of various trick programs for which halting is undecidable and recognizing them is undecidable.