11–20 of 34 posts
assuming unbounded time and memory. 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 nua…
I don’t follow this proof. If Q takes an executable program, then Q(x) is executable, but Q alone isn’t. So you can ask questions about Q(Q(x)), but Q(Q) shouldn’t type check, as the inner Q isn’t executable without an argument. Am I being dumb? How would you do this proof with types?
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.
I don’t follow this proof. If Q takes an executable program, then Q(x) is executable, but Q alone isn’t. So you can ask questions about Q(Q(x)), but Q(Q) shouldn’t type check, as the inner Q isn’t executable without an argument. Am I being dumb? How would you do this proof with types?
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.
assuming unbounded time and memory. 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 nua…
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.
I don’t follow this proof. If Q takes an executable program, then Q(x) is executable, but Q alone isn’t. So you can ask questions about Q(Q(x)), but Q(Q) shouldn’t type check, as the inner Q isn’t executable without an argument. Am I being dumb? How would you do this proof with types?
Define P(A, S) as the function that takes as input an algorithm A and a string S and returns true if A(S) halts, and false if A(S) does not halt. The claim is that P does not exist. 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: s…
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)
Pullum keeps a slightly updated version of this poem on his website: http://www.lel.ed.ac.uk/~gpullum/loopsnoop.html 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…
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.