3 ms·

> When Turing proved the halting problem was undecidable - that there is no program that can decide whether another program will ever finish Turing didn't prov

by qiskit 5y ago

> When Turing proved the halting problem was undecidable - that there is no program that can decide whether another program will ever finish Turing didn't prove the halting problem was undecidable. The halting problem was defined after Turing's death by Martin Davis. It's a common misunderstanding people have. Turing's definition of Turing Machines classified machines that halted as circular/unsatisfactory. Turing wanted his machine to run forever ( circle-free/satisfactory ). > Personally, I think we should set aside Gödel’s original number-theory-based proof as an artifact of history, the way we no longer use Isaac Newton’s original notation for calculus. We also don't teach Turing's version either. No computer science class teaches real Turing. It's been reformulated to a point Turing would barely recognize it. Also, you can't understand the halting problem or Turing without "number-theory-based proof" as "number based proof" and godel numbering is at the heart of turing machines ( look up what descriptive numbers ) are. > We should accept that the concepts of mathematical proof and computer algorithms are intertwined at their heart Computer algorithms are mathematical algorithms. Mathematicians have been using computers/algorithms to derive theorems from axioms since at least the 1950s. You are saying we should accept what everyone already accepts and have accepted for decades.

JadeNB 5y ago
> We also don't teach Turing's version either. No computer science class teaches real Turing. It's been reformulated to a point Turing would barely recognize it. I think that this is true of most long-lived subjects taught in a modern science course. Imagine Euclid's puzzlement at all the things that are now called Euclidean! > Also, you can't understand the halting problem or Turing without "number-theory-based proof" as "number based proof" and godel numbering is at the heart of turing machines ( look up what descriptive numbers ) are. Since you say most of what one learns in a CS course isn't directly about Turing's original work, I don't want to speak to that, but I think that it is possible to understand the halting problem, and even its undecidability, without number theory. It arguably isn't possible to understand the halting problem without some notion of encoding (of the data that constitute a Turing machine in a form that can itself be processed by a Turing machine), but there's no reason that encoding has to be number-theoretic. (I speak here as a number theorist—it's a neat application, just much more important for incompleteness than for halting.)
- qiskit 5y ago
  > It arguably isn't possible to understand the halting problem without some notion of encoding (of the data that constitute a Turing machine in a form that can itself be processed by a Turing machine) You can understand the halting problem without math. You can explain it logically. But the halting problem has nothing to do with Turing. As I stated, the halting problem was invented/discovered by someone else years after Turing's death. We don't need Turing or the Turing machine to understand undecidability since Alonzo Church already proved undecidability before Turing. > but there's no reason that encoding has to be number-theoretic Sure. Turing encoded to the standard description ( letters ) and to description numbers. But number theory is necessary if you want to follow Turing's approach since you need to show for starters that turing machines and computable numbers are enumerable.
lacker 5y ago
Turing didn't prove the halting problem was undecidable. The halting problem was defined after Turing's death by Martin Davis. Really? I did not include a reference link here but I grabbed the dates from Wikipedia, which states: Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist. https://en.wikipedia.org/wiki/Halting_problem https://en.wikipedia.org/wiki/Halting_problem Obviously Wikipedia is not the end-all be-all of mathematical sources, but I'd be curious to see a source that contradicts it here.
- chalst 5y ago
  The Wikipedia article is sound and it also documents that Martin Davis came up with the term "halting problem" for a lecture he gave in 1952. He used Turing machines in his 1958 book. Turing machines are still a commonly used formalism in some areas of theoretical computer science.
mirceal 5y ago
lol no https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf I'll let you guess what Entscheidungsproblem means.

by qiskit 5y ago

JadeNB 5y ago

> We also don't teach Turing's version either. No computer science class teaches real Turing. It's been reformulated to a point Turing would barely recognize it. I think that this is true of most long-lived subjects taught in a modern science course. Imagine Euclid's puzzlement at all the things that are now called Euclidean! > Also, you can't understand the halting problem or Turing without "number-theory-based proof" as "number based proof" and godel numbering is at the heart of turing machines ( look up what descriptive numbers ) are. Since you say most of what one learns in a CS course isn't directly about Turing's original work, I don't want to speak to that, but I think that it is possible to understand the halting problem, and even its undecidability, without number theory. It arguably isn't possible to understand the halting problem without some notion of encoding (of the data that constitute a Turing machine in a form that can itself be processed by a Turing machine), but there's no reason that encoding has to be number-theoretic. (I speak here as a number theorist—it's a neat application, just much more important for incompleteness than for halting.)

qiskit 5y ago
> It arguably isn't possible to understand the halting problem without some notion of encoding (of the data that constitute a Turing machine in a form that can itself be processed by a Turing machine) You can understand the halting problem without math. You can explain it logically. But the halting problem has nothing to do with Turing. As I stated, the halting problem was invented/discovered by someone else years after Turing's death. We don't need Turing or the Turing machine to understand undecidability since Alonzo Church already proved undecidability before Turing. > but there's no reason that encoding has to be number-theoretic Sure. Turing encoded to the standard description ( letters ) and to description numbers. But number theory is necessary if you want to follow Turing's approach since you need to show for starters that turing machines and computable numbers are enumerable.

lacker 5y ago

Turing didn't prove the halting problem was undecidable. The halting problem was defined after Turing's death by Martin Davis. Really? I did not include a reference link here but I grabbed the dates from Wikipedia, which states: Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist. https://en.wikipedia.org/wiki/Halting_problem https://en.wikipedia.org/wiki/Halting_problem Obviously Wikipedia is not the end-all be-all of mathematical sources, but I'd be curious to see a source that contradicts it here.

chalst 5y ago
The Wikipedia article is sound and it also documents that Martin Davis came up with the term "halting problem" for a lecture he gave in 1952. He used Turing machines in his 1958 book. Turing machines are still a commonly used formalism in some areas of theoretical computer science.

mirceal 5y ago

lol no https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf I'll let you guess what Entscheidungsproblem means.