Rice's theorem
In computability theory, 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 property is "non-trivial" if it is neither true for every partial computable function, nor false for every partial computable function. Rice's theorem can also be put in terms of functions: 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. Here, a property of partial functions is called "trivial" if it holds for all partial computable functions or for none, and an effective decision method is called "general" if it decides correctly for every algorithm. The theorem is named after Henry Gordon Rice, who proved it in his doctoral dissertation of 1951 at Syracuse University. Introduction. Let be a property of a formal language that is nontrivial, meaning (that is, "p" is neither uniformly true nor uniformly false for all recursively enumerable languages). Then it is undecidable to  determine for a given Turing machine "M", whether the language recognized by it – "L(M)" – has the property "p". In practice, this means that there is no machine that can always decide whether the language of a given Turing machine has a particular nontrivial property. Special cases include e.g. the undecidability of whether the language recognized by a Turing machine could be recognized by a nontrivial simpler machine, such as a finite automaton (meaning, it is undecidable whether the language of a Turing machine is regular). It is important to note that Rice's theorem does not concern the properties of  machines or programs; it concerns properties of functions and languages. For example, whether a machine runs for more than 100 steps on a particular input is a decidable property, even though it is non-trivial. Two different machines recognizing exactly the same language might require a different number of steps to recognize the same input string. Similarly, whether a machine has more than five states is a decidable property of the machine, as the number of states can simply be counted. For properties of this kind, which concerns a Turing machine but not the language recognized by it, Rice's  theorem does not apply. Using Rogers' characterization of acceptable programming systems, Rice's theorem may essentially be generalized from Turing machines to most computer programming languages: there exists no automatic method that decides with generality non-trivial questions on the behavior of computer programs. As an example, consider the following variant of the halting problem. Let "P" be the following property of partial functions F of one argument: "P"(F) means that F is defined for the argument '1'. It is obviously non-trivial, since there are partial functions that are defined at 1, and others that are undefined at 1 . The "1-halting problem" is the problem of deciding of any algorithm whether it defines a function with this property, i.e., whether the algorithm halts on input 1. By Rice's theorem, the 1-halting problem is undecidable. Similarly the question of whether a Turing machine "T" terminates on an initially empty tape (rather than with an initial word "w" given as second argument in addition to a description of "T", as in the full halting problem) is still undecidable. Formal statement. Let formula_1 denote the natural numbers, and let formula_2 denote the class of unary (partial) computable functions. Let  formula_3 be an admissible numbering of the computable functions. Denote by formula_4 the th (partial) computable function. We identify each "property" that a computable function may have with the subset of formula_2 consisting of the functions with that property. Thus, given a set formula_6, a computable function formula_7 has property formula_8 if and only if formula_9. For each property formula_6 there is an associated membership decision problem formula_11 of determining, given , whether formula_9. Rice's theorem states that the decision problem formula_11 is decidable (also called "recursive" or "computable") if and only if formula_14 or formula_15. Examples. According to Rice 's theorem, if there is at least one partial computable function in a particular class "C" of partial computable functions and another partial computable function not in "C" then the problem of deciding whether a particular program computes a function in "C" is undecidable. For example, Rice's theorem shows that each of the following sets of partial computable functions is undecidable (that is, the set is not recursive, or not computable): Proof by Kleene's recursion theorem. A corollary to Kleene's recursion theorem states that for every Gödel numbering formula_3 of the computable functions and every computable function  formula_17, there is an index formula_18 such that formula_19 returns formula_20. (In the following, we say that formula_21 "returns" formula_22 if either formula_23, or both formula_21 and formula_22 are undefined.) Intuitively, formula_7 is a quine, a function that returns its own source code (Gödel number), except that rather than returning it directly, formula_7 passes its Gödel number to formula_28 and returns the result. Assume for contradiction that formula_8 is a set of computable functions such that formula_30. Then there are computable functions formula_31 and formula_32. Suppose that the set of indices formula_33 such that formula_34 is decidable; then, there exists  a function formula_17 that returns formula_36 if formula_34, and formula_38 otherwise. By the corollary to the recursion theorem, there is an index formula_18 such that formula_19 returns formula_20. But then, if formula_9, then formula_7 is the same function as formula_44, and therefore formula_45; and if formula_45, then formula_7 is formula_48, and therefore formula_9. In both cases, we have a contradiction. Proof by reduction from the halting problem. Proof sketch. Suppose, for concreteness, that we have an algorithm for examining a program "p" and determining infallibly whether "p" is an implementation of the squaring function, which takes an integer "d" and  returns "d". The proof works just as well if we have an algorithm for deciding any other nontrivial property of program behavior (i.e. a semantic and non-trivial property), and is given in general below. The claim is that we can convert our algorithm for identifying squaring programs into one that identifies functions that halt. We will describe an algorithm that takes inputs "a" and "i" and determines whether program "a" halts when given input "i". The algorithm for deciding this is conceptually simple: it constructs (the description of) a new program "t" taking an argument "n", which (1) first  executes program "a" on input "i" (both "a" and "i" being hard-coded into the definition of "t"), and (2) then returns the square of "n". If "a"("i") runs forever, then "t" never gets to step (2), regardless of "n". Then clearly, "t" is a function for computing squares if and only if step (1) terminates. Since we've assumed that we can infallibly identify programs for computing squares, we can determine whether "t", which depends on "a" and "i", is such a program, and that for every "a" and "i"; thus we have obtained a program that decides whether  program "a" halts on input "i". Note that our halting-decision algorithm never executes "t", but only passes its description to the squaring-identification program, which by assumption always terminates; since the construction of the description of "t" can also be done in a way that always terminates, the halting-decision cannot fail to halt either. This method doesn't depend specifically on being able to recognize functions that compute squares; as long as "some" program can do what we're trying to recognize, we can add a call to "a" to obtain our "t". We could have had  a method for recognizing programs for computing square roots, or programs for computing the monthly payroll, or programs that halt when given the input "Abraxas"; in each case, we would be able to solve the halting problem similarly. Formal proof. For the formal proof, algorithms are presumed to define partial functions over strings and are themselves represented by strings. The partial function computed by the algorithm represented by a string "a" is denoted F. This proof proceeds by reductio ad absurdum: we assume that there is a non-trivial property that is decided by an algorithm, and then show that  it follows that we can decide the halting problem, which is not possible, and therefore a contradiction. Let us now assume that "P"("a") is an algorithm that decides some non-trivial property of F. Without loss of generality we may assume that "P"("no-halt") = "no", with "no-halt" being the representation of an algorithm that never halts. If this is not true, then this holds for the negation of the property. Since "P" decides a non-trivial property, it follows that there is a string "b" that represents an algorithm and "P"("b") = "yes". We can then define an  algorithm "H"("a", "i") as follows: We can now show that "H" decides the halting problem: Since the halting problem is known to be undecidable, this is a contradiction and the assumption that there is an algorithm "P"("a") that decides a non-trivial property for the function represented by "a" must be false. Rice's theorem and index sets. Rice's theorem can be succinctly stated in terms of index sets: Let formula_50 be a class of partial recursive functions with index set formula_51. Then formula_51 is recursive if and only if formula_53 or formula_54. Here formula_55 is the set of  natural numbers, including zero. An analogue of Rice's theorem for recursive sets. One can regard Rice's theorem as asserting the impossibility of effectively deciding for any "recursively enumerable" set whether it has a certain nontrivial property. In this section, we give an analogue of Rice's theorem for recursive sets"," instead of recursively enumerable sets. Roughly speaking, the analogue says that if one can effectively determine for every "recursive" set whether it has a certain property, then only finitely many integers determine whether a recursive set has the property. This result is analogous to the original theorem of  Rice, because both results assert that a property is "decidable" only if one can determine whether a set has that property by examining "for at most finitely many formula_56" (for no formula_56, for the original theorem), if formula_56 belongs to the set. Let formula_59 be a class (called a "simple game" and thought of as a property) of recursive sets. If formula_60 is a recursive set, then for some formula_18, computable function formula_7 is the characteristic function of formula_60. We call formula_18 a "characteristic index" for formula_60. (There are infinitely many such formula_18.) Let's say the class formula_59 is  computable if there is an algorithm (computable function) that decides for any nonnegative integer formula_18 (not necessarily a characteristic index), A set formula_73 "extends" a string formula_74 of 0's and 1's if for every formula_75 (the length of formula_74), the formula_77th element of formula_74 is 1 if formula_79; and is 0 otherwise. For example, formula_80 extends the string formula_81. A string formula_74 is "winning determining" if every recursive set extending formula_74 belongs to formula_59. A string formula_74 is "losing determining" if no recursive set extending formula_74 belongs to formula_59. We can now state the following "analogue of Rice 's theorem": A class formula_59 of recursive sets is computable if and only if there are a recursively enumerable set formula_89 of losing determining strings and a recursively enumerable set formula_90 of winning determining strings such that every recursive set extends a string in formula_91. This result has been applied to foundational problems in computational social choice (more broadly, algorithmic game theory). For instance, Kumabe and Mihara apply this result to an investigation of the Nakamura numbers for simple games in cooperative game theory and social choice theory.