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

41–50 of 116 posts

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

#41

Post by tsimionescu »

lou1306 wrote: post #14
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…

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

If it's not sound, than the result is meaningless. If it is not complete, then it only works on a subset of problems, which is equivalent to what I said.

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

#42

Post by jhanschoo »

shannifin wrote: post #37
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…

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

Not knowing the configuration of a TM at time t without running it (or similarly involved computation) doesn't mean that we cannot divide the space of TMs into classes.

One class has to each TM an associated mathematical function mapping inputs to nonnegative integers that tells you the exact integral time at which the TM transitions to the halting state. This is the class of decidable TMs.

The other class contains every TM not in the first class. For this class, any choice of such a function is provably wrong for some input. This is the class of undecicdable TMs.

Both classes are nonempty, and their existence is just about as well-defined as many other common mathematical objects. It is just not possible to provide a "nice" alternative characterization which TMs fall under which class.

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

#43

Post by kragen »

jononor wrote: post #39
arethuza wrote: post #19

Earlier quoted context omitted.

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.

bounded model checking is indeed a thing, but it's bounded

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

#44

Post by arethuza »

kragen wrote: post #43
jononor wrote: post #39

Earlier quoted context omitted.

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.

bounded model checking is indeed a thing, but it's bounded

A few months back I spent a couple of hours writing a binary TM simulator (yes I know you can download them - I wanted to write one) and then spent a couple of weeks running various TMs for days on end...

They exhibit quite bizarre amounts of complexity for what are really simple structures - indeed some TMs have apparently been observed employing Collatz conjecture type behaviour.

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

#45

Post by kragen »

arethuza wrote: post #44
kragen wrote: post #43

Earlier quoted context omitted.

bounded model checking is indeed a thing, but it's bounded

A few months back I spent a couple of hours writing a binary TM simulator (yes I know you can download them - I wanted to write one) and then spent a couple of weeks running various TMs for days on end... They exhibit quite bizarre amounts of complexity for what are really simple structures - indeed some TMs have apparently been observed employing Collatz conjecture type behaviour.

awesome!

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

#47

Post by jekude »

While it is an interesting quirk of history that we mainly think about computability hand-in-hand with the "halting" problem instead of Turing's symbol-printing, there are so many more interesting nuggets in the 1936 paper (like computational universality, the first ever programming bugs, etc). I do think the paper linked gets the nuances of attribution here correct.

I wrote up a little guide to Turing's paper a while back [0] if anyone is interested in reading it but needs help like I did.

[0] https://github.com/planetlambert/turing/blob/main/GUIDE.md

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

#49

Post by User23 »

FartyMcFarter wrote: post #7
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…

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…

It’s worth noting that the undecidability of the halting problem doesn’t prevent computing scientists from proving that a program halts or has some other nontrivial property.

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

#50

Post by Ygg2 »

User23 wrote: post #49
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…

It’s worth noting that the undecidability of the halting problem doesn’t prevent computing scientists from proving that a program halts or has some other nontrivial property.

Not a CS theorist, but it's not about you proving a program halts, it's about program proving that any program halts.

It's kinda like some statements in math given a set of axioms can't be proven or disproven.

Post reply on HN