Did Turing prove the undecidability of the halting problem?
1–10 of 116 posts
Re: Did Turing prove the undecidability of the halting problem?
#2[flagged]
Re: Did Turing prove the undecidability of the halting problem?
#3It's interesting indeed that Turing's machines as he defined them can never halt:
> he does not discuss the halting of his machines at all, and makes no provision for the computational processes undertaken by his machines ever to stop; in particular, he has no convention as in contemporary accounts of a halt state for the machines
So instead of asking whether they halt, Turing asked whether they ever print a particular symbol. Of course one could call that symbol the halting symbol, and adopt the convention that printing the halting symbol amounts to halting. So while Turing did not name it the "Halting Problem" he proved an obviously equivalent result.
Re: Did Turing prove the undecidability of the halting problem?
#4[deleted]
Re: Did Turing prove the undecidability of the halting problem?
#5It's interesting indeed that Turing's machines as he defined them can never halt: > he does not discuss the halting of his machines at all, and makes no provision for the computational processes undertaken by his machines ever to stop; in particular, he has no convention as in contemporary accounts of a halt state for the machines So instead of asking whether they halt, Turing asked whether they ever print a particul…
[deleted]
Re: Did Turing prove the undecidability of the halting problem?
#6It's interesting indeed that Turing's machines as he defined them can never halt: > he does not discuss the halting of his machines at all, and makes no provision for the computational processes undertaken by his machines ever to stop; in particular, he has no convention as in contemporary accounts of a halt state for the machines So instead of asking whether they halt, Turing asked whether they ever print a particul…
Note, the origins are stated in Wikipedia:
> Many papers and textbooks refer the definition and proof of undecidability of the halting problem to Turing's 1936 paper. However, this is not correct.[19][24] Turing did not use the terms "halt" or "halting" in any of his published works, including his 1936 paper.[25] A search of the academic literature from 1936 to 1958 showed that the first published material using the term “halting problem” was Rogers (1957). However, Rogers says he had a draft of Davis (1958) available to him,[19] and Martin Davis states in the introduction that "the expert will perhaps find some novelty in the arrangement and treatment of topics",[26] so the terminology must be attributed to Davis.[ https://en.wikipedia.org/wiki/Halting_problem#Origin_of_the_...
Re: Did Turing prove the undecidability of the halting problem?
#7It's interesting indeed that Turing's machines as he defined them can never halt: > he does not discuss the halting of his machines at all, and makes no provision for the computational processes undertaken by his machines ever to stop; in particular, he has no convention as in contemporary accounts of a halt state for the machines So instead of asking whether they halt, Turing asked whether they ever print a particul…
I think Rice's theorem implies that proving the undecidability of the halting problem is equivalent to proving the undecidability of any other non-trivial semantic property of a program (*). So this discussion is basically just splitting hairs as you said.
https://en.wikipedia.org/wiki/Rice%27s_theorem#Proof_by_redu...
(*) > Rice's theorem states that all non-trivial semantic properties of programs are undecidable. A semantic property is one about the program's behavior (for instance, "does the program terminate for all inputs?"), unlike a syntactic property (for instance, "does the program contain an if-then-else statement?"). A non-trivial property is one which is neither true for every program, nor false for every program.
Re: Did Turing prove the undecidability of the halting problem?
#8It's interesting indeed that Turing's machines as he defined them can never halt: > he does not discuss the halting of his machines at all, and makes no provision for the computational processes undertaken by his machines ever to stop; in particular, he has no convention as in contemporary accounts of a halt state for the machines So instead of asking whether they halt, Turing asked whether they ever print a particul…
I think Rice's theorem implies that proving the undecidability of the halting problem is equivalent to proving the undecidability of any other non-trivial semantic property of a program (*). So this discussion is basically just splitting hairs as you said. https://en.wikipedia.org/wiki/Rice%27s_theorem#Proof_by_redu... (*) > Rice's theorem states that all non-trivial semantic properties of programs are undecidable. A…
I kinda hate that people dress up this analysis as a theorem. We have lots of formally verified programs that show useful work can be done here. And even if we can't prove most of it, high assurance methods are very useful for preventing fuckery. I can't mathematically prove any lock is unpickable. But I can use a lock advanced enough that the cost of picking it becomes absurd.
Also, theoretical quantum computers can solve whether a problem halts 100% of the time. So Rice's Theorem is theoretically meaningless.
Re: Did Turing prove the undecidability of the halting problem?
#9It's interesting indeed that Turing's machines as he defined them can never halt: > he does not discuss the halting of his machines at all, and makes no provision for the computational processes undertaken by his machines ever to stop; in particular, he has no convention as in contemporary accounts of a halt state for the machines So instead of asking whether they halt, Turing asked whether they ever print a particul…
Note, the origins are stated in Wikipedia: > Many papers and textbooks refer the definition and proof of undecidability of the halting problem to Turing's 1936 paper. However, this is not correct.[19][24] Turing did not use the terms "halt" or "halting" in any of his published works, including his 1936 paper.[25] A search of the academic literature from 1936 to 1958 showed that the first published material using the…
The paper in the OP discusses this claim in section 3, and mentions that Kleene came even before that:
> We would note that Kleene seems, however, to have already had the self-referential argument earlier in his classic book from 1952, Introduction to Metamathematics
They also bring up the "symbol-printing problem" present in Turing's 1936 paper, which is trivially equivalent to the halting problem with today's hindsight. That paper has a well nuanced take with a lot of interesting information.
Re: Did Turing prove the undecidability of the halting problem?
#10Earlier quoted context omitted.
I think Rice's theorem implies that proving the undecidability of the halting problem is equivalent to proving the undecidability of any other non-trivial semantic property of a program (*). So this discussion is basically just splitting hairs as you said. https://en.wikipedia.org/wiki/Rice%27s_theorem#Proof_by_redu... (*) > Rice's theorem states that all non-trivial semantic properties of programs are undecidable. A…
I kinda hate that people dress up this analysis as a theorem. We have lots of formally verified programs that show useful work can be done here. And even if we can't prove most of it, high assurance methods are very useful for preventing fuckery. I can't mathematically prove any lock is unpickable. But I can use a lock advanced enough that the cost of picking it becomes absurd. Also, theoretical quantum computers can…
> We have lots of formally verified programs that show useful work can be done here.
Yes, by restricting things to a non-Turing Complete subset.
> Also, theoretical quantum computers can solve whether a problem halts 100% of the time.
That is absolutely not true. Quantum computers are proven to be entirely equivalent to classical computers in terms of what problems they can solve. The only difference is that they seem to show an exponential speed advantage for a certain very limited subset of problems, mostly related to quantum transforms.