Rice’s Theorem and the Collapse of Semantic Properties

Static analysis tools answer questions about programs. The questions they can answer exactly and for all programs form a sharply limited class, and the boundary is drawn by a theorem from 1953 that applies to any language a program might compute, in any programming language, on any machine model. The theorem does not say analysis is hard in practice. It says that for a large class of questions, no program that always halts can answer them correctly.

Properties of the function, not of the text

The distinction that carries the theorem is between syntactic and semantic properties. A syntactic property is a predicate on the description of a program: does the text contain a while loop, does the description exceed 500 characters, does the machine have an even number of states. These are decidable, trivially, by examining the description.

A semantic property is a predicate on the function the program computes, that is, on the set of strings it accepts. “The program accepts at least one string” is semantic. “The program accepts the empty string” is semantic. “The program accepts exactly the strings of even length” is semantic. “The program’s description mentions a counter variable” is not.

Formally, a property P of recognizable languages is a set of languages. A machine M has property P when L(M) ∈ P. The property is nontrivial when at least one recognizable language has it and at least one does not. Rice’s theorem states: for every nontrivial P, the set {⟨M⟩ : L(M) ∈ P} is undecidable.

Two extreme properties must be excluded, and they are exactly the trivial ones. The empty property, which no language satisfies, gives the empty set of descriptions, decidable by a machine that always rejects. The universal property, which every language satisfies, gives the set of all descriptions, decidable by a machine that always accepts after a parse check. Every property strictly between the two is undecidable.

The theorem is sometimes stated for partial computable functions rather than recognizable languages. The two formulations are the same statement, because a partial function and its domain correspond, and the domain of a partial computable function is a recognizable set. Programs that may fail to terminate on some inputs are therefore covered. The reduction that proves the theorem is the standard one-way map, and it is worth reading alongside the general account of direction and polarity in Mapping Reductions and the Halting Problem.

Smuggling halting into an arbitrary property

The proof reduces the acceptance problem to a trivial variant of the property set, with the choice depending on a single case split. Nontriviality supplies a recognizable language L₀ with a machine M₀ on the needed side of the property, which is all the construction requires.

Given ⟨M, w⟩, construct a machine N that behaves as follows on input x: first run M on w, but abort as soon as M halts, whichever state it halts in; then run M₀ on x and answer as M₀ does; and if M runs forever, N runs forever on every x and answers nothing. Equivalently, N ignores its own input until the halting question about M on w is settled, and only then behaves like a machine whose language was chosen in advance.

Now examine L(N). If M halts on w, the first stage completes and N behaves exactly as M₀, so L(N) = L₀, including the case where M halts by rejecting. If M never halts on w, N never reaches the second stage on any x, so N accepts nothing and L(N) = ∅. The non-halting branch is what forces the empty language; a wrapper that treated halting-with-rejection as a separate case would need a third behaviour and would no longer be this simple.

When ∅ lacks the property, take L₀ with the property. Halting gives L(N) = L₀ ∈ P, and non-halting gives L(N) = ∅ ∉ P. So HALT ≤_m {⟨N⟩ : L(N) ∈ P}, and the property set is undecidable by Mapping Reductions and the Halting Problem.

When ∅ has the property, take L₀ without the property instead. Halting gives L(N) = L₀ ∉ P, and non-halting gives L(N) = ∅ ∈ P. So the reduction maps HALT to the complement of the property set. A decider for the property set decides its complement by swapping the accept and reject states, so the complement is undecidable exactly when the property set is, and the property set is undecidable in this case too.

Two features of the construction are doing all the work. The non-halting branch produces ∅ rather than a second witness language, which removes the need for any witness on the empty side and makes the same wrapper serve both cases. And the choice of M₀ is the only place the property enters, so the reduction is one construction plus a single case split on whether ∅ has the property.

Why the reduction is uniform

The proof is a reduction, and its uniformity is what makes the theorem strong. The construction of N depends on P only through the choice of the witness language L₀ and its machine M₀, a single value fixed by the property. Once that is fixed, the map from ⟨M, w⟩ to ⟨N⟩ is a simple syntactic transformation: prepend a simulation of M on w that stops when M halts, then append M₀. The theorem quantifies over P, but each instance of the theorem is proved by the same three-line transformation.

So the undecidability is not a property of any particular question. It is inherited from the fact that a program’s behaviour can be made conditional on an arbitrary computation. Any question about behaviour that can distinguish two machines can be made to encode “does M halt on w”. The theorem’s power comes from quantifying over all nontrivial P at once.

Which questions survive

The theorem’s boundary is precise, and the questions on the decidable side are exactly those that can be answered from the description without knowing the language.

• Syntactic checks. Whether a program contains a specific construct, whether it parses, whether its description is under a size limit. All decidable, all uninteresting as semantic facts.
• Approximate analyses. A tool that says “definitely yes”, “definitely no”, or “unknown” is not a decider for the property; it is a sound approximation. Rice’s theorem forbids exact answers, not useful ones. The “unknown” bucket is where all real static analysis lives, and its size is a design parameter.
• Restricted program classes. Total languages, primitive-recursive programs, finite-state programs, and languages with bounded recursion have decidable properties precisely because they are not Turing-complete. The price is expressiveness.
• Bounded questions. “Does this program accept w within 1000 steps” is decidable, because the search space is finite. “Does it accept w” is not.

The last two are the escape routes that matter in practice, and they are the reason the theorem does not make program analysis impossible. It makes it necessarily approximate or necessarily restricted.

A sound approximation returns three values, and the third is where the theorem is respected:

UNKNOWN = None

# Decidable syntactic facts map to the semantic verdict they license.
# Each fact is checkable by inspection of the program's description.
RULES = [
    ('entry-block-accepts-unconditionally', True),
    ('every-return-statement-is-a-literal-accept', True),
    ('contains-a-call-to-an-unanalysed-foreign-function', UNKNOWN),
]

def classify(facts):
    """facts: set of decidable syntactic facts about one program."""
    verdicts = {verdict for fact, verdict in RULES if fact in facts}
    if len(verdicts) == 1:
        return verdicts.pop()          # every applicable rule agrees
    return UNKNOWN                     # conflicting rules: no claim is made

Every rule is a syntactic test that a checker performs in bounded time, and the function never returns the negated verdict. That asymmetry is deliberate: asserting that not all inputs are accepted would require deciding a semantic fact, which the theorem forbids.

The same shape in other guises

Rice’s theorem is a template that recurs wherever a system can encode arbitrary computation. A few instances, stated without proof, share the exact structure.

Virus detection. Deciding whether a program is malicious is a semantic question if maliciousness is defined by behaviour. If it is defined by a signature — a byte pattern — it is syntactic and decidable. The gap between these two definitions is the gap between what signature scanners can do and what they cannot.

Compiler optimisation legality. Whether a transformation preserves the observable behaviour of every possible input is a semantic question about two programs. Compilers answer it by proving conservative approximations: a transformation is applied only when a syntactic side condition guarantees equivalence.

Equivalence checking. Deciding whether two programs compute the same function is the property “L(M₁) = L(M₂)”, a two-machine question rather than a one-machine property. It is undecidable by a direct reduction, and it is the reason equivalence checkers are restricted to finite-state models or to bounded unrolling.

Termination analysis. “M halts on every input” is the property L(M) = Σ*, which is nontrivial and therefore undecidable. Termination tools escape by giving up on the general question and looking for a specific witness of termination: a well-founded order that every rewrite step decreases, such as a recursive path ordering or a polynomial interpretation. Finding one such order can be automated, but its existence is a sufficient condition rather than a decision, and the general guarantee is lost.

What the theorem does not say

Three misreadings are common enough to be worth refuting explicitly.

The theorem does not say that no property of a specific program is decidable. For any fixed program, its language is a fixed set, and every individual set is decidable by a machine with a lookup table or by a machine that ignores the input. Undecidability is a statement about the uniform question across all programs. A tool may know a great deal about a particular program.

The theorem does not say that all interesting questions are undecidable. It says that nontrivial semantic properties are. A property that holds of every recognizable language, or of none, is trivial and decidable; a property that is syntactic is decidable; and a property of a restricted class may be decidable even when the class’s general form is not.

The theorem does not depend on the programming language. It holds for any acceptable numbering of machines, meaning any enumeration in which the map from index to machine is computable and the universal machine exists. Every general-purpose language and every machine model satisfies this, which is why the theorem is stated about machines and applies to languages without change. The invariance is the content of the Church–Turing thesis applied to descriptions rather than to computations.

Where the theorem is genuinely silent is complexity. It says nothing about how hard the decidable restrictions are. A property may be decidable but require exponential time, and that is a separate question with its own machinery, as the gap between decidability and tractability in Decision Procedures for Word Equations and Unification illustrates. The undecidability boundary and the tractability boundary are different boundaries, and conflating them produces bad arguments in both directions.