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

21–30 of 116 posts

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

#21

Post by lisper »

tromp wrote: post #18
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?

No. In fact, my guess is that you can prove there is no such function. But (and I confess I have not thought this all the way through so I might be wrong) while producing such a mapping would be sufficient to carry out the equivalence proof (if it were possible, which I suspect it is not) it is not necessary. All that is necessary (I think) is to show that if a machine is non-circular, then it is possible to produce an equivalent machine by using a halting state which is entered after the machine prints its final "symbol of the first kind". And that seems like it should not be hard, though I concede I may have overstated my case by calling it trivial.

(You also have to prove the opposite, that a machine with a halting state can be converted into a Turing-style TM, but that really is obviously trivial.)

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

#22

Post by mafuy »

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…

I would like to add that even deciding if a particular single program halts can be undecidable. At least in PA or ZFC, and I don't think there is a better math framework.

There was a pretty cool Bachelor's thesis (I think? Can't recall) that that used this fact to show that busy beavers beyond some point cannot be determined.

And even without any trickery, deciding single program halting can be extremely hard. For instance, the 3x+1 problem is as trivial to write as fizzbuzz but noone can figure out if it halts.

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

#23

Post by enugu »

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…

Quantum computers can't solve the halting problem but that is not Penrose's argument which is not summarized well in the quote.

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

#24

Post by tromp »

lisper wrote: post #21
tromp wrote: post #18

Earlier quoted context omitted.

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

No. In fact, my guess is that you can prove there is no such function. But (and I confess I have not thought this all the way through so I might be wrong) while producing such a mapping would be sufficient to carry out the equivalence proof (if it were possible, which I suspect it is not) it is not necessary. All that is necessary (I think) is to show that if a machine is non-circular, then it is possible to produce…

> to show that if a machine is non-circular, then it is possible to produce an equivalent machine by using a halting state which is entered after the machine prints its final "symbol of the first kind".

This looks rather impossible to me. Yet you claim

> And that seems like it should not be hard

Could you elaborate how to do so?

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

#25

Post by arethuza »

mafuy wrote: post #22
darby_nine wrote: post #12

Earlier quoted context omitted.

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…

I would like to add that even deciding if a particular single program halts can be undecidable. At least in PA or ZFC, and I don't think there is a better math framework. There was a pretty cool Bachelor's thesis (I think? Can't recall) that that used this fact to show that busy beavers beyond some point cannot be determined. And even without any trickery, deciding single program halting can be extremely hard. For in…

Was it this one?

https://scottaaronson.blog/?p=2725

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

#26

Post by less_less »

tromp wrote: post #18
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?

I think you'd want the reverse, which is indeed elementary: if f halts then you get a circle-free TM, but if f does not halt then you get a non-circle-free TM. This can be done by

  f(); while(1) output_digit(0);
or any number of other simple constructions. This is because a circle-free TM always reaches a certain pre-defined event (output_digit), much like a halting TM. But a non-circle-free TM might forever fail to make progress, in a way that you can't necessarily tell if it's stuck or will eventually output another digit, much like a non-halting TM.

Edited to add: also Turing proved that the symbol-printing problem is undecidable, as the authors of this paper describe: will a Turing machine ever print a certain symbol? If you name the symbol in question "HALT" then this is almost identical to the halting problem, and easily reducible in either direction.

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

#27

Post by spiritbear14 »

tromp wrote: post #3

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

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.

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

#28

Post by ykonstant »

bionhoward wrote: post #17
darby_nine wrote: post #12

Earlier quoted context omitted.

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

Lovely video!

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

#29

Post by Sharlin »

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…

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

I think it's subtler than that. Circular programs in Turing's language are those that return to some exact earlier state and thus go into an infinite loop. So circular programs by definition do not halt. But circle-free programs can either halt or not halt!

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

#30

Post by FartyMcFarter »

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…

What do you mean by dressing it up as a theorem? It is a theorem because there's a proof for it.
Post reply on HN