Rice's theorem

In computability theory, Rice's theorem states that all non-trivial semantic properties of programs are undecidable.

"), unlike a syntactic property (for instance, "does the program contain an if-then-else statement?").

The theorem generalizes the undecidability of the halting problem.

It has far-reaching implications on the feasibility of static analysis of programs.

It implies that it is impossible, for example, to implement a tool that checks whether any given program is correct, or even executes without error (it is possible to implement a tool that always overestimates or always underestimates, so in practice one has to decide what is less of a problem).

The theorem is named after Henry Gordon Rice, who proved it in his doctoral dissertation of 1951 at Syracuse University.

Rice's theorem puts a theoretical bound on which types of static analysis can be performed automatically.

For example, Rice's theorem implies that in dynamically typed programming languages which are Turing-complete, it is impossible to verify the absence of type errors.

In essence, this should be understood as a feature of the syntax (taken in a broad sense) of those languages.

Another way of working around Rice's theorem is to search for methods which catch many bugs, without being complete.

Yet another direction for verification is model checking, which can only apply to finite-state programs, not to Turing-complete languages.

Let φ be an admissible numbering of partial computable functions.

is a non-trivial, extensional and computable set of natural numbers.

Suppose, for concreteness, that we have an algorithm for examining a program p and determining infallibly whether p is an implementation of the squaring function, which takes an integer d and returns d2.

The proof works just as well if we have an algorithm for deciding any other non-trivial property of program behavior (i.e. a semantic and non-trivial property), and is given in general below.

The algorithm for deciding this is conceptually simple: it constructs (the description of) a new program t taking an argument n, which (1) first executes program a on input i (both a and i being hard-coded into the definition of t), and (2) then returns the square of n. If a(i) runs forever, then t never gets to step (2), regardless of n. Then clearly, t is a function for computing squares if and only if step (1) terminates.

Note that our halting-decision algorithm never executes t, but only passes its description to the squaring-identification program, which by assumption always terminates; since the construction of the description of t can also be done in a way that always terminates, the halting-decision cannot fail to halt either.

This method does not depend specifically on being able to recognize functions that compute squares; as long as some program can do what we are trying to recognize, we can add a call to a to obtain our t. We could have had a method for recognizing programs for computing square roots, or programs for computing the monthly payroll, or programs that halt when given the input "Abraxas"; in each case, we would be able to solve the halting problem similarly.

The partial function computed by the algorithm represented by a string a is denoted Fa.

This proof proceeds by reductio ad absurdum: we assume that there is a non-trivial property that is decided by an algorithm, and then show that it follows that we can decide the halting problem, which is not possible, and therefore a contradiction.

Let us now assume that P(a) is an algorithm that decides some non-trivial property of Fa.

If this is not true, then this holds for the algorithm P that computes the negation of the property P. Now, since P decides a non-trivial property, it follows that there is a string b that represents an algorithm Fb and P(b) = "yes".

We can then define an algorithm H(a, i) as follows: We can now show that H decides the halting problem: Since the halting problem is known to be undecidable, this is a contradiction and the assumption that there is an algorithm P(a) that decides a non-trivial property for the function represented by a must be false.