It adjusts the phrasing in a few places to make the meter flow more naturally. Apparently it also fixes a small error in the original proof, which, for the life of me, I cannot find.
I've used this poem to teach the halting problem to a variety of people for almost a decade and a half. Reading the one linked here just didn't sound right.
not being pedantic.
you can exhaustively enumerate all inputs for a program.
tautologically self-references aside, axiomatically, yes, we can determine if a program will halt, if it has a finite amount of time, or memory.
if it doesn't [have unbounded range], then it must [terminate], but it is very, very, very hard to determine if that is the case.
but not impossible.
and this nuance being lost seems so pedantic, but so integral to the claim, that I can't help but think those who repeat this sans the disclaimer, do not _truly_ understand the paradox
The very problem is that there is no algorithm that can output whether an arbitrary algorithm on a given input needs unbounded time to begin with.
>if it doesn't [have unbounded range], then it must [terminate], but it is very, very, very hard to determine if that is the case.
This is also false. You can limit the scope of the halting problem to algorithms that have a range of one single input and the halting problem is still undecidable. Heck, you can limit the halting problem to algorithms that don't even take any input whatsoever, they just have a start button and either they halt or do not halt, and that problem is still undecidable. The range has nothing to do with it.
This is useful. Verifiers which work by symbolic execution examine large numbers of cases they work through the control flow. Each case can contain a large number of states; you only need one case for each control flow pattern. Now, some programs run into combinatorial explosion when you do that. The number of cases to be examined grows rapidly. That means halting detection is NP-hard, not impossible. There's a difference.
The Microsoft Static Driver Verifier operates on the assumption that if symbolic execution doesn't terminate after a reasonable amount of automatic analysis, your driver doesn't get to run in the kernel. This is a good, practical solution.
ETA: wait that doesn't make sense because it's equivalent to computing the busy beaver number for the program under consideration. What am I missing?
[1] I'm aware there's no unique BB sequence, I don't know that the rigorous phrasing is.
A ton of useful stuff (for instance in compiler optimizers) can be done with deciding between "trivial to prove it terminates" vs. "who knows, this instance of the problem is hard! I'll just skip this optimization in this ridiculously non-representatively rare case."
You say that you are not being pedantic,
So why does that make me feel so frantic?
If we need unbounded ranges and time,
Is that in your lifetime, or possibly mine?
Someday we have to compare all our notes,
So none will have learned it only by rote.If you’re only concerned with physically realizable computing: the number of states can easily become too large to be analyzable.
Is it "obvious" you can produce program Y that doesn't halt if program X halts? Do you understand one program can be taken as input string of another? If so, the Halting Problem proof in Sudkamp's Languages and Machines, my undergraduate text in the 90s, can indeed take just a page.
Scooping the Loop Snooper: Proof That the Halting Problem Is Undecidable (2000) - https://news.ycombinator.com/item?id=20956756 - Sept 2019 (33 comments)
Scooping the Loop Snooper (2000) - https://news.ycombinator.com/item?id=10077471 - Aug 2015 (2 comments)
Assume P exists, let Q(S) be the function that takes a string S and halts if P(Q, S) returns false, otherwise it loops forever. Q(S) is not some whacky function either, in TypeScript it could be implemented as follows:
function P(A: (S: string) => void, S: string): boolean;
function Q(S: string): void {
if(P(Q, S)) {
while(true) {}
}
}
If P(Q, S) returns false, then that implies Q(S) runs forever, but by definition Q(S) halts when P(Q, S) returns false, so P was incorrect about Q(S).
If P(Q, S) returns true, then that implies Q(S) halts, but by definition Q(S) loops forever when P(Q, S) returns true, so P was incorrect about Q(S).
This exhausts all possibilities, hence our assumption that there is such a P must be false.
function HasPropertyX(A: (S: string) => void, S: string): boolean;
function Q(S: string): void {
if(HasPropertyX(Q, S)) {
AvoidHavingX();
} else {
HaveX();
}
}
function RaisesException(A: (S: string) => void, S: string): boolean;
function Q(S: string): void {
if(RaisesException(Q, S)) {
pass;
} else {
raise Exception;
}
}
function BlowsUpThePlanet(A: (S: string) => void, S: string): boolean;
function Q(S: string): void {
if(BlowsUpThePlanet(Q, S)) {
pass;
} else {
HitTheBigRedButtonAndGoKaboom();
}
}
function ReturnsTrue(A: (S: string) => boolean, S: string): boolean;
function Q(S: string): boolean {
return not ReturnsTrue(Q,S);
}
Am I getting this right? How far does this go? Is there a deeper theorem about the limitations of program checking that brings this all together?