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

51–60 of 116 posts

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

#51

Post by chuckadams »

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…

Penrose's entire thesis seems to boil down that AGI is impossible because brains use Quantum Oogly-Boogly and that since Quantum Oogly-Boogly isn't computable, no computer can do it. The Emperor's New Mind is a tour de force of a book, but its central premise feels thoroughly unconvincing, or at least poorly communicated.

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

#52

Post by chuckadams »

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 actually like the symbol phrasing, it's more general than halting. You can't prove that any arbitrary program that can be in state X will ever actually reach state X. Besides, I feel like https://xkcd.com/1266/ is relevant :)

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

#53

Post by pjungwir »

Oh this is very helpful!

When I read Turing's paper some years ago, this really confused me. The best sense I could make was that "circle-free" means "halts". But in popular explanations, writers often equate "halts" with "gives a result" and "doesn't halt" with "has a bug", i.e. an infinite loop. And Turing seems to connote just the opposite. The point is to print a real number, so if the program stops printing digits, something went wrong. (I guess many numbers would end in 0s forever.) From today's paper:

> a program is circular, when it produces only finitely many digits of the output digit sequence, and circle-free, when it has succeeded in giving us an infinite digit sequence for the output real number.

But I could never really believe my interpretation. It was just the best I could come up with, as an amateur reading the paper alone for fun. Later I read Petzold's book, and I'm not sure that really solved the trouble for me either.

I've only read a few pages so far, but I'm gathering it's not as simple as I wanted: "circle-free" is not merely equivalent to "halts" after all. I'm looking forward to seeing their more nuanced take.

EDIT: Btw, this reminds me of the best riddle I've ever invented myself. Q: What do you call a fully autonomous self-driving car that can operate with as much understanding as a person? A: N Gheavat Znpuvar. (I didn't say it was a good riddle.)

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

#54

Post by Tainnor »

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

It's maybe nitpicky, but by definition "decidable" applies to a language, i.e. a set of programs, not a single program. Of course, there is a trivial TM (either the one that always accepts or the one that always rejects) that, for any given single program, gives the correct answer for exactly that program, but that is rather uninteresting. So this framing doesn't make a lot of sense.

What is actually decidable is the language consisting of pairs of a TM (+ input) and a valid proof of its termination, and that's why we can prove (some) programs to be terminating (or any other more interesting property).

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

#55

Post by dcow »

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

Penrose's entire thesis seems to boil down that AGI is impossible because brains use Quantum Oogly-Boogly and that since Quantum Oogly-Boogly isn't computable, no computer can do it. The Emperor's New Mind is a tour de force of a book, but its central premise feels thoroughly unconvincing, or at least poorly communicated.

The universe is a quantum computer that computes itself, so it’s certainly possible.

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

#56

Post by ryangs »

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.

Right - it is saying that there is no algorithm to do this in general. Any specific instance may have a solution.

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

#57

Post by byteknight »

pjungwir wrote: post #53

Oh this is very helpful! When I read Turing's paper some years ago, this really confused me. The best sense I could make was that "circle-free" means "halts". But in popular explanations, writers often equate "halts" with "gives a result" and "doesn't halt" with "has a bug", i.e. an infinite loop. And Turing seems to connote just the opposite. The point is to print a real number, so if the program stops printing digi…

Now we can add me to the list of confused.

> ... when it has succeeded in giving us an infinite digit sequence for the output real number.

How can it actually ever succeed then? Infinity never ends.

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

#58

Post by anon291 »

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.

In general, it absolutely does. I'm not sure what you're trying to say.

(1) Yes, there are classes of programs for which you can say whether it halts

(2) Yes, there are programs who do not fall into those classes who can be shown to halt

But the point remains... there's no 'general' way to show that any program halts.

Part of the point of good PL design is to produce a language that is amenable to analysis, including halting analysis. Some languages do this better than others. Others are okay so long as you make particular assumptions. The halting problem tells us that the languages that are perfectly analyzable are categorically less powerful than the ones that are not. However, this may be 'enough' for us.

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

#59

Post by Maxatar »

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…

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 decidability of particular Turing Machines and also why the halting problem is not, and never was about specific Turing Machines.

As to your point about being decidable within ZFC or PA, that is true but it's also not really significant. Neither ZFC or PA are a kind of master authority when it comes to decidability and in fact the vast majority of mathematics is fairly agnostic with respect to the use of ZFC.

The choice of a particular set theory tends to only come up in very explicit circumstances, and even in those circumstances you'll find mathematicians using theories that are more powerful than ZFC such as by making use of large cardinal axioms.

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

#60

Post by User23 »

ryangs wrote: post #56
User23 wrote: post #49

Earlier quoted context omitted.

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.

Right - it is saying that there is no algorithm to do this in general. Any specific instance may have a solution.

It's a little more impactful than that. Have a look at Z3, Boogie, Dafny, and similar technologies to see practical application of what I mean. It boils down to there being "non-general" algorithms that still work for virtually every input you're ever going to give them. A hypothetical algorithm that decides the halting problem for 99.9999999% of programs would not violate the impossibility proof.

The limit case is maybe interesting. What about the algorithm that decides the halting problem for every program except for one? Does the impossibility proof prohibit such an algorithm? Does it make a difference if the identity of the unique program is known or unknown?

And then of course there is classic pen and paper hand derivation like the old guard (Knuth and his peers) did. The claim that that is following an algorithm is yet to be proved or disproved.

Post reply on HN