from Hacker News

Scooping the Loop Snooper (2000)

by soferio on 4/23/24, 10:42 PM with 15 comments

• by dang on 4/24/24, 4:08 AM

  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)

• by skulk on 4/23/24, 11:24 PM

  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

• by beders on 4/23/24, 11:45 PM

  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.

  Gödel's incompleteness theorems has a similar proof that will mess with your brain :)

• by g___ on 4/23/24, 11:30 PM

  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.

  λ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.

• by QuinnyPig on 4/23/24, 11:35 PM

  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."

• by flanfly on 4/24/24, 9:31 AM

  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.

• by VikingCoder on 4/24/24, 12:00 AM

  I've been working on a proof for a long time, but I'm just not sure if I'll finish it...

• by vincent-manis on 4/24/24, 9:20 PM

  But he rhymed “data” (in British pronunciation, “dattah”) with “later”!

• by fragmede on 4/24/24, 9:35 AM

  so, for classes of problem where it's been talked about enough in the training data, gpt 4 manages to solve the halting problem.

• by srcreigh on 4/23/24, 11:46 PM

  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.