Having seen that the halting problem is undecidable, one may wonder whether it is an isolated case. Rice's theorem says it is not: it is the rule. Any non-trivial question about the behaviour of a program, that is about the function it computes or the language it recognizes, is undecidable. It is one of the most general and most practical results in computability theory, because it pins down precisely what automatic verification tools can and cannot do.
Semantic and syntactic properties
We need to distinguish two kinds of question about a Turing machine M.
Syntactic properties concern M's description, its "text".
- Does M have more than 20 states?
- Does M contain a transition that writes the symbol X?
- Does M enter state q₅ within the first 100 steps on the empty input?
Many of these are decidable: just read the description or simulate a bounded number of steps.
Semantic properties concern only the language L(M) recognized by M. Two machines recognizing the same language either both have the property or both lack it.
- Is L(M) empty?
- Does L(M) contain the string 0101?
- Is L(M) finite?
- Is L(M) regular?
- Is L(M) = Σ*, that is does M accept everything?
Rice's theorem is about the latter.
The statement
Let P be a property of Turing-recognizable languages. P is non-trivial if at least one machine's language has the property and at least one machine's language does not. Then:
the language {⟨M⟩ : L(M) has property P} is undecidable.
There are only two trivial properties: the one that holds for every recognizable language and the one that holds for none. For these the answer is always yes or always no, and deciding is immediate.
The idea of the proof
We reduce A_TM, already known to be undecidable, to the problem of deciding P.
Assume, without loss of generality, that the empty language does not have property P (otherwise argue about the complement of P). Since P is non-trivial, there is a machine T whose language L(T) has the property.
Given a pair ⟨M, w⟩, build a machine M′ that, on input x:
- simulates M on w;
- if M accepts w, runs T on x and answers as T does.
Now observe:
- if M accepts w, M′ behaves like T, so L(M′) = L(T), which has the property;
- if M does not accept w, M′ accepts nothing, so L(M′) = ∅, which lacks the property.
A decider for P, applied to ⟨M′⟩, would decide whether M accepts w. Since building M′ from ⟨M, w⟩ is mechanical, we would get a decider for A_TM, which does not exist.
Examples of application
| Question | Semantic? | Non-trivial? | Decidable? |
|---|---|---|---|
| Is L(M) empty? | Yes | Yes | No |
| Does L(M) contain the empty string? | Yes | Yes | No |
| Is L(M) regular? | Yes | Yes | No |
| Does M have at least 10 states? | No | — | Yes |
| On the empty input, does M ever move its head left? | No | — | Yes, with a dedicated argument |
| Is L(M) recognizable? | Yes | No, it is trivial | Yes (the answer is always yes) |
The row on moving left is instructive: it is a property of the machine, not of the language, so Rice does not apply. It is shown decidable by noting that a machine that always moves right, once past the input, reads only blanks and so either halts or repeats a state within a bounded number of steps.
Consequences for real software
Translated into the language of programs, Rice's theorem says there is no analyzer that, for every program, correctly decides:
- whether the program always returns the right result with respect to a specification;
- whether two programs compute the same function;
- whether a program can ever produce a certain output, such as printing a password;
- whether a program contains code that will actually run on some input;
- whether an executable file, once launched, will behave maliciously.
The last point has a concrete meaning in security: no antivirus can recognize with certainty, in every case, exactly the malicious programs, if "malicious" is defined in terms of behaviour.
How we work anyway
The theorem does not doom automatic analysis, but it forces trade-offs. The approaches used in practice are:
- Sound approximation: the analyzer may raise false alarms but never miss real problems (or the other way round). This is the approach of many static analysis tools and of type systems.
- Restricting the language: on programs without unbounded loops, or on finite-state models, many questions become decidable. Model checking exploits this.
- Syntactic properties: signatures and byte-sequence rules look at the program's text, not its behaviour, which is why they are decidable; the price is that they can be evaded by changing the code.
- Assisted verification: a human provides invariants and proofs, and the machine merely checks them.
In short
- Semantic properties depend only on the language recognized, not on the program text.
- Rice's theorem: every non-trivial semantic property is undecidable.
- The proof reduces A_TM by building a machine that either behaves like T or accepts nothing.
- Syntactic properties, such as the number of states, often remain decidable.
- Real tools live with the theorem through approximation, restriction and assisted verification.
