Classes of Recursively Enumerable Sets and Their Decision Problems
Reference: Rice, H. G. (1953). Classes of recursively enumerable sets and their decision problems. Transactions of the American Mathematical Society, 74(2), 358–366. DOI 10.2307/1990888. Based on Rice’s 1951 Princeton PhD thesis under Alonzo Church.
Summary
A nine-page paper that established one of the most consequential results in computability theory — now universally known as Rice’s Theorem. Rice’s question: given a class C of recursively enumerable (r.e.) sets, is there an effective procedure that, applied to a Gödel number (index) of an r.e. set W, decides whether W ∈ C? The paper’s central result is that the answer is no whenever C is a non-trivial extensional property — i.e. whenever C is neither empty nor the whole collection of r.e. sets, and membership in C depends only on which set is described, not on how it is described. Every property of the computed function itself (as opposed to syntactic properties of the program text) is therefore undecidable.
The proof is a reduction from the halting problem (Turing’s K). Rice constructs, for an arbitrary index i, a machine whose r.e. set is either a fixed element of C or a fixed element of its complement depending on whether φ_i(i) halts; a decision procedure for C would then decide K, which is known impossible. The technique — parametric construction of “switch” machines that toggle semantic behaviour based on a halting oracle — is the template used throughout undecidability theory for subsequent results (Rogers’ isomorphism theorem, the Myhill isomorphism, the theory of m-reducibility).
Beyond the headline theorem, the paper classifies decision problems about r.e. sets by the logical complexity of the class C: some non-trivial classes are Σ₁-hard, others Π₁-hard, others fall at higher levels of the arithmetical hierarchy. This classification anticipates the later development of degree theory. The paper is short, elementary, and entirely foundational: it tells us, once and for all, that semantic questions about arbitrary programs cannot be answered by mechanical inspection. Every program-analysis, verification, and capability-bounding enterprise since has been organised around the frontier Rice drew — by restricting the class of programs considered, approximating (sound-but-incomplete), or proving properties syntactically rather than semantically.
Key Ideas
- Theorem B (Rice’s Theorem): for any non-trivial class
Cof r.e. sets, the problem of deciding whether a given r.e. set belongs toCis undecidable. - Extensional vs. intensional properties:
Cmust depend on what is computed (the set), not on how (the index/program text). Intensional properties (program size, presence of a given opcode) can be decidable. - Proof by reduction from the halting problem, via a parametric “switch” construction that conditionally produces an element of
Cor its complement depending on whether a reference computation halts. - Arithmetical hierarchy classification of classes of r.e. sets by the quantifier complexity of their defining predicates, foreshadowing Kleene’s and Rogers’ later work.
- Implicit corollary: every tool that claims to decide a non-trivial semantic property of arbitrary programs must either (i) restrict the input class, (ii) approximate, or (iii) violate computability.
Connections
- Rice’s Theorem
- Halting Problem
- Computability
- Universal Turing Machine
- Recursive Function
- Inductive Inference
- Formal Verification
- Static Analysis
- Security Applications Of Formal Language Theory
- The Halting Problems of Network Stack Insecurity
- House on Rock - LangSec in Ethereum Classic
- Assigning Meanings to Programs
- Program Verification
Conceptual Contribution
- Claim: There is no uniform effective procedure that decides any non-trivial extensional property of recursively enumerable sets; equivalently, every non-trivial semantic property of the partial function computed by an arbitrary program is undecidable.
- Mechanism: Given a hypothesised decision procedure for a non-trivial class
C, and a distinguishing pairA ∈ C,B ∉ C, construct for each indexia machineM_ithat simulatesφ_i(i)and, if it halts, begins enumeratingA; otherwise enumeratesB. The set enumerated byM_iis inCiffφ_i(i)halts, so a decision procedure forCwould decide the halting problem — contradiction. - Concepts introduced/used: Rice’s Theorem, Halting Problem, Computability, Recursive Function, Universal Turing Machine
- Stance: foundational theorem paper (computability theory)
- Relates to: Generalises Turing’s halting theorem from the specific property “halts on input x” to all non-trivial semantic properties; sets the decidability frontier that all subsequent work in Formal Verification, Static Analysis, and LangSec (Security Applications Of Formal Language Theory, The Halting Problems of Network Stack Insecurity) must respect; directly underwrites the Rice’s-theorem argument in House on Rock - LangSec in Ethereum Classic that Ethereum’s gas mechanism cannot deliver a semantic safety guarantee.
Bibliography (Rice 1953)
- An Unsolvable Problem of Elementary Number Theory — Church, Alonzo. An unsolvable problem of elementary number theory, American Journal of Mathematics 58(2) (1936), 345–363.
- Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I — Gödel, Kurt. Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I, Monatshefte für Mathematik und Physik 38 (1931), 173–198.
- General Recursive Functions of Natural Numbers — Kleene, Stephen C. General recursive functions of natural numbers, Mathematische Annalen 112 (1936), 727–766.
- On Notation for Ordinal Numbers — Kleene, Stephen C. On notation for ordinal numbers, Journal of Symbolic Logic 3(4) (1938), 150–155.
- Recursive Predicates and Quantifiers — Kleene, Stephen C. Recursive predicates and quantifiers, Transactions of the American Mathematical Society 53 (1943), 41–73.
- On Definable Sets of Positive Integers — Mostowski, Andrzej. On definable sets of positive integers, Fundamenta Mathematicae 34 (1946), 81–112.
- Recursively Enumerable Sets of Positive Integers and Their Decision Problems — Post, Emil L. Recursively enumerable sets of positive integers and their decision problems, Bulletin of the American Mathematical Society 50 (1944), 284–316.
- Extensions of Some Theorems of Gödel and Church — Rosser, J. Barkley. Extensions of some theorems of Gödel and Church, Journal of Symbolic Logic 1(3) (1936), 87–91.
Tags
#computability #undecidability #foundational #halting-problem #verification