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

81–90 of 116 posts

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

#81

Post by legacynl »

byteknight wrote: post #57
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.

I don't think the examples are meant as actual real world things, but rather abstractions to help reason about the problem.

The most important thing about the halting problem, is that Turing gave an example of a computational problem that is unsolvable, thereby proofing that from all possible computational problems, some of them are be unsolvable.

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

#82

Post by Tainnor »

User23 wrote: post #77
anon291 wrote: post #58

Earlier quoted context omitted.

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…

> In general, it absolutely does. I'm not sure what you're trying to say. I can see that you don't so I'll try to be clearer. For any given program one might choose there is no reason in principle why a competent computing scientist can't perform a semantic analysis for every statement and then deduce from that whether it is totally or partially correct. Obviously most programs in the set of all programs are too long…

If you fix a particular axiom system for deriving your termination proofs (e.g. because you write them all down in Coq), then for Gödelian reasons, there are programs that don't terminate but for which a nontermination proof doesn't exist (and thus can never be found). If Coq is consistent, then the program that enumerates all possible Coq proofs and stops as soon as it finds a contradiction, is one such program.

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

#83

Post by mafuy »

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

Was it this one? https://scottaaronson.blog/?p=2725

Probably! This paper is a year or two newer but used the exact same principle. It also has a much better constant than I recall. Perhaps I was reading a precursor article. I really enjoy this approach, it is a lovely idea.

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

#84

Post by afiori »

User23 wrote: post #60
ryangs wrote: post #56

Earlier quoted context omitted.

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

With a little massaging of input and output you can convert any program P into the program P_n defined as "repeat P n times".

For any n P terminate if and only if P_n terminates, so no general procedure can decide the halting problem for all programs except 1.

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

#85

Post by svat »

User23 wrote: post #77
anon291 wrote: post #58

Earlier quoted context omitted.

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…

> In general, it absolutely does. I'm not sure what you're trying to say. I can see that you don't so I'll try to be clearer. For any given program one might choose there is no reason in principle why a competent computing scientist can't perform a semantic analysis for every statement and then deduce from that whether it is totally or partially correct. Obviously most programs in the set of all programs are too long…

I'm sure you know this, but even very simple/short programs can have complex behaviours that put them out of reach of computer scientists with present-day knowledge. For example, short programs can encode things like the Goldbach conjecture, the Collatz conjecture, or the Riemann Hypothesis. For example, does this program (written in Python, but translate to your computational system) halt?

    def isprime(n): return n > 1 and all(n % d for d in range(2, n))
    def goldbach(n): return any(isprime(p) and isprime(n - p) for p in range(2, n))
    n = 4
    while goldbach(n): n += 2
(See also the recent https://www.quantamagazine.org/amateur-mathematicians-find-f... which describes how hard it was to prove things even about puny 5-state Turing machines, and that already with just 6 states there is one "antihydra" that encodes Collatz-like behaviour and will probably be hard to prove anything about.)

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

#86

Post by anon291 »

auggierose wrote: post #70
anon291 wrote: post #66

Earlier quoted context omitted.

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.

That's my point. I don't believe they do. I don't believe the reals are well defined since no one can name them. In general, I lean towards mathematical constructivism: https://en.wikipedia.org/wiki/Constructivism_(philosophy_of_...

I agree that computable real numbers exist, even if they're intractable to compute.

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

#87

Post by anon291 »

Rhapso wrote: post #73
anon291 wrote: post #58

Earlier quoted context omitted.

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…

There is 1 general way to show any given program halts. Run it on each equivalency class of input and wait! This just might take forever.

That is not a determinable way though, since when a program enters a 'loop'ing state, it's unclear if it's going to halt or not.

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

#88

Post by nextaccountic »

anon291 wrote: post #58
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.

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…

But do we need general ways to show that any program halts? We don't write general programs

In particular, our programs have a limited size and use a limited amount of memory (or else the OS will make sure they will halt..). And for this specific class of programs, the halting problem is actually decidable!

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

#89

Post by anon291 »

User23 wrote: post #77
anon291 wrote: post #58

Earlier quoted context omitted.

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…

> In general, it absolutely does. I'm not sure what you're trying to say. I can see that you don't so I'll try to be clearer. For any given program one might choose there is no reason in principle why a competent computing scientist can't perform a semantic analysis for every statement and then deduce from that whether it is totally or partially correct. Obviously most programs in the set of all programs are too long…

> I can see that you don't so I'll try to be clearer. For any given program one might choose there is no reason in principle why a competent computing scientist can't perform a semantic analysis for every statement and then deduce from that whether it is totally or partially correct.

'Correct'? In what sense? 'Correctness' and halting have little to do with each other. For example:

    def f(p):
       p()
       return 2
is 'correct' if the definition of f is to evaluate to two. But it's not clear it's ever going to halt (depends on haltingness of p).

But that being said, actually no, there are many reasons in principle why a competent computer scientist would not be able to perform a semantic analysis for every statement and deduce from that whether the program will halt.

> Obviously most programs in the set of all programs are too long for a computing scientist to read in a human life time, but that's another issue entirely.

Irrelevant because even an immortal computer scientist would be unable to determine if the program halts.

> This points to (but doesn't prove) the possibility that the human computing scientist isn't using a decision procedure to analyze (or construct) the program.

The difference between a computer and a person (and I'm going to ignore all the various philosophies of consciousness) is that a human will 'arbitrarily' determine under what system he/she wants to operate, and thus can change axioms on the fly. of course, one could write a computer system that does this as well. It's really not obvious what you're saying here

> About here is where I expect to see some misinterpretation of Church-Turing as somehow proving that everything, including computing scientists, is a Turing machine brought up. Oddly, rarely is the far more interesting Curry-Howard correspondence mentioned.

Computer scientists may or may not be turing machines, but any deterministic procedure they follow can be encoded as a turing machine so your distinction is irrelevant.

I'm not sure what Curry-Howard really has to do with this, but in general, for a theorem checker, you should make sure your proofs are total.

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

#90

Post by kbelder »

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 found his Physics Stack Exchange answers to be immensely valuable. Although, I did have to read everything he wrote with a little bit of a critical eye, due to some of the rants he went on.

I'm glad to see he bought into the abiotic generation of oil; it's my favorite fringe theory I just can't shake.

Post reply on HN