Fork me on GitHub
Math for the people, by the people.

User login

halting problem

Type of Math Object: 
Theorem
Major Section: 
Reference

Mathematics Subject Classification

03D75 no label found

Comments

I love decidability proofs. This sentence is false.

I think the proof glosses over the crucial part: How can Break refer to itself within Break's definition?

You need to use Goedel's trick somehow: first construct an algorithm B that stops if and only if its argument, interpreted as an algorithm, won't stop on its own description, and then feed the description of B to B itself.

Akin to the barber (B) who shaves everybody who doesn't shave himself. Ask whether B shaves B and it blows up.

This is true, but in this particular case it's not really a problem to gloss over the fact. Goedel's trick in this context is: find a way to encode an algorithm as a string of data that an algorithm can process. But this is exact what programming languages do. Running "Halt" on the encoded form of "Break" is not a diificult opertaion to visualize.

Of course, for a full proof, you're quite right. But if one is willing to accept that, say, Scheme is Turing-complete (easy to demonstrate: just write a Turing machine simlator) the proof is relatively straightforward.

To elaborate:

The current Break algorithm reads:

Break(x) {
if Halt(Break,x) then
while true do nothing
else
return true
fi
}

modify it to:
Break(x) {
if IsValidCode(x) and Halt(x,x) then
while true do nothing
else
return true
fi
}

This no longer references itself. Let Break be some encoding of the
program Break(x). Consider Break(Break). IsValidCode(Break) is certainly true. Now if Halt(Break,Break) is true then Break(Break) gets stuck in the while loop, so doesn't halt. If Halt(Break,Break) is false, then the if branches to the return true statement and the Break(Break) halts after all. Thus the given program Halt(x,y) is not a solution to the halting problem (since it gives the wrong result for the particular case of Break given above.)

"Running "Halt" on the encoded form of "Break" is not a diificult opertaion to visualize."

True, but programming "Break" in the first place is extremely hard to visualize. After all, the programm "Break" contains within it a representation of the program "Break"! It's not clear how to write something like that in Scheme, for instance.

Please change Break(x) in the way suggested by John Allsup below.

Break(x) {
if IsValidCode(x) and Halt(x,x) then
while true do nothing
else
return true
fi
}

Subscribe to Comments for "halting problem"