Is that actually proven?
Or is it possible that in fact, there might be an efficient algorithm for solving the halting problem in practice for computers, but it's just that we haven't discovered it yet?
Just because the state space is big doesn't mean that there aren't shortcuts to figure out in a much more efficient way whether a program loops forever.
It seems incredibly likely that this question has a complexity of O(exp(N)) which very quickly makes the halting problem infeasible to solve for modern computers.
That's an oxymoron, because Turing machines have a state space of infinite bits by definition. I understand you mean "deterministic finite-state machines" rather than "Turing machines".
> It seems incredibly likely that this question has a complexity of O(exp(N)) which very quickly makes the halting problem infeasible to solve for modern computers.
I mean, I agree that it's likely, but again, is this proven?
I'm not aware that it is and therefore I think this is actually missing many of the points I mentioned.
It could be false for all we know.
I meant "Turing machines with X states and a type limited to Y bits, with X + Y = N". You can, of course, cast those as Deterministic Finite State Machines, but that will require incredibly many states.
Could we solve it without brute force? Well, there are plenty of math problems we can’t prove; we can write a program that only halts if counter example is found, and we would be unable to prove if the program halts. We can also write program that will halt if it can prove ZF set theory is false, but we already know it’s impossible to prove that (it only possible to prove it is false). So symbolically deciding if a program halts is also impossible in the general case.
Yes, but again, you're missing my point: you would be able to prove if the program halts.
It's just that in this particular case it would not necessarily be useful, because it just might happen that to solve the mathematical problem it would require more memory than you have available.
So if the halting detector says: "the program halted due to running out of memory", the results would be inconclusive for answering a difficult mathematical problem.
But that's not what most programs do, in fact, the vast majority of programs would benefit immensely from knowing whether they will exceed some finite memory limit.
> We can also write program that will halt if it can prove ZF set theory is false, but we already know it’s impossible to prove that (it only possible to prove it is false).
The same point above applies.
> So symbolically deciding if a program halts is also impossible in the general case.
No, it's not. You completely missed my point. It is 100% decidable. It's only undecidable if you're imagining running this program on an imaginary machine which cannot physically be constructed.
Attempting to overflow it is impractical using cpu cache memory sizes, no hard drive needed. No matter how fast you go through states, there are too many possible states in the cpu, and too many states even a small program can iterate through while still eventually terminating.
What limitations of math exactly? What you're talking about is not related to efficiency of solving the Halting problem on a machine with a finite number of states.
> Attempting to overflow it is impractical using cpu cache memory sizes, no hard drive needed. No matter how fast you go through states, there are too many possible states in the cpu, and too many states even a small program can iterate through while still eventually terminating.
You are assuming that you have to simulate going through all the running states of a program to determine whether it halts or not.
Why do you assume that you have to run a complete simulation of the program to analyze it?
see if you follow this one one, for a real computer:
Suppose I pick a n bit key, and encrypt a phrase with it. I will provide you the plain text phrase and either a real or fake cipher text. You have to determine if a program which loops through all the keys will decrypt the ciphertext into a the phrase.
Either you know weaknesses in the crypto system, or you have no choice but to iterate though each key to see if the output matches the phrase.
There is a relationship with proof of work crypto as well. Even all the Bitcoin mining has trouble finding hashes with a certain number of leading zeroes, add a few more zeros and no one will ever find a working seed again. There is no way to speed up the process beyond iterating over the seeds.
You can tie this to the halting problem by just saying to go back the key 0 once the key space is exhausted.
> There is a relationship with proof of work crypto as well. Even all the Bitcoin mining has trouble finding hashes with a certain number of leading zeroes, add a few more zeros and no one will ever find a working seed again.
Yup, I know. But here's the part I think you're missing:
None of those crypto systems you're mentioning are proven not to have weaknesses. In fact, weaknesses in hashing and encryption algorithms are encountered every now and then, even for those that have been considered state-of-the-art.
So yes, I agree that in practice we don't know how to solve this problem efficiently yet. Which means it's currently impractical, and would currently requiring brute forcing through all the states.
But I haven't seen a proof that it's not possible to find a practical algorithm.
There are also lesser problems that have been around a while which we haven’t been able to prove, but might be provable… you can iterate over numbers looking for an counter example to the Collatz conjecture… I think that’s the best example of a simple program that is outside our current knowledge of math (better than the crypto one), but maybe someday we will have an answer.