5 ms·

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

> 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.
  - schoen 2y ago
    > Almost any unproven mathematical conjecture, e.g. a program that searches for counterexamples to the Riemann hypothesis. This is a very good example. We don't know whether such programs will ever stop, and knowing is exactly equivalent to resolving the conjectures. > 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. This is a less good example because SAT solvers can always run in finite time and can be proven to halt. Even if they do "get stuck", they will take exponential time rather than infinite time. There are probably some problems that arise practically that are undecidable in general (e.g. type checking for sufficiently expressive type systems), but problems that "reduce to SAT" are never examples of such undecidable problems because SAT is decidable.
    - musicale 2y ago
      I was going to say the same thing about SAT, or any NP-hard problem. The first example doesn't seem to be good either however. I don't think that proving a mathematical conjecture which has resisted proof for decades (or longer) is something that we would typically expect a computer program to be able to do. Whenever this happens, it is hailed as a major breakthrough.
      - anyfoo 2y ago
        Is there some circular logic in your reasoning? What is the difference between the computer program solving the conjecture, and “us” doing it?
      - lmm 2y ago
        The point is that it can complicate analysis of a program, at least if you take the fundamentalist view that all program behaviour should be provably correct. Like if you need the collantz sequence of a number or something in your program, you would just calculate it and use it, but it's surprisingly hard to prove that it always exists. Which isn't so much a problem in itself as it complicates trying to prove anything else about your program's behaviour.
anyfoo 2y ago
> 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.'" The awesome and surprising thing is, I’ve actually written such a program! It regularly runs the program to test, but stops and screams “trick program!” if the program to test did not finish within five minutes. Sadly, I haven’t been awarded my Fields Medal yet, probably because I didn’t use LLMs.

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.
- schoen 2y ago
  > Almost any unproven mathematical conjecture, e.g. a program that searches for counterexamples to the Riemann hypothesis. This is a very good example. We don't know whether such programs will ever stop, and knowing is exactly equivalent to resolving the conjectures. > 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. This is a less good example because SAT solvers can always run in finite time and can be proven to halt. Even if they do "get stuck", they will take exponential time rather than infinite time. There are probably some problems that arise practically that are undecidable in general (e.g. type checking for sufficiently expressive type systems), but problems that "reduce to SAT" are never examples of such undecidable problems because SAT is decidable.
  - musicale 2y ago
    I was going to say the same thing about SAT, or any NP-hard problem. The first example doesn't seem to be good either however. I don't think that proving a mathematical conjecture which has resisted proof for decades (or longer) is something that we would typically expect a computer program to be able to do. Whenever this happens, it is hailed as a major breakthrough.
    - anyfoo 2y ago
      Is there some circular logic in your reasoning? What is the difference between the computer program solving the conjecture, and “us” doing it?
    - lmm 2y ago
      The point is that it can complicate analysis of a program, at least if you take the fundamentalist view that all program behaviour should be provably correct. Like if you need the collantz sequence of a number or something in your program, you would just calculate it and use it, but it's surprisingly hard to prove that it always exists. Which isn't so much a problem in itself as it complicates trying to prove anything else about your program's behaviour.

anyfoo 2y ago

> 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.'" The awesome and surprising thing is, I’ve actually written such a program! It regularly runs the program to test, but stops and screams “trick program!” if the program to test did not finish within five minutes. Sadly, I haven’t been awarded my Fields Medal yet, probably because I didn’t use LLMs.