In a previous post, I discussed decision problems, decidability, complexity classes, and the Halting problem. In computability theory, Rice’s theorem is an important result that can be thought of as an extension of the Halting Theorem. Rice’s Theorem is a fundamental concept in computer science within automata theory and computational theory.

The undecidability of the Halting Problem means that there exists no universal algorithm that decides whether or not a program will terminate. Rice’s theorem generalizes the result from halting or termination to any non-trivial semantic property. Properties of programs can be classified broadly into two categories: syntactic (relating to the syntax, i.e. the structure and contents) and semantic (relating to the semantics, i.e. the meaning and behaviour). A semantic property is one that describes the behaviour and output of a program, such as whether it terminates or not. A syntactic property is related to its actual syntax, such as how many while loops it contains. Understanding a semantic property requires more than just examining the code; it often involves running and testing it, and examining its output. A non-trivial property is one that not a vacuous statement, i.e. which is neither true nor false for every program.

Rice’s theorem states that every non-trivial semantic property of a program (such as its halting behaviour) is undecidable. More precisely, consider the following problem $P$, which takes as input a program P and outputs “true” if $P$ satisfies a specific semantic property $S$ holds true about $P$. Then, Rice’s theorem says that this problem is undecidable, i.e. there exists no universal algorithm A corresponding to property S which solves the problem $Pr$ for all inputs. Thus, Rice’s theorem is a generalization of the undecidability of the Halting problem.

Rice’s theorem is very powerful and has far-reaching implications on the feasibility of static analysis of programs. For instance, it implies that it is impossible to build a universal tool (program) that checks whether a given program is correct, or even if it is free from bugs and executes without running into an error.

The proof for Rice’s theorem involves a reduction from the halting problem, which, as discussed, is undecidable. The proof is sketched out as follows. We first fix the semantic property $S$ to be “is an implementation of the squaring function, which takes an integer $d$ and returns $d_2$. If Rice’s theorem is false, then there exists an algorithm $A$ for examining a program $P$ and determining infallibly whether $P$ satisfies $S$, i.e. whether or not $P$  is an implementation of the squaring function.

The proof would work if we replaced $S$ with any other non-trivial semantic property of a program behavior. We now show that algorithm A for identifying squaring programs can be converted into can also identify functions that halt.

Let $B$ be an arbitrary program with input $i$. Consider a new program $t$ with input a number $n$, which first executes program $B$ on input $i$ (both B and i are hard-coded into t), and then returns the square of $n$. If $n$ runs forever, then $t$ never gets to the second step, regardless of $n$. Thus, $t$ is a function for computing squares if and only if the first step of computing $n$ terminates.

By our assumption, we have an algorithm $A$ which examines a program and determines if they compute squares. Thus, A can, in particular, decide this property for $t$. But, this means exactly that $A$ decides whether the program $B$ halts on input $i$. We can extend this argument by constructing programs with the first step being any program with any input, and the second step being the squaring operation. Thus, $A$ also decides the halting behaviour of an arbitrary program. Note that our decision algorithm $A$ never executes $t$, but only passes its description to the squaring-identification program, which by assumption always terminates. We therefore have a contradiction to the undecidability of the halting problem, and conclude that such an algorithm $A$ cannot exist, i.e. any semantic property of a program must be undecidable. In fact, Rice’s Theorem is a direct corollary of the undecidability of the Halting problem.