7 ms·

It'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 provis

by tromp 2y ago

It'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.

deleted 2y ago
[deleted]
tinganho 2y ago
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_halting_problem https://en.wikipedia.org/wiki/Halting_problem#Origin_of_the_...
- syrak 2y ago
  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.
FartyMcFarter 2y ago
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_reduction_from_the_halting_problem 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.
- indolering 2y ago
  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.
  - tsimionescu 2y ago
    > 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.
    - lou1306 2y ago
      > Yes, by restricting things to a non-Turing Complete subset. No, not necessarily. There are procedures that _can_ verify properties against Turing-complete and even infinite-state systems. It's just that no _general_ (as in, sound and complete) procedure can exist.
spiritbear14 2y ago
This version makes more sense to me. When the halting problem was first explained to me in school the professor didn't get into what it actually meant in terms of computability, just that we couldn't tell if a program halted or not then we just moved on.
chuckadams 2y ago
I actually like the symbol phrasing, it's more general than halting. You can't prove that any arbitrary program that can be in state X will ever actually reach state X. Besides, I feel like https://xkcd.com/1266/ https://xkcd.com/1266/ is relevant :)

by tromp 2y ago

deleted 2y ago

[deleted]

tinganho 2y ago

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_halting_problem https://en.wikipedia.org/wiki/Halting_problem#Origin_of_the_...

syrak 2y ago
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.

FartyMcFarter 2y ago

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

indolering 2y ago
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.
- tsimionescu 2y ago
  > 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.
  - lou1306 2y ago
    > Yes, by restricting things to a non-Turing Complete subset. No, not necessarily. There are procedures that _can_ verify properties against Turing-complete and even infinite-state systems. It's just that no _general_ (as in, sound and complete) procedure can exist.

spiritbear14 2y ago

This version makes more sense to me. When the halting problem was first explained to me in school the professor didn't get into what it actually meant in terms of computability, just that we couldn't tell if a program halted or not then we just moved on.

chuckadams 2y ago

I actually like the symbol phrasing, it's more general than halting. You can't prove that any arbitrary program that can be in state X will ever actually reach state X. Besides, I feel like https://xkcd.com/1266/ https://xkcd.com/1266/ is relevant :)