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: An index set is r.e. iff C is closed under the "finite approximation" condition: f ∈ C iff some finite subfunction of f is in C, and C upward closed.

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

Symbols.

Symbol	Unicode	Name	Meaning
φ_e	—	Program	e-th partial recursive function
C	—	Property class	Set of functions
A	—	Index set	{e : φ_e ∈ C}
≤_m	—	Reduction	Many-one

Metatheory. Places all non-trivial extensional program properties outside the decidable. Rice-Shapiro locates exactly which lie at the r.e. level. 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.