9 ms·

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 seman

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_reduction_from_the_halting_problem 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 semantic property is one about the program's behavior (for instance, "does the program terminate for all inputs?"), unlike a syntactic property (for instance, "does the program contain an if-then-else statement?"). A non-trivial property is one which is neither true for every program, nor false for every program.

indolering 2y ago
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 solve whether a problem halts 100% of the time. So Rice's Theorem is theoretically meaningless.
- tsimionescu 2y ago
  > 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 seem to show an exponential speed advantage for a certain very limited subset of problems, mostly related to quantum transforms.
  - lou1306 2y ago
    > 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.
    - tsimionescu 2y ago
      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.
      - lou1306 2y ago
        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.
        deleted 2y ago
        [deleted]
        lostmsu 2y ago
        Not sure what are you trying to say. Surely the "subset of instances" is non-Turing complete.
  - isaacfrond 2y ago
    huh, is that true? Is that class of computable function with a halting guarantee strictly smaller than the class of computable function without one? <citation missing>
    - tsimionescu 2y ago
      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 loops with a known bound (e.g. while (x > 0) is not ok, but for(i = 0; i < 100; i++) is ok, as long as i is not modified in the body), don't use in-line ASM, don't use recursion, don't use stdlib functions (definitely no string functions). These rules can be verified syntactically (+- problems with UB), and the resulting program is guaranteed to halt. But there are problems for which you can't write such a program. As to the relative size of these sets, I think that's a meaningless question - they are both infinite sets.
- frabert 2y ago
  > We have lots of formally verified programs that show useful work can be done here Yes, if you start writing your program with the explicit intent of making such proofs possible, then it can be done. What Rice's theorem says is that you can't expect to be able to do so when given an arbitrary program, not that it's always impossible.
- darby_nine 2y ago
  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 class issue, and my understanding is that quantum computation can't compute anything that turing machines can't, they just are able to compute certain algorithms faster. Am i wrong? Among other things we can simulate quantum computers on turing machines, just without the complexity advantages. Like think about what you're saying: of course we can prove that "exit(0)" halts, it'd be absurd to say otherwise. So we're clearly referring to a harder problem—proving whether arbitrary programs halt with a single algorithm in finite time. If it helps, Roger Penrose misunderstood the halting problem and basically said "humans aren't practically constrained by godel's incompleteness theorems (equivalent to the halting problem I believe) so consciousness is quantum". This might yet be true but human computers are still bound by the same computational constraints computer's are. It's been a bit since my computer theory courses so apologies for any botched terminology or understanding.
  - bionhoward 2y ago
    Relevant video about MIP*=RE https://youtu.be/2H8629BCbkM https://youtu.be/2H8629BCbkM
    - ykonstant 2y ago
      Lovely video!
  - arethuza 2y ago
    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/blob/main/bb5_undecided_machines.csv https://github.com/bbchallenge/bbchallenge-undecided-index/b...
- FartyMcFarter 2y ago
  What do you mean by dressing it up as a theorem? It is a theorem because there's a proof for it.
  - Tainnor 2y ago
    For example, here's a formally verified proof in Lean: https://github.com/leanprover-community/mathlib4/blob/12473136ebd2e811c9c929c11522af5a32d603fb/Mathlib/Computability/Halting.lean#L219-L234 https://github.com/leanprover-community/mathlib4/blob/124731...
- anon291 2y ago
  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.
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.
- 2y ago

indolering 2y ago

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 solve whether a problem halts 100% of the time. So Rice's Theorem is theoretically meaningless.

tsimionescu 2y ago
> 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 seem to show an exponential speed advantage for a certain very limited subset of problems, mostly related to quantum transforms.
- lou1306 2y ago
  > 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.
  - tsimionescu 2y ago
    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.
    - lou1306 2y ago
      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.
      - deleted 2y ago
        [deleted]
      - lostmsu 2y ago
        Not sure what are you trying to say. Surely the "subset of instances" is non-Turing complete.
- isaacfrond 2y ago
  huh, is that true? Is that class of computable function with a halting guarantee strictly smaller than the class of computable function without one? <citation missing>
  - tsimionescu 2y ago
    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 loops with a known bound (e.g. while (x > 0) is not ok, but for(i = 0; i < 100; i++) is ok, as long as i is not modified in the body), don't use in-line ASM, don't use recursion, don't use stdlib functions (definitely no string functions). These rules can be verified syntactically (+- problems with UB), and the resulting program is guaranteed to halt. But there are problems for which you can't write such a program. As to the relative size of these sets, I think that's a meaningless question - they are both infinite sets.
frabert 2y ago
> We have lots of formally verified programs that show useful work can be done here Yes, if you start writing your program with the explicit intent of making such proofs possible, then it can be done. What Rice's theorem says is that you can't expect to be able to do so when given an arbitrary program, not that it's always impossible.
darby_nine 2y ago
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 class issue, and my understanding is that quantum computation can't compute anything that turing machines can't, they just are able to compute certain algorithms faster. Am i wrong? Among other things we can simulate quantum computers on turing machines, just without the complexity advantages. Like think about what you're saying: of course we can prove that "exit(0)" halts, it'd be absurd to say otherwise. So we're clearly referring to a harder problem—proving whether arbitrary programs halt with a single algorithm in finite time. If it helps, Roger Penrose misunderstood the halting problem and basically said "humans aren't practically constrained by godel's incompleteness theorems (equivalent to the halting problem I believe) so consciousness is quantum". This might yet be true but human computers are still bound by the same computational constraints computer's are. It's been a bit since my computer theory courses so apologies for any botched terminology or understanding.
- bionhoward 2y ago
  Relevant video about MIP*=RE https://youtu.be/2H8629BCbkM https://youtu.be/2H8629BCbkM
  - ykonstant 2y ago
    Lovely video!
- arethuza 2y ago
  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/blob/main/bb5_undecided_machines.csv https://github.com/bbchallenge/bbchallenge-undecided-index/b...
FartyMcFarter 2y ago
What do you mean by dressing it up as a theorem? It is a theorem because there's a proof for it.
- Tainnor 2y ago
  For example, here's a formally verified proof in Lean: https://github.com/leanprover-community/mathlib4/blob/12473136ebd2e811c9c929c11522af5a32d603fb/Mathlib/Computability/Halting.lean#L219-L234 https://github.com/leanprover-community/mathlib4/blob/124731...
anon291 2y ago
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.

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