Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Did Turing prove the undecidability of the halting problem?

arxiv.org

Post reply on HN
Print view View original

11–20 of 116 posts

Re: Did Turing prove the undecidability of the halting problem?

#11

Post by frabert »

indolering wrote: post #8
FartyMcFarter wrote: post #7

Earlier 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, if you start writing your program with the explicit intent of making such proofs possible, then it can be done. What Rice's theorem says is that you can't expect to be able to do so when given an arbitrary program, not that it's always impossible.

Re: Did Turing prove the undecidability of the halting problem?

#12

Post by darby_nine »

indolering wrote: post #8
FartyMcFarter wrote: post #7

Earlier 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…

Man I feel like I'm missing something. Figuring out whether a single given program halts is decidable, it's figuring out an arbitrary unknown problem (or all of them rather) that is undecidable. So you can formally verify programs but you can't formally verify all programs with the same algorithm.

Secondly, what do you mean by the idea that quantum computation makes the problem decidable? This isn't a complexity class issue, and my understanding is that quantum computation can't compute anything that turing machines can't, they just are able to compute certain algorithms faster. Am i wrong? Among other things we can simulate quantum computers on turing machines, just without the complexity advantages.

Like think about what you're saying: of course we can prove that "exit(0)" halts, it'd be absurd to say otherwise. So we're clearly referring to a harder problem—proving whether arbitrary programs halt with a single algorithm in finite time.

If it helps, Roger Penrose misunderstood the halting problem and basically said "humans aren't practically constrained by godel's incompleteness theorems (equivalent to the halting problem I believe) so consciousness is quantum". This might yet be true but human computers are still bound by the same computational constraints computer's are.

It's been a bit since my computer theory courses so apologies for any botched terminology or understanding.

Re: Did Turing prove the undecidability of the halting problem?

#13

Post by lisper »

This is ridiculous academic click-bait. Here is a quote from Turing's 1936 paper:

"If a computing machine never writes down more than a finite number of symbols of the first kind [i.e. 0 or 1], it will be called circular. Otherwise it is said to be circle-free."

He then goes on to prove that "circularity" as he has defined it is undecidable.

So no, he never defines "halting", he just talks about whether or not a machine ever prints a finite number of 1's and 0's. Showing that these questions are equivalent is an elementary exercise.

He also proves that "there can be no machine £ which, when supplied with the S.D of an arbitrary machine AV, will determine vhether AV ever prints a given symbol (0 say)." Which, again, is trivially equivalent to the question of whether or not the machine ever enters a particular privileged state.

Saying that Turing's paper was not about the halting problem because it doesn't use the word "halt" is like saying that the EPR paper was not about entanglement because it doesn't use the word "entangled".

Re: Did Turing prove the undecidability of the halting problem?

#14

Post by lou1306 »

tsimionescu wrote: post #10
indolering wrote: post #8

Earlier quoted context omitted.

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 see…

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

Re: Did Turing prove the undecidability of the halting problem?

#17

Post by bionhoward »

darby_nine wrote: post #12
indolering wrote: post #8

Earlier quoted context omitted.

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…

Man I feel like I'm missing something. Figuring out whether a single given program halts is decidable, it's figuring out an arbitrary unknown problem (or all of them rather) that is undecidable. So you can formally verify programs but you can't formally verify all programs with the same algorithm. Secondly, what do you mean by the idea that quantum computation makes the problem decidable? This isn't a complexity clas…

Relevant video about MIP*=RE

https://youtu.be/2H8629BCbkM

Re: Did Turing prove the undecidability of the halting problem?

#18

Post by tromp »

lisper wrote: post #13

This is ridiculous academic click-bait. Here is a quote from Turing's 1936 paper: "If a computing machine never writes down more than a finite number of symbols of the first kind [i.e. 0 or 1], it will be called circular. Otherwise it is said to be circle-free." He then goes on to prove that "circularity" as he has defined it is undecidable. So no, he never defines "halting", he just talks about whether or not a mach…

> Showing that these questions are equivalent is an elementary exercise.

Do you mean that there's a simple computable mapping f from TMs as Turing defined them to TMs which can halt such that machine m prints finitely many 0s/1s iff f(m) halts?

Re: Did Turing prove the undecidability of the halting problem?

#19

Post by arethuza »

darby_nine wrote: post #12
indolering wrote: post #8

Earlier quoted context omitted.

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…

Man I feel like I'm missing something. Figuring out whether a single given program halts is decidable, it's figuring out an arbitrary unknown problem (or all of them rather) that is undecidable. So you can formally verify programs but you can't formally verify all programs with the same algorithm. Secondly, what do you mean by the idea that quantum computation makes the problem decidable? This isn't a complexity clas…

Also worth noting that, from a practical perspective, even very simple programs/TMs can exhibit very complex behaviours that make it difficult to work out whether they will actually halt or not.

At the time of writing there are 2833 5 state binary TMs that haven't been decided yet:

https://github.com/bbchallenge/bbchallenge-undecided-index/b...

Re: Did Turing prove the undecidability of the halting problem?

#20

Post by PaulHoule »

My grad school mate Ron Maimon one day told me in a bar about the problem of computable numbers in a way that made him sound like a serious crackpot. I thought about it enough to conclude that the “real” numbers were “phony” numbers because unlike the integers or rationals most of them don’t have a name and can’t be referred to specifically.

I found out later that Turing had introduced the computable numbers idea and that was the work he had really done as opposed to the modern formulation of the halting problem.

As for Ron he really descended into conspiracy theory insanity and got kicked off Quora because he was saying the Boston bombing was an inside job. I still wish Steve Wolfram would grow some balls, take his constructivist program seriously, and reject the axiom of choice.

Post reply on HN