[HN Gopher] Scooping the Loop Snooper (2000)
___________________________________________________________________
Scooping the Loop Snooper (2000)
Author : soferio
Score : 76 points
Date : 2024-04-23 22:42 UTC (1 days ago)
(HTM) web link (www.lel.ed.ac.uk)
(TXT) w3m dump (www.lel.ed.ac.uk)
| skulk wrote:
| Diagonalizations 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
| g___ wrote:
| Suppose 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.
|
| lP. ~O (P P)
|
| Now we ask whether this machine will halt given its own source
| code as input. In symbols:
|
| (lP. ~O (P P)) (lP. ~O (P P))
|
| which is the Y-combinator in lambda calculus.
| thedudeabides5 wrote:
| aren'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 wrote:
| No, in fact you can use oracles to prove the halting problem.
| QuinnyPig wrote:
| The 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 wrote:
| ...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 wrote:
| Is your name an anagram for PunnyQuip
| beders wrote:
| Sweet 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.
|
| Godel's incompleteness theorems has a similar proof that will
| mess with your brain :)
| srcreigh wrote:
| Obligatory 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 wrote:
| For sufficiently large N, it's impossible to prove Halt_N
| correct.
|
| (The N required depends on your axioms.)
| VikingCoder wrote:
| I've been working on a proof for a long time, but I'm just not
| sure if I'll finish it...
| dang wrote:
| Related:
|
| _Scooping the Loop Snooper (2000)_ -
| 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 - Sept 2019 (33
| comments)
|
| _Scooping the Loop Snooper (2000)_ -
| https://news.ycombinator.com/item?id=10077471 - Aug 2015 (2
| comments)
| flanfly wrote:
| I 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.
| fragmede wrote:
| so, for classes of problem where it's been talked about enough in
| the training data, gpt 4 manages to solve the halting problem.
| vincent-manis wrote:
| But he rhymed "data" (in British pronunciation, "dattah") with
| "later"!
___________________________________________________________________
(page generated 2024-04-24 23:02 UTC)