Did Turing prove the undecidability of the halting problem? • Hacker News Board

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

#31

Post by lisper » Tue, Jul 02, 2024, 11:26 AM UTC

tromp wrote: post #24

lisper wrote: post #21

Earlier quoted context omitted.

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?

The key is the assumption that the machine is non-circular. So there must be a state in which it prints its last symbol (can we agree to drop the "of the first kind" qualification?). After that, it never prints another symbol, so you can just replace whatever it does after that with a halting state.

But I see the problem with this now that I've written it out. The future behavior of the machine also depends on the state of the tape so you can't "just replace" all the future behavior because you don't know which entry into the state that prints the last symbol will be the one that actually prints the last symbol. So that doesn't work.

Still, going meta, there are only two possibilities here: either the undecidability of the HP is equivalent to the undecidability of circularity (i.e. that either result follows from the other) or it isn't. If it isn't then that would be Big News, and if it is, then it's just a question of how easy or hard it is to prove this. If it's hard, then someone should get the credit for being the first, and since I've never heard anyone get the credit I conclude that it's probably easy notwithstanding that my intuition about how to do it turns out to be wrong.

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

#32

Post by lisper » Tue, Jul 02, 2024, 11:29 AM UTC

Sharlin wrote: post #29

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

> Circular programs in Turing's language are those that return to some exact earlier state

No, they aren't. They are programs that print a finite number of "symbols of the first kind" i.e. 0s and 1s. They can print an infinite number of other symbols.

You might want to check out this branch of the discussion:

https://news.ycombinator.com/item?id=40855382

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

#33

Post by tromp » Tue, Jul 02, 2024, 11:33 AM UTC

lisper wrote: post #31

tromp wrote: post #24

Earlier quoted context omitted.

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

The key is the assumption that the machine is non-circular. So there must be a state in which it prints its last symbol (can we agree to drop the "of the first kind" qualification?). After that, it never prints another symbol, so you can just replace whatever it does after that with a halting state. But I see the problem with this now that I've written it out. The future behavior of the machine also depends on the st…

Chaitin has pointed out an important difference between such questions [1] :

> In our approach to incompleteness, we shall ask whether or not a program produces an infinite amount of output rather than asking whether it produces any; this is equivalent to asking whether or not a diophantine equation has infinitely many solutions instead of asking whether or not it is solvable. If one asks whether or not a diophantine equation has a solution for N different values of a parameter, the N different answers to this question are not independent; in fact, they are only log2 N bits of information. But if one asks whether or not there are infinitely many solutions for N different values of a parameter, then there are indeed cases in which the N different answers to these questions are independent mathematical facts, so that knowing one answer is no help in knowing any of the others

[1] https://theswissbay.ch/pdf/Gentoomen%20Library/Information%2...

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

#34

Post by syrak » Tue, Jul 02, 2024, 11:50 AM UTC

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…

That point is discussed in the paper: circle-freeness is Pi^0_2 in the arithmetic hierarchy, so there isn't a reduction to halting (Sigma^0_1) in the usual sense of a mapping between inputs. And in fact, Turing's paper does do a construction like you describe to show that yet another problem ("symbol-printing") is undecidable, and that one is much more similar to halting than circle-freeness. Again, this subtlety is discussed in the paper.

I think you were a bit quick in dismissing the OP paper based only on its title.

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

#35

Post by lisper » Tue, Jul 02, 2024, 11:52 AM UTC

syrak wrote: post #34

lisper wrote: post #21

Earlier quoted context omitted.

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…

That point is discussed in the paper: circle-freeness is Pi^0_2 in the arithmetic hierarchy, so there isn't a reduction to halting (Sigma^0_1) in the usual sense of a mapping between inputs. And in fact, Turing's paper does do a construction like you describe to show that yet another problem ("symbol-printing") is undecidable, and that one is much more similar to halting than circle-freeness. Again, this subtlety is…

Yes, I think you might be right about that. FWIW, it's 4AM here and I am not firing on all cylinders. I live in the U.S. and politics is weighing heavily on my mind tonight.

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

#36

Post by Tainnor » Tue, Jul 02, 2024, 11:56 AM UTC

FartyMcFarter wrote: post #30

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…

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

For example, here's a formally verified proof in Lean: https://github.com/leanprover-community/mathlib4/blob/124731...

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

#37

Post by shannifin » Tue, Jul 02, 2024, 12:00 PM UTC

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…

> "Figuring out whether a single given program halts is decidable"

What does "decidable" mean in this context? Simply running the program may not be sufficient to know whether or not it halts. One could have a program that loops infinitely but never repeats the same state. So it will never halt, nor will its looping be obvious. So does it count as "decidable" if we cannot yet prove whether or not it's looping?

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

#38

Post by isaacfrond » Tue, Jul 02, 2024, 12:03 PM UTC

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…

huh, is that true? Is that class of computable function with a halting guarantee strictly smaller than the class of computable function without one?

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

#39

Post by jononor » Tue, Jul 02, 2024, 12:19 PM UTC

arethuza wrote: post #19

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…

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

That is a much lower complexity grade than I thought we would struggle with. Especially since we have decades of experience in solvers for rather large Boolean Satisfiability Problems, which seems like it could be adapted here.

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

#40

Post by tsimionescu » Tue, Jul 02, 2024, 12:24 PM UTC

isaacfrond wrote: post #38

tsimionescu wrote: post #10

Earlier quoted context omitted.

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

huh, is that true? Is that class of computable function with a halting guarantee strictly smaller than the class of computable function without one?

I'm not sure what you're asking about. It is well known that certain computations can be determinstically proven to halt - there's even a prigramming language that only accepts programs that do so, Idris.

Of course, not any computation can be written in such a way. But it's clearly possible to write certain programs in such a way that they must halt by construction. You can even do it in C: don't use goto, only use loops with a known bound (e.g. while (x > 0) is not ok, but for(i = 0; i As to the relative size of these sets, I think that's a meaningless question - they are both infinite sets.