Scooping the Loop Snooper (2000)
lel.ed.ac.uk
Scooping the Loop Snooper (2000)
1–10 of 18 posts
Re: Scooping the Loop Snooper (2000)
#2[deleted]
Re: Scooping the Loop Snooper (2000)
#3Diagonalizations 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.
Re: Scooping the Loop Snooper (2000)
#4Suppose 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.
Re: Scooping the Loop Snooper (2000)
#5The 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."
Re: Scooping the Loop Snooper (2000)
#6Suppose 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.
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
Re: Scooping the Loop Snooper (2000)
#7Sweet 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 :)
Re: Scooping the Loop Snooper (2000)
#8Obligatory 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.
Re: Scooping the Loop Snooper (2000)
#9Suppose 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.
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
No, in fact you can use oracles to prove the halting problem.
Re: Scooping the Loop Snooper (2000)
#10I've been working on a proof for a long time, but I'm just not sure if I'll finish it...