3 ms·
Someone discovered the halting problem again. Sigh. First, the halting problem only applies to systems with infinite memory. If memory is finite and the system
by Animats 2y ago
Someone discovered the halting problem again. Sigh.
First, the halting problem only applies to systems with infinite memory. If memory is finite and the system is deterministic, the program will either halt or repeat a state. The halting problem is thus decidable for non-infinite systems. So there.
The next question is whether there are programs with lower time bounds that can be made arbitrarily large. Actually, we don't know the answer to that. Cryptography assumes the answer is yes, but that's an assumption. We don't actually know that factoring is inherently hard, only that enough people have beaten on the problem that we know there's no easy to find shortcut.
Proof of correctness systems run into the complexity problem. You can write things that force a SAT solver to explore so many cases that it won't finish in any reasonable time. But that's not undecidability. My usual comment on this is that if your program is unreasonably hard to test for termination, it's broken. Microsoft takes that position with their Static Driver Verifier. There's a timeout; if it takes too long to prove your kernel driver safe, it doesn't get signed for use in the kernel.
> A lot of people use the proof that the halting problem is undesirable to make some deep philosophical point
Penrose comes to mind. There are people who are desperate to prove that humans transcend computers in some fundamental way. We heard a lot more from that crowd before LLMs started writing better than some of their critics.
- AlotOfReading 2y agoThe next question is whether there are programs with lower time bounds that can be made arbitrarily large. It's not precisely the same as "arbitrarily large", but this is the practical result given the busy beaver function. Following from that, yedidia and Aaronson proved the existence of BBs outside of ZFC that are smaller than almost all real programs. I'd consider that essentially what you're complaining is unproven here.
- Dylan16807 2y ago> The next question is whether there are programs with lower time bounds that can be made arbitrarily large. Actually, we don't know the answer to that. Cryptography assumes the answer is yes, but that's an assumption. Cryptography does not assume that. It only needs a certain amount of slowness, and a large polynomial like n^20 is more than sufficient. But more importantly the best case for cryptographic security is exponential time. Cryptography ignores the entire science of super large numbers. To really boil down what cryptography needs, it's problems that take ≤2^40 operations to verify but ≥2^200 (irreversible) operations to solve. It doesn't actually need to scale at all. Also it's not hard to make programs that take huge amounts of time. In particular, a program that uses exponential time and leaves an exponentially long output is downright trivial to write. In pseudocode: while(i++ < 2^n) output.append(1)
- nine_k 2y ago> If memory is finite and the system is deterministic, the program will either halt or repeat a state. The halting problem is thus decidable for non-infinite systems. While this is theoretically correct, there are offensively short programs for which we can't (yet) decide if they terminate or loop infinitely. E.g. Collatz conjecture offers such a program that does not even require a colossal state to track during execution, its state is one integer. Sadly there are problems that are theoretically decidable but cannot be practically decidable, because the required computation would take the resources of the entire universe, and would take longer than it's projected to exist (at least in a state that can support computation). [1]: https://en.wikipedia.org/wiki/Collatz_conjecture https://en.wikipedia.org/wiki/Collatz_conjecture
- schoen 2y ago> E.g. Collatz conjecture offers such a program that does not even require a colossal state to track during execution, its state is one integer. Hence exactly as large as an infinite array of integers! https://en.wikipedia.org/wiki/G%C3%B6del_numbering#G%C3%B6del's_encoding https://en.wikipedia.org/wiki/G%C3%B6del_numbering#G%C3%B6de... Though I have the same intuition that the Collatz state doesn't feel large or complicated. It isn't updated, or used, in any complex way.
- whatshisface 2y ago>The halting problem is thus decidable for non-infinite systems. So there. The word "decidable" invokes a computer with infinite memory.
- lmm 2y ago> First, the halting problem only applies to systems with infinite memory. If memory is finite and the system is deterministic, the program will either halt or repeat a state. The halting problem is thus decidable for non-infinite systems. So there. The article mentions this fact specifically in about the third paragraph, and goes on to talk about why it's less relevant than it might appear. > The next question is whether there are programs with lower time bounds that can be made arbitrarily large. Actually, we don't know the answer to that. No, the time hierarchy theorems prove that such programs exist. > My usual comment on this is that if your program is unreasonably hard to test for termination, it's broken. Microsoft takes that position with their Static Driver Verifier. There's a timeout; if it takes too long to prove your kernel driver safe, it doesn't get signed for use in the kernel. Timeouts make it much harder to reason about programs and perform safe refactors, because the class of refactors that are guaranteed to not break a program becomes quite small. E.g. you can no longer prove that "val y = f(x); g(y)" is correct if "g(f(x))" is correct and vice versa.
- taneq 2y ago> There's a timeout; if it takes too long to prove your kernel driver safe, it doesn't get signed Ah, but what if it takes too long next time? :D
- Tainnor 2y ago> The halting problem is thus decidable for non-infinite systems. That's only true in the most boring way possible, i.e. because every system must eventually halt in a universe where the laws of thermodynamics hold. If you replace "halts" with "halts in a reasonable amount of time" (for whatever value you consider reasonable), you'll find that the same diagonalisation argument shows that no algorithm can decide in a reasonable amount of time whether some arbitrary program halts in a reasonable amount of time.