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)
Gödel's incompleteness theorems has a similar proof that will mess with your brain :)
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.
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
"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."
Undecidability is more about compression than it is about whether we can determine if TMs halt.
(The N required depends on your axioms.)