Rice–Shapiro theorem explained

In computability theory, the Rice–Shapiro theorem is a generalization of Rice's theorem, named after Henry Gordon Rice and Norman Shapiro. It states that when a semi-decidable property of partial computable functions is true on a certain partial function, one can extract a finite subfunction such that the property is still true.

The informal idea of the theorem is that the "only general way" to obtain information on the behavior of a program is to run the program, and because a computation is finite, one can only try the program on a finite number of inputs.

A closely related theorem is the Kreisel-Lacombe-Shoenfield-Tseitin theorem, which was obtained independently by Georg Kreisel, Daniel Lacombe and Joseph R. Shoenfield, and by Grigori Tseitin.

Formal statement

Rice-Shapiro theorem. Let P be a set of partial computable functions such that the index set of P (i.e., the set of indices e such that φeP, for some fixed admissible numbering φ) is semi-decidable. Then for any partial computable function f, it holds that P contains f if and only if P contains a finite subfunction of f (i.e., a partial function defined in finitely many points, which takes the same values as f on those points).

Kreisel-Lacombe-Shoenfield-Tseitin theorem. Let P be a set of total computable functions such that the index set of P is decidable with a promise that the input is the index of a total computable function (i.e., there is a partial computable function D which, given an index e such that φe is total, returns 1 if φeP and 0 otherwise; D(e) need not be defined if φe is not total). We say that two total functions f, g "agree until n" if for all kn it holds that f(k) = g(k). Then for any total computable function f, there exists n such that for all total computable function g which agrees with f until n, fPgP.

Discussion

The two theorems are closely related, and also relate to Rice's theorem. Specifically:

Examples

By the Rice-Shapiro theorem, it is neither semi-decidable nor co-semi-decidable whether a given program:

By the Kreisel-Lacombe-Shoenfield-Tseitin theorem, it is undecidable whether a given program which is assumed to always terminate:

Proof of the Rice-Shapiro theorem

Let P be a set of partial computable functions with semi-decidable index set.

Upward closedness

We first prove that P is an upward closed set, i.e., if fg and fP, then gP (here, fg means that f is a subfunction of g, i.e., the graph of f is contained in the graph of g). The proof uses a diagonal argument typical of theorems in computability.

Assume for contradiction that there are two functions f and g such that fP, gP and fg. We build a program p as follows. This program takes an input x. Using a standard dovetailing technique, p runs two tasks in parallel.

We distinguish two cases.

Extracting a finite subfunction

Next, we prove that if P contains a partial computable function f, then it contains a finite subfunction of f. Let us fix a partial computable function f in P. We build a program p which takes input x and runs the following steps:

Suppose that φpP. This implies that the semi-algorithm for semi-deciding P used in the first step never returns true. Then, p computes f, and this contradicts the assumption fP. Thus, we must have φpP, and the algorithm for semi-deciding P returns true on p after a certain number of steps n. The partial function φp can only be defined on inputs x such that xn, and it returns f(x) on such inputs, thus it is a finite subfunction of f that belongs to P.

Conclusion

It only remains to assemble the two parts of the proof. If P contains a partial computable function f, then it contains a finite subfunction of f by the second part, and conversely, if it contains a finite subfunction of f, then it contains f, because it is upward closed by the first part. Thus, the theorem is proved.

Proof of the Kreisel-Lacombe-Shoenfield-Tseitin theorem

Preliminaries

A total function

h:N\rarrN

is said to be ultimately zero if it always takes the value zero except for a finite number of points, i.e., there exists N such that for all nN, h(n) = 0. Note that such a function is always computable (it can be computed by simply checking if the input is in a certain predefined list, and otherwise returning zero).

We fix U a computable enumeration of all total functions which are ultimately zero, that is, U is such that:

We can build U by standard techniques (e.g., for increasing N, enumerate ultimately zero functions which are bounded by N and zero on inputs larger than N).

Approximating by ultimately zero functions

Let P be as in the statement of the theorem: a set of total computable functions such that there is an algorithm which, given an index e and a promise that φe is computable, decides whether φeP.

We first prove a lemma: For all total computable function f, and for all integer N, there exists an ultimately zero function h such that h agrees with f until N, and fPhP.

To prove this lemma, fix a total computable function f and an integer N, and let B be the boolean fP. Build a program p which takes input x and takes these steps:

Clearly, p always terminates, i.e., φp is total. Therefore, the promise to P run on p is fulfilled.

Suppose for contradiction that one of f and φp belongs to P and the other does not, i.e., (φpP) ≠ B. Then we see that p computes f, since P does not return B on p no matter the amount of steps. Thus, we have f = φp, contradicting the fact that one of f and φp belongs to P and the other does not. This argument proves that fPφpP. Then, the second step makes p return zero for sufficiently large x, thus φp is ultimately zero; and by construction (due to the first step), φp agrees with f until N. Therefore, we can take h = φp and the lemma is proved.

Main proof

With the previous lemma, we can now prove the Kreisel-Lacombe-Shoenfield-Tseitin theorem. Again, fix P as in the theorem statement, let f a total computable function and let B be the boolean "fP". Build the program p which takes input x and runs these steps:

We first prove that P returns B on p. Suppose by contradiction that this is not the case (P returns ¬B, or P does not terminate). Then p actually computes f. In particular, φp is total, so the promise to P when run on p is fulfilled, and P returns the boolean φpP, which is fP, i.e., B, contradicting the assumption.

Let n be the number of steps that P takes to return B on p. We claim that n satisfies the conclusion of the theorem: for all total computable function g which agrees with f until n, it holds that fPgP. Assume by contradiction that there exists g total computable which agrees with f until n and such that (gP) ≠ B.

Applying the lemma again, there exists k such that U(k) agrees with g until n and gPU(k) ∈ P. For such k, U(k) agrees with g until n and g agrees with f until n, thus U(k) also agrees with f until n, and since (gP) ≠ B and gPU(k) ∈ P, we have (U(k) ∈ P) ≠ B. Therefore, U(k) satisfies the conditions of the parallel search step in the program p, namely: U(k) agrees with f until n and (U(k) ∈ P) ≠ B. This proves that the search in the second step always terminates. We fix k to be the value that it finds.

We observe that φp = U(k). Indeed, either the second step of p returns U(k)(x), or the third step returns f(x), but the latter case only happens for xn, and we know that U(k) agrees with f until n.

In particular, φp = U(k) is total. This makes the promise to P run on p fulfilled, therefore P returns φpP on p.

We have found a contradiction: one the one hand, the boolean φpP is the return value of P on p, which is B, and on the other hand, we have φp = U(k), and we know that (U(k) ∈ P) ≠ B.

Perspective from effective topology

For any finite unary function

\theta

on integers,let

C(\theta)

denote the 'frustum'of all partial-recursive functions that are defined, and agree with

\theta

,on

\theta

's domain.

Equip the set of all partial-recursive functions with the topology generated by thesefrusta as base. Note that for every frustum

C

, the index set

Ix(C)

is recursively enumerable. More generally it holds for every set

A

of partial-recursive functions:

Ix(A)

is recursively enumerable iff

A

is a recursively enumerable union of frusta.

Applications

The Kreisel-Lacombe-Shoenfield-Tseitin theorem has been applied to foundational problems in computational social choice (more broadly, algorithmic game theory). For instance, Kumabe and Mihara apply this result to an investigation of the Nakamura numbers for simple games in cooperative game theory and social choice theory.

Notes

[1] [2] [3] [4] [5] [6] [7] [8] [9] [10]

Notes and References

  1. Moschovakis . Yiannis N. . Kleene's amazing second recursion theorem . The Bulletin of Symbolic Logic . 16 . 2 . June 2010 .
  2. Royer . James S. . Semantics vs Syntax vs Computations: Machine Models for Type-2 Polynomial-Time Bounded Functionals . Journal of Computer and System Sciences . 54 . 3 . June 1997 . 424-436 . 10.1006/jcss.1997.1487 . free .
  3. Book: Rogers Jr. , Hartley . Hartley Rogers Jr. . Theory of Recursive Functions and Effective Computability . MIT Press . 0-262-68052-1 . 1987 .
  4. Book: Cutland , Nigel . Computability: an introduction to recursive function theory . Nigel Cutland . Cambridge University Press . 1980 .
    Theorem 7-2.16.
  5. Book: Odifreddi , Piergiorgio . Classical Recursion Theory . Piergiorgio Odifreddi . North Holland . 1989 .
  6. Book: Kreisel . Georg . Georg Kreisel . Lacombe . Daniel . Shoenfield . Joseph R. . Joseph R. Shoenfield . Constructivity in Mathematics . Partial recursive functionals and effective operations . 1959 . Heyting . Arend . Arend Heyting . Studies in Logic and the Foundations of Mathematics . North-Holland . Amsterdam . 290–297 .
  7. Kumabe . M. . Mihara . H. R. . Computability of simple games: A characterization and application to the core . Journal of Mathematical Economics . 44 . 348–366 . 2008 . 3–4 . 10.1016/j.jmateco.2007.05.012 . 0705.3227 . 8618118 .
  8. Kumabe . M. . Mihara . H. R. . The Nakamura numbers for computable simple games . Social Choice and Welfare . 31 . 4 . 621 . 2008 . 10.1007/s00355-008-0300-5 . 1107.0439 . 8106333 .
  9. Book: Longley . John . Normann . Dag . Higher-Order Computability . 2015 . Springer . 10.1007/978-3-662-47992-6 . 441 .
  10. Tseitin . Grigori . Grigori Tseitin . Algorithmic operators in constructive complete separable metric spaces . 1959 . Doklady Akademii Nauk . 128 . 49-52 .