<<Up     Contents

Rice's theorem

Redirected from Rices theorem

Rice's theorem is an important result in the theory of recursive functions. A property of partial functions is trivial if it holds for all partial recursive functions, or for none. Rice's theorem states that for any non-trivial property of partial functions, the question of whether a given algorithm computes a partial function with this property is undecidable.

As an example, consider the following variant of the halting problem: Take the property a partial function F has if F is defined for argument 1. It is obviously non-trivial, since there are partial functions which are defined for 1 and others which are undefined at 1. The 1-halting problem is the problem of deciding of any algorithm whether it defines a function with this property, i.e., whether the algorithm halts on input 1. By Rice's theorem, the 1-halting problem is undecidable.

Sketch of Proof

Algorithms are presumed here to define partial functions over strings, and are themselves represented by strings. The partial function computed by the algorithm represented by a string a is denoted as 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. Without loss of generality we may assume that P(no-halt) = "no" with no-halt the representation of an algorithm that never halts. If this is not the case then this will hold for the negation of the property. Since P decides a non-trivial property it follows that there is a string b that represents an algorithm 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.

wikipedia.org dumped 2003-03-17 with terodump