Main Page

encyclopedia.codeboy.net

 

Rice's theorem

Category:Recursion theoryCategory:Theorems Rice's theorem (also known as The Rice-Myhill-Shapiro theorem) is an important result in the theory of\nrecursive functions. A property of partial functions is\ntrivial if it holds for all partial recursive functions or for\nnone. Rice's theorem states that, for any non-trivial property of\npartial functions, the question of whether a given algorithm computes\na partial function with this property is undecidable. Using Rogers' characterization of acceptable programming systems, this result may essentially be generalized to most computer programming languages: there exists no automatic method that decides with generality non-trivial questions on the final behavior of computer programs. This is one explanation of the difficulty of debugging. As an example, consider the following variant of the \nhalting problem: Take the property a partial function F has if F\nis defined for argument 1. It is obviously non-trivial, since there\nare partial functions that are defined for 1 and others that are\nundefined at 1. The 1-halting problem is the problem of deciding\nof any algorithm whether it defines a function with this property,\ni.e., whether the algorithm halts on input 1. By Rice's theorem, the\n1-halting problem is undecidable.

Proof

Suppose, for concreteness, that we have an algorithm for examining a\nprogram p and determining infallibly whether or not p is an\nimplementation of the squaring function, which takes an integer d and\nreturns d2. The proof works just as well if we have an\nalgorithm for deciding any other nontrivial property of programs, and\nwill be given in general below. The claim is that we can convert our algorithm for identifying\nsquaring programs into one which identifies functions that halt. We\nwill describe an algorithm which takes inputs a and i and determines\nwhether program a halts when given input i. The algorithm\nis simple: we construct a new program t which (1) temporarily ignores its input while it tries to \nexecute program a on input i, and then, if that halts, (2) returns the square of its input. Clearly, t is a function for computing squares if and only if step (1) halts. Since we've assumed that we can infallibly identify program for computing squares, we can determine whether t is such a program, and therefore whether program a halts on input i. Note that we needn't actually execute t; we need only decide whether it is a squaring program, and, by hypothesis, we know how to do this. This method doesn't depend specifically on being able to recognize functions that compute squares; if we could had a method for recognizing programs for computing square roots, or programs for \ncomputing the monthly payroll, or programs that halt when given the input "Abraxas", or programs that commit array bounds errors, we would be able to solve the halting problem similarly. For the formal proof, algorithms are presumed to define partial\nfunctions over
strings and are themselves represented by\nstrings. The partial function computed by the algorithm represented by\na string a is denoted Fa. This proof proceeds\nby reductio ad absurdum: we assume that there is a non-trivial\nproperty that is decided by an algorithm, and then show that it\nfollows that we can decide the halting problem, which is not\npossible, and therefore a contradiction. Let us now assume that P(a) is an algorithm that decides some\nnon-trivial property of Fa. Without loss of\ngenerality we may assume that P(no-halt) = "no", with\nno-halt being the representation of an algorithm that never\nhalts. If this is not true, then this will hold for the negation of\nthe property. Since P decides a non-trivial property, it follows\nthat there is a string b that represents an algorithm and\nP(b) = "yes". We can then define an algorithm H(a,\ni) as follows:
1. construct a string t that represents an algorithm T such that \n:* T first simulates the computation of Fa(i) \n:* then T simulates the computation of Fb(d) and returns its result. \n:2. return P(t)
We can now show that H decides the halting problem:
  • Assume that the algorithm represented by a halts on input i. In this case Ft = Fb and, because P(b) = "yes" and the output of P(x) depends only on Fx, it follows that P(t) = "yes" and, therefore H(a, i) = "yes".
  • Assume that the algorithm represented by a does not halt on input i. In this case Ft = Fno-halt, i.e., the partial function that is never defined. Since P(no-halt) = "no" and the output of P(x) depends only on Fx, it follows that P(t) = "no" and, therefore H(a, i) = "no".
Since the halting problem is known to be undecidable, this is a\ncontradiction and the assumption that there is an algorithm\n'\'P(a) that decides a non-trivial property for the function\nrepresented by a'' must be false.

"Don't let it end like this. Tell them I said something." - last words of Pancho Villa (1877-1923)