4 ms·

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 nontri

by User23 2y ago

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.

ryangs 2y ago
Right - it is saying that there is no algorithm to do this in general. Any specific instance may have a solution.
- User23 2y ago
  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.
  - afiori 2y ago
    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.
Ygg2 2y ago
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.
anon291 2y ago
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.
- Rhapso 2y ago
  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.
  - anon291 2y ago
    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.
    - Rhapso 2y ago
      it was unclear the entire runtime. Just need to keep evaluating.
- User23 2y ago
  > 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 for a computing scientist to read in a human life time, but that's another issue entirely. As a matter of practicality though, the working computing scientist is far more likely to first decide on the properties he wants his program to have and then derive a program that has them. This is yet another case of construction being considerably easier than verification. 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. 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.
thargor90 2y ago
You are right in that there is a class of algorithms for which it is possible to do that. It is just not possible to decide if any algorithm is in that specific class of algorithms or not. There is an even smaller class of algorithms that can be constructed bottom up from halting sub algorithms. But these are not as powerful.

by User23 2y ago

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.

ryangs 2y ago

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

User23 2y ago
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.
- afiori 2y ago
  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.

Ygg2 2y ago

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.

anon291 2y ago

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.

Rhapso 2y ago
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.
- anon291 2y ago
  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.
  - Rhapso 2y ago
    it was unclear the entire runtime. Just need to keep evaluating.
User23 2y ago
> 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 for a computing scientist to read in a human life time, but that's another issue entirely. As a matter of practicality though, the working computing scientist is far more likely to first decide on the properties he wants his program to have and then derive a program that has them. This is yet another case of construction being considerably easier than verification. 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. 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.

thargor90 2y ago

You are right in that there is a class of algorithms for which it is possible to do that. It is just not possible to decide if any algorithm is in that specific class of algorithms or not. There is an even smaller class of algorithms that can be constructed bottom up from halting sub algorithms. But these are not as powerful.