Hacker News new | ask | show | jobs
by ryangs 715 days ago
Right - it is saying that there is no algorithm to do this in general. Any specific instance may have a solution.
1 comments

It's a little more impactful than that. Have a look at Z3, Boogie, Dafny, and similar technologies to see practical application of what I mean. It boils down to there being "non-general" algorithms that still work for virtually every input you're ever going to give them. A hypothetical algorithm that decides the halting problem for 99.9999999% of programs would not violate the impossibility proof.

The limit case is maybe interesting. What about the algorithm that decides the halting problem for every program except for one? Does the impossibility proof prohibit such an algorithm? Does it make a difference if the identity of the unique program is known or unknown?

And then of course there is classic pen and paper hand derivation like the old guard (Knuth and his peers) did. The claim that that is following an algorithm is yet to be proved or disproved.

With a little massaging of input and output you can convert any program P into the program P_n defined as "repeat P n times".

For any n P terminate if and only if P_n terminates, so no general procedure can decide the halting problem for all programs except 1.