This is a question that arose when studying Rice's theorem. As you all might know, Rice's theorem (informally and simply) states:

"There is no Turing machine (i.e. program) that can always (or generally) decide whether the language of another given Turing machine (i.e. program) satisfies a particular nontrivial property".

Some real examples of these nontrivial properties are:

  • Does a given program eventually halt for all possible inputs? (Turing's halting problem)
  • Are all accesses to an array in a given program inside the array's bounds? (buffer-overflow/overrun)
  • Is a given C program free of "use-after-free" bugs? (using a pointer after releasing it)

But there are also some other nontrivial properties for programs that can be decided using other programs (for example, compilers):

  • Are all the function invocations in a program previously defined? (Detecting undefined function invocations)
  • Are all the variables in a program initialized?
  • Do all assignment operations in a program, satisfy type-safety? (Detecting incompatible types assignments)

So it seems that not all nontrivial properties are the subject of Rice's undecidability theorem. An explanation in the Wikipedia article states:

"It is important to note that Rice's theorem does not say anything about those properties of machines or programs that are not also properties of functions and languages."

Unfortunately, this explanation didn't exactly help me understand the distinguishing aspect of properties that are subject of Rice's theorem from those properties that aren't.

Further down the Wikipedia article, it restates the matter like this:

"There exists no automatic method that decides with generality non-trivial questions on the behavior of computer programs."

My speculation from the term "program behavior", and additionally by observing the example properties, is that any nontrivial property that is related to the program's runtime data, is the subject of Rice's theorem (e.g. array indexing, pointer lifetime, halting, ...). In contrast, properties that are unrelated to the program's runtime data are not subject to Rice's theorem (e.g. type-safety, function definitions, variable initialization, ...). Note that I'm assuming "variable initialization" to be static data, not dynamic runtime data.

How correct or accurate is my speculation? If I'm mistaken then, is there an intuitive and concise explanation on the distinguishing aspects of properties that are subject to Rice's theorem from those that are not?

By "intuitive and concise" I mean an explanation suitable for a one session presentation of Rice's theorem to an audience of higher-undergrads and grad students of CS.


closed as off-topic by Hsien-Chih Chang 張顯之, Emil Jeřábek, Kristoffer Arnsfelt Hansen, Sasho Nikolov, Kaveh May 3 '15 at 6:15

This question appears to be off-topic. The users who voted to close gave this specific reason:

  • "Your question does not appear to be a research-level question in theoretical computer science. For more information about the scope, please see help center. Your question might be suitable for Computer Science which has a broader scope." – Hsien-Chih Chang 張顯之, Emil Jeřábek, Kristoffer Arnsfelt Hansen, Sasho Nikolov, Kaveh
If this question can be reworded to fit the rules in the help center, please edit the question.

  • $\begingroup$ @DownVoter It would be more constructive to provide a reason for a down-vote ... $\endgroup$ – Seyed Mohammad May 2 '15 at 19:12
  • $\begingroup$ Based on the tip @Shaull gave, I referred to cstheory.stackexchange.com/help/on-topic and I realize that my question doesn't exactly fit the intended topics of this Q/A site. I acknowledge this isn't a research question, but it's not a typical undergrad discussion either, thus my mistake! $\endgroup$ – Seyed Mohammad May 3 '15 at 2:05
  • $\begingroup$ @Moderators: I would migrate the question to cs.stackexchange If I could, but I can't. So how about performing a migrate instead of a hold? $\endgroup$ – Seyed Mohammad May 3 '15 at 6:22

This question is probably more suitable in cs.se, but until it gets migrated, here is an answer.

Rice's theorem regards non-trivial semantic properties.

Formally, a semantic property is a set of Turing machines $P$ such that for every two TMs $M_1,M_2$, if $L(M_1)=L(M_2)$, then either $M_1,M_2\in P$, or $M_1,M_2\notin P$. That is, membership in $P$ is determined solely by the language of the machine, and not by its "inner working".

Rice's theorem states that for every such property $P$ that is nontrivial (so it is not empty, nor contains every machine), it holds that deciding membership in $P$ is undecidable.

EDIT per the OP's request:

An intuitive way to look at a semantic property is that it only concerns what a program does, rather than how it does it. That is - memory management, pointers, data, types, etc - are all syntactic, in a way, and thus are not semantic properties. This is because for every program you can build a different program that works entirely differently, but achieves the same result.

Semantic properties only look at the "output" of the program (in cases where this is well-defined).

Thus, your intuition is incorrect. None of the internal workings of a program are subject to Rice's theorem, exactly because if you change entirely the inner workings (while maintaining the output), then either both programs should have the property, or both should not have them.

  • $\begingroup$ You didn't comment on the correctness of my speculation. Also, your answer doesn't meet my requested criteria! As requested in the question, I'm seeking a more "intuitive" explanation rather than such formal and hard to comprehend explanations. Thanks anyway though. $\endgroup$ – Seyed Mohammad May 2 '15 at 19:11
  • 1
    $\begingroup$ Edited. I hope it will be clearer now. By the way, I'm pretty sure the down vote is because this question is not research-level. It is a perfectly valid question for cs.se, though, and will probably be migrated there. $\endgroup$ – Shaull May 2 '15 at 19:54
  • $\begingroup$ Thanks for the edit. This is helpful. One last thing is can you also provide a "supporting reference" for this explanation? I mean something worth to be cited which supports this explanation and provides complementary discussions. $\endgroup$ – Seyed Mohammad May 3 '15 at 3:36
  • 1
    $\begingroup$ I don't know of any reference to this. I think the reason is that Rice's theorem shows such a fundamental result for TMs, that there is no motivation to examine it under the light of RAM machines, or programming languages, since these are "harder" cases. $\endgroup$ – Shaull May 3 '15 at 5:56

Not the answer you're looking for? Browse other questions tagged or ask your own question.