Райс теоремасы: Есептеу теориясының шектеулері

Theorem in computability theory
In computability theory, Rice's theorem states that all non trivial semantic properties of programs are undecidable. A semantic property is one about the program's behavior (for instance, "does the program terminate for all inputs? "), unlike a syntactic property (for instance, "does the program contain an if then else statement?"). A non trivial property is one which is neither true for every program, nor false for every program. 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 a given program is correct, or even executes without error. 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. One can distinguish between the syntax of a program, and its semantics. The syntax is the detail of how the program is written, or its "intension", and the semantics is how the program behaves when run, or its "extension". Rice's theorem asserts that it is impossible to decide a property of programs which depends only on the semantics and not on the syntax, unless the property is trivial (true of all programs, or false of all programs). By Rice's theorem, it is impossible to write a program that automatically verifies for the absence of bugs in other programs, taking a program and a specification as input, and checking whether the program satisfies the specification. This does not imply an impossibility to prevent certain types of bugs. 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. On the other hand, statically typed programming languages feature a type system which statically prevents type errors. In essence, this should be understood as a feature of the syntax (taken in a broad sense) of those languages. In order to type check a program, its source code must be inspected; the operation does not depend merely on the hypothetical semantics of the program. In terms of general software verification, this means that although one cannot algorithmically check whether a given program satisfies a given specification, one can require programs to be annotated with extra information that proves the program is correct, or to be written in a particular restricted form that makes the verification possible, and only accept programs which are verified in this way. In the case of type safety, the former corresponds to type annotations, and the latter corresponds to type inference. Taken beyond type safety, this idea leads to correctness proofs of programs through proof annotations such as in Hoare logic. Another way of working around Rice's theorem is to search for methods which catch many bugs, without being complete. This is the theory of abstract interpretation. 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. Let P be a subset of Suppose that:
P is non trivial: P is neither empty nor itself. P is extensional: for all integers m and n, if φm = φn, then m ∈ P ⟺ n ∈ P.
Then P is undecidable. A more concise statement can be made in terms of index sets: The only decidable index sets are ∅ and .

Assume for contradiction that is a non trivial, extensional and computable set of natural numbers. There is a natural number and a natural number Define a function by when and when By Kleene's recursion theorem, there exists such that Then, if , we have , contradicting the extensionality of since , and conversely, if , we have , which again contradicts extensionality since .