Rice's theorem, in its formal language version, says: every nontrivial property of the computably enumerable language accepted by a Turing machine has an undecidable set of machine descriptions. Here nontrivial means that some computably enumerable language has the property and some does not. The property must be an extensional property of programs: any two Turing machines accepting the same formal language must agree about it. It need not be a property of all formal languages, including those no Turing machine accepts.
Let be such a property and writeWe prove the theorem by a many-one reduction from the halting problem. First suppose the empty language is not in . Nontriviality provides a fixed Turing machine with . Given a Turing machine and a word over an alphabet , effectively construct a Turing machine which, on input , first simulates on . If that simulation ever halts, it simulates on and accepts precisely when accepts. If the first simulation never halts, it never accepts .
The Turing machine encoding of is computable from those of : the description merely embeds and the fixed simulator for . Constructing it does not require predicting whether halts. Its accepted formal language isConsequentlyA decider for would therefore decide the halting problem, a contradiction. Invalid descriptions can be mapped to a fixed description of a machine accepting the empty language, if the many-one reduction is formulated on all strings.
If the empty language does belong to , apply the preceding argument to the opposite property, within the computably enumerable languages. This opposite property is still nontrivial and excludes the empty language. A hypothetical decider for would decide the opposite property's index set by first rejecting malformed Turing machine encodings and otherwise reversing its answer. The opposite property is undecidable by the first case, giving the required contradiction in this case too.
For example, takeThis is a decidable language: check that the input is a valid Turing machine encoding, count its declared states, and test the count's integer parity. There are Turing machines with even state counts and Turing machines with odd state counts, so the formal language contains some but not all valid descriptions.
There is no contradiction with Rice's theorem because this is a syntactic property of the description. Add one unreachable state to a Turing machine, assigning any permitted transitions to it. The accepted formal language is unchanged, while the integer parity of the state count changes. Thus the property is not an extensional property of programs, which is an essential hypothesis of Rice's theorem.
is undecidable. The condition depends only on the accepted formal language. It holds for a Turing machine accepting the empty language, and fails for a Turing machine accepting the singleton , where is an alphabet symbol. It is therefore a nontrivial extensional property of programs, and Rice's theorem applies. In particular, the condition does not assert that the machine halts on every input; nonacceptance of long words over an alphabet may result from rejection or from an infinite computation.
is a decidable language: it consists of every valid Turing machine encoding. Every multitape Turing machine has an equivalent single-tape Turing machine. To see this, represent the finitely used portions of its tapes on one tape, separated by delimiters, and mark each simulated head position. To simulate one step, scan these portions to read the marked symbols, retain this fixed number of symbols and the control state in finite control, and scan again to update the symbols and head marks. Extend a represented portion with a blank cell when necessary. Each simulated step takes finitely many real steps.
The single-tape Turing machine accepts exactly when the simulated multitape Turing machine accepts; infinite computations remain infinite. The simulation may increase time complexity, but the question only asks about accepted formal languages. Hence a decider simply checks the syntax of the Turing machine encoding and accepts every valid description. Rice's theorem does not make this property undecidable, because the property is true of every computably enumerable language and is therefore trivial in the theorem's sense.