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

61–70 of 116 posts

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

#61

Post by anon291 »

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…

Formal verification (i.e., automated theorem proving) relies on only admitting 'total' programs, which usually requires that any potential sources of 'bottom' (i.e., non-termination) come equipped with a proof that that never happens (usually based on well ordering of some structural decomposition in the recursion).

Thus, most theorem provers are not turing complete and explicitly ban any turing complete structures.

So, the various things they show and prove cannot be said to encompass all programs.

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

#62

Post by anon291 »

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

Whether any single given program? No, it's not decidable. For many programs, sure.

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

#63

Post by lou1306 »

tsimionescu wrote: post #41
lou1306 wrote: post #14

Earlier quoted context omitted.

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

Agree that soundness is desirable, but "it only works on a subset of instances" and "you are restricted to a non-Turing complete subset" are not equivalent in the slightest.

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

#66

Post by anon291 »

PaulHoule wrote: post #20

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…

I think it's one of the more unfortunate thing in mathematics that the real numbers are as popular as they are. I'm with your roommate. I don't believe they exist. I don't think every set of rational numbers has a least upper bound

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

#67

Post by Tainnor »

Maxatar wrote: post #59
mafuy wrote: post #22

Earlier quoted context omitted.

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…

It is never undecidable to determine whether a single particular program halts or not. For any single program, one of these two functions will correctly output whether it halts or not. bool always_true(TuringMachine M) { return true; } bool always_false(TuringMachine M) { return false; } It won't work for every Turing Machine, but it will work for a specific one. This is why it's not very meaningful to talk about the…

I suspect what GP means is that for certain programs, (assuming a fixed set of axioms) there exists neither a proof of its termination nor of its non-termination (not just that we can't find it; it doesn't exist).

Of course, if the program did eventually terminate, then a termination proof would exist (just enumerate all the state transitions, there's only a finite number of them). So what it means is that some programs never halt, but it's impossible to prove this fact.

This ties in with Gödel's theorems, e.g. (if we use ZFC and assume ZFC is consistent) a program that enumerates all possible valid proofs from axioms in ZFC and halts whenever it finds a contradiction, would never halt, but we can't prove this (at least not in ZFC) because that would contradict Gödel's second incompleteness theorem.

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

#68

Post by Tainnor »

tsimionescu wrote: post #40
isaacfrond wrote: post #38

Earlier quoted context omitted.

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

> there's even a prigramming language that only accepts programs that do so, Idris.

If you declare every function total. Idris still allows partial functions, and you can even cheat the whole system with "assert_total". Of course, with some sort of linter, you could still make sure that everything is actually total (although technically, in Idris "total" doesn't necessarily mean "halts" - programs which generate infinite input are also total in Idris).

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

#69

Post by SkiFire13 »

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

This comment really didn't age well https://discuss.bbchallenge.org/t/july-2nd-2024-we-have-prov...

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

#70

Post by auggierose »

anon291 wrote: post #66
PaulHoule wrote: post #20

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…

I think it's one of the more unfortunate thing in mathematics that the real numbers are as popular as they are. I'm with your roommate. I don't believe they exist. I don't think every set of rational numbers has a least upper bound

I don't believe that either. But every set of rational numbers bounded from above has a least upper bound in the reals.
Post reply on HN