11 ms·

Rice's Theorem isn't as strong as you say it is. What it says is that there exist programs that it's impossible to prove whether or not they have specific non-t

Rice's Theorem isn't as strong as you say it is. What it says is that there exist programs that it's impossible to prove whether or not they have specific non-trivial properties. But there still exist many programs where we can prove their correctness / incorrectness. What's more, I'd argue that if you're writing code whose behaviour is literally undecidable, you're doing something wrong, unless you're doing it for research purposes or something like that.

mkleczek 4y ago
> Rice's Theorem isn't as strong as you say it is It is very strong: its corollary is there is no general algorithm to build Turing Machines with arbitrary non-trivial properties (if there was such an algorithm we could use it to build a TM that solves the halting problem) So for any non-trivial property the only way to build a TM with this property is to use some ad-hoc method (as there is no general algorithm) - but how do we know the TM we've just built really holds the property we wanted it to? There is no way to verify it due to Rice's theorem.
- feanaro 4y ago
  This still doesn't exclude the existence of a general method for a well-behaved subset of Turing machines. It is the model of Turing machines that is too powerful.
  - mkleczek 4y ago
    There are two problems with this: 1. Even for as weak computational model as FSM the problem of verifying its correctness is intractable (NP-hard). And modularisation does not help. 2. We don't know any weaker computational model that is strong enough to be viable for the problems we want to solve and still weaker than TM. It is well known that it is surprisingly easy for a language to be (accidentally) Turing complete.
    - ncmncm 4y ago
      It is not necessary to verify that random presented machines have some property. It suffices that we can reliably construct machines that perform a desired function and have the desired property.
      - mkleczek 4y ago
        > It suffices that we can reliably construct machines that perform a desired function and have the desired property. See above - there is no reliable procedure (algorithm) that would allow you to do that.
    - feanaro 4y ago
      Yet languages with totality checkers and coinduction like Idris exist. These allow you to make useful but provably terminating programs. Humans are able to construct these termination proofs, though presumably not for all programs. In practice, this means that the reductive take of Turing completeness, the halting problem and Rice's theorem is misleading in some way. Yes, there is no general algorithm for constructing termination proofs for any arbitrary Turing machine. But there are clearly classes of problems for which a biological computer (a human) is able to construct termination proofs and proofs regarding other semantic properties.
      - deleted 4y ago
        [deleted]
- librexpr 4y ago
  Quoting from Wikipedia about Rice's theorem: > for any non-trivial property of partial functions, no general and effective method can decide whether an algorithm computes a partial function with that property This basically translates to "for each non-trivial property P, there exists a program x for which it is undecidable if x has the property P", or "∀P ∃x such that it's undecidable if x has property P". Notice that in this statement, programs are quantified using an "exists", not a "forall". Something similar holds for what you said here: > its corollary is there is no general algorithm to build Turing Machines with arbitrary non-trivial properties Translated to logic, this becomes "for every program y which takes as input a property and outputs a Turing Machine, there exists a property P such that the y(P) does not have property P", or "∀y ∃P y(P) does not have property P". Because this statement uses "exists" on the property, it does not rule out the existence of a y which works for most properties P that we'd care about. It only rules out one that works for all properties. As a simple example where it's possible to prove a non-trivial property, take the property "x is the identity function". This is a non-trivial property, because it is not true about all programs, nor is it false about all programs. And it is trivial to prove that the function "(n) => n" satisfies this property. Now, I additionally think that most practical programs can have their correctness / incorrectness proven. My reason for this belief is that generally, I expect coders to understand why the code they're writing should work. If nobody understands why the code works, I'd generally consider that a bug, or at least a major code smell. But if the programmer actually understands why the code works, and hasn't made any mistakes, then in principle their understanding could be converted into a proof, because proofs are more or less just correct reasoning, but written out formally. Of course, it would still be very hard, but it's not "provably impossible". Edit: minor text change
  - mkleczek 4y ago
    > Because this statement uses "exists" on the property, it does not rule out the existence of a y which works for most properties P that we'd care about. It only rules out one that works for all properties. Translated: there exists a computational model weaker than TM but strong enough to implement programs we care about. Unfortunately, we don't know such computational model and we know empirically surprisingly many problems require a TM (ie. surprisingly many languages are accidentally Turing complete)

mkleczek 4y ago

> Rice's Theorem isn't as strong as you say it is It is very strong: its corollary is there is no general algorithm to build Turing Machines with arbitrary non-trivial properties (if there was such an algorithm we could use it to build a TM that solves the halting problem) So for any non-trivial property the only way to build a TM with this property is to use some ad-hoc method (as there is no general algorithm) - but how do we know the TM we've just built really holds the property we wanted it to? There is no way to verify it due to Rice's theorem.

feanaro 4y ago
This still doesn't exclude the existence of a general method for a well-behaved subset of Turing machines. It is the model of Turing machines that is too powerful.
- mkleczek 4y ago
  There are two problems with this: 1. Even for as weak computational model as FSM the problem of verifying its correctness is intractable (NP-hard). And modularisation does not help. 2. We don't know any weaker computational model that is strong enough to be viable for the problems we want to solve and still weaker than TM. It is well known that it is surprisingly easy for a language to be (accidentally) Turing complete.
  - ncmncm 4y ago
    It is not necessary to verify that random presented machines have some property. It suffices that we can reliably construct machines that perform a desired function and have the desired property.
    - mkleczek 4y ago
      > It suffices that we can reliably construct machines that perform a desired function and have the desired property. See above - there is no reliable procedure (algorithm) that would allow you to do that.
  - feanaro 4y ago
    Yet languages with totality checkers and coinduction like Idris exist. These allow you to make useful but provably terminating programs. Humans are able to construct these termination proofs, though presumably not for all programs. In practice, this means that the reductive take of Turing completeness, the halting problem and Rice's theorem is misleading in some way. Yes, there is no general algorithm for constructing termination proofs for any arbitrary Turing machine. But there are clearly classes of problems for which a biological computer (a human) is able to construct termination proofs and proofs regarding other semantic properties.
    - deleted 4y ago
      [deleted]
librexpr 4y ago
Quoting from Wikipedia about Rice's theorem: > for any non-trivial property of partial functions, no general and effective method can decide whether an algorithm computes a partial function with that property This basically translates to "for each non-trivial property P, there exists a program x for which it is undecidable if x has the property P", or "∀P ∃x such that it's undecidable if x has property P". Notice that in this statement, programs are quantified using an "exists", not a "forall". Something similar holds for what you said here: > its corollary is there is no general algorithm to build Turing Machines with arbitrary non-trivial properties Translated to logic, this becomes "for every program y which takes as input a property and outputs a Turing Machine, there exists a property P such that the y(P) does not have property P", or "∀y ∃P y(P) does not have property P". Because this statement uses "exists" on the property, it does not rule out the existence of a y which works for most properties P that we'd care about. It only rules out one that works for all properties. As a simple example where it's possible to prove a non-trivial property, take the property "x is the identity function". This is a non-trivial property, because it is not true about all programs, nor is it false about all programs. And it is trivial to prove that the function "(n) => n" satisfies this property. Now, I additionally think that most practical programs can have their correctness / incorrectness proven. My reason for this belief is that generally, I expect coders to understand why the code they're writing should work. If nobody understands why the code works, I'd generally consider that a bug, or at least a major code smell. But if the programmer actually understands why the code works, and hasn't made any mistakes, then in principle their understanding could be converted into a proof, because proofs are more or less just correct reasoning, but written out formally. Of course, it would still be very hard, but it's not "provably impossible". Edit: minor text change
- mkleczek 4y ago
  > Because this statement uses "exists" on the property, it does not rule out the existence of a y which works for most properties P that we'd care about. It only rules out one that works for all properties. Translated: there exists a computational model weaker than TM but strong enough to implement programs we care about. Unfortunately, we don't know such computational model and we know empirically surprisingly many problems require a TM (ie. surprisingly many languages are accidentally Turing complete)