Rice's Theorem

Origin. Rice (1953). Sweeping undecidability result: every non-trivial semantic property of programs is undecidable. Generalizes the halting problem to all extensional properties.

Models. A property of the function a program computes — not of its code — cannot be decided from the code, unless the property is trivial (holds for all or for none).

Formalism.

Index set: For a class C of partial recursive functions, A = {e : φ_e ∈ C}. Extensional: depends only on the computed function.

Rice's theorem: A is recursive iff C = ∅ or C = all partial recursive functions. Every non-trivial C gives an undecidable index set.

Proof sketch: Fix f₀ ∈ C, f₁ ∉ C (or symmetric). Reduce K to A using s-m-n and the recursion theorem. Decidability of A would decide K.

Examples (all undecidable): Totality: {e : φ_e total}. Emptiness of domain: {e : dom(φ_e) = ∅}. Computing a fixed constant. Equivalence φ_e = φ_i.

Rice–Shapiro refinement: The theorem is a necessary condition only. If A = {e : φ_e ∈ C} is r.e., then for every partial recursive f, f ∈ C iff some finite θ ⊆ f has θ ∈ C. (Upward closure follows: if θ ⊆ f ⊆ g and θ ∈ C then g ∈ C.)

The converse fails as stated. The finite-approximation condition is a topological condition — it says C is open in the Scott topology — and openness alone does not make an index set r.e., since C may collect a non-r.e. family of finite functions. The converse needs an effectiveness hypothesis: if in addition the set of canonical indices of finite functions in C is r.e., then A is r.e. That is the Myhill–Shepherdson direction, and together the two say index sets are r.e. exactly when C is effectively open.

Using it: {e : φ_e total} is not even r.e. Take f total, so f ∈ C; Rice–Shapiro would give a finite θ ⊆ f with θ ∈ C, but no finite function is total.

Intensional escape: Properties of the code (states, syntax) can be decidable. "Has exactly five instructions" is decidable — not extensional.

Symbols.

Metatheory. Places all non-trivial extensional program properties outside the decidable. Rice–Shapiro gives the necessary condition at the r.e. level and Myhill–Shepherdson the matching sufficient one. Sharp boundary between intensional (code) and extensional (behavior) properties.

Applies to. Limits of static analysis and verification. Compiler optimization boundaries. Program-equivalence undecidability. Abstract interpretation motivation.

Limitations. Worst-case over all programs; sound approximations still useful. Silent on complexity. Extensionality assumption essential — code properties may be decidable.

© 2026 Lingenic LLC