7 ms·
Scooping the Loop Snooper (2000)
- beders 2y agoSweet poem. I remember being blown away when I studied computer science. The whole idea that there are inherit limits to computing on Turing machines seemed crazy. Gödel's incompleteness theorems has a similar proof that will mess with your brain :)
- srcreigh 2y agoObligatory mention that although Halt doesn’t exist for arbitrary P, there are Halt_N for every natural N where Halt_N works on empty-input TMs with at most N states. Undecidability is more about compression than it is about whether we can determine if TMs halt.
- snarkconjecture 2y agoFor sufficiently large N, it's impossible to prove Halt_N correct. (The N required depends on your axioms.)
- VikingCoder 2y agoI've been working on a proof for a long time, but I'm just not sure if I'll finish it...
- dang 2y agoRelated: Scooping the Loop Snooper (2000) - https://news.ycombinator.com/item?id=30783422 https://news.ycombinator.com/item?id=30783422 - March 2022 (31 comments) Scooping the Loop Snooper: Proof That the Halting Problem Is Undecidable (2000) - https://news.ycombinator.com/item?id=20956756 https://news.ycombinator.com/item?id=20956756 - Sept 2019 (33 comments) Scooping the Loop Snooper (2000) - https://news.ycombinator.com/item?id=10077471 https://news.ycombinator.com/item?id=10077471 - Aug 2015 (2 comments)
- fragmede 2y agoso, for classes of problem where it's been talked about enough in the training data, gpt 4 manages to solve the halting problem.
- flanfly 2y agoI quoted this, in full, in my MSc thesis. It's both a light hearted introduction to the Halting Problem and something you need to reference quite often when writing about static program analysis. Good times.
- vincent-manis 2y agoBut he rhymed “data” (in British pronunciation, “dattah”) with “later”!
- aaron695 2y ago[dead]
- deleted 2y ago[deleted]
- skulk 2y agoDiagonalizations are some of the easiest to understand, yet most profound proofs in math. Another example is the proof that any continuum is larger in cardinality than the set of integers. https://en.m.wikipedia.org/wiki/Diagonal_argument https://en.m.wikipedia.org/wiki/Diagonal_argument
- g___ 2y agoSuppose O is the oracle for the halting problem. We create a machine: given a program P, ask O whether P halts given input P and negate the answer. λP. ~O (P P) Now we ask whether this machine will halt given its own source code as input. In symbols: (λP. ~O (P P)) (λP. ~O (P P)) which is the Y-combinator in lambda calculus.
- thedudeabides5 2y agoaren't oracles, just attempts to escape the halting problem? assume you have an O which doesn't halt now feed P which DOES halt into O oh look it catches it! misses the boat
- bongodongobob 2y agoNo, in fact you can use oracles to prove the halting problem.
- QuinnyPig 2y agoThe halting problem--a tough endeavor "Will the loop complete or run forever?" Many fixes were attempted (Lambda's 15 minute limit doesn't get exempted) You'll quickly find there is no winning As the LOADING ball keeps spinning To date there remains a single hack: Rip the cable out the back You'll have an answer clarified: "The loop is done; the power died."
- QuinnyPig 2y ago...this comment made a lot more sense when the title was "a poem about the halting problem." Now I just look more deranged than I usually do.
- stainforth 2y agoIs your name an anagram for PunnyQuip