5 ms·
That's backwards. One proof of rice's theorem relies on the fact that, if you could decide any interesting property of programs in general, then you could solv
by moonchild 3y ago
That's backwards. One proof of rice's theorem relies on the fact that, if you could decide any interesting property of programs in general, then you could solve the halting problem; it doesn't follow that, if you could solve the halting problem, then you could decide any interesting property.
It happens to be true that, if you could solve the halting problem, then you could decide any interesting property of programs; but this is simply because the antecedent is false.
- Ygg2 3y ago> That's backwards. See Wikipedia entry for Rice theorem subsection proof by reduction from the halting problem. 1. Have intersting property solver (e.g. is input squared) 2. Convert solver to halting problem solver 3. Solver is undecidable So they are in some equatable/convertible.
- moonchild 3y agoBeing able to turn an interesting property solver into a halting problem solver is not the same thing as being able to turn a halting property solver into an interesting problem solver.
- Ygg2 3y agoMy claim or at least intent was you can solve interesting property solver like you can solve a halting problem. I.e. not in a satisfying way (no false negatives or false positives with unlimited iterations). You can solve it to some extent (e.g. does program terminate in X steps).
- UncleMeat 3y agoBut this is vacuous and unrelated to the halting problem or Rice's Thm. A program that emits "Yes" on every input will decide some property of programs with zero false negatives.
- Ygg2 3y agoHence, the interesting property part. Program that returns "true" on everything is trivial.
- UncleMeat 3y ago"Interesting property", as defined by Rice's Thm, is "any semantic property that is not either always true or always false for all program executions." It does not mean "interesting" as in "interesting to humans." And I'm talking about the decider, not the program being fed as input.
- Ygg2 3y agoI'm not a computer scientist, but I am aware Interesting doesn't mean interesting to humans. > And I'm talking about the decider EDIT: If by decider you mean program tested for having property P, that's a particular case and not applicable in general, ergo non-important (a program that's a NOP can be shown to leak no memory as well). So the property P you are testing always returns true? Then it's not interesting per your definition. Leaking memory however is interesting.
- UncleMeat 3y agoNo that's not what I mean by decider. The decider is the program that takes the other program as input and tells you whether that input program has the semantic property you want. The only noninteresting semantic properties of programs that exist are "this is a program" and "this is not a program."
- Ygg2 3y agoYes. And you said > A program that emits "Yes" on every input will decide some property of programs with zero false negatives. Followed by > any semantic property that is not either always true or always false for all program executions So what you said is your decider always outputs true. That's not an interesting property, because it's true for all inputs. Btw what is the point of your argument? It still doesn't refute my initial statement. If you want to determine an interesting property of program like leaks, or automatic lifetime calculation or whether output is square of input, you run into Rice Theorem, which makes the problem undecidable. In other words it's impossible to get correct yes and no algorithmically.