Rice–Shapiro theorem

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 be a set of partial computable functions such that the index set of is semi-decidable. Then for any partial computable function, it holds that contains if and only if contains a finite subfunction of .
Kreisel–Lacombe–Shoenfield–Tseitin theorem. Let be a set of total computable functions such that the index set of is decidable with a promise that the input is the index of a total computable function. We say that two total functions, "agree until " if holds for all. Then for any total computable function, there exists such that for all total computable function which agrees with until, we have.

Examples

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

Terminates on all inputs ;
Terminates on finitely many inputs;
Is equivalent to a fixed other program.

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

Always returns an even number;
Is equivalent to a fixed other program that always terminates;
Always returns the same value.

Discussion

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

Rice's theorem applies to decidable sets of partial computable functions, concluding that they must be trivial.
The Rice-Shapiro theorem applies to semi-decidable sets of partial computable functions, concluding that they can only recognize elements based on a finite number of values.
The Kreisel–Lacombe–Shoenfield–Tseitin theorem applies to decidable sets of total computable functions, with a conclusion similar to the Rice-Shapiro theorem.

It is natural to wonder what can be said about semi-decidable sets of total computable functions. Perhaps surprisingly, these need not verify the conclusion of the Rice-Shapiro and Kreisel–Lacombe–Shoenfield–Tseitin theorems. The following counterexample is due to Richard M. Friedberg.
Let be the set of total computable functions such that is not the constant zero function and, defining to be the maximum index such that is zero, there exists a program of code such that is defined and equal to for each. Let be the set with the constant zero function added.
On the one hand, contains the constant zero function by definition, yet there is no such that if a total computable agrees with the constant zero function until then. Indeed, given, we can define a total function by setting to some value larger than every for such that is defined, and for. The function is zero except on the value, thus computable, it agrees with the zero function up to, but it does not belong to by construction.
On the other hand, given a program and a promise that is total, it is possible to semi-decide whether by dovetailing, running one task to semi-decide, which can clearly be done, and another task to semi-decide whether for all. This is correct because the zero function is detected by the second task, and conversely, if the second task returns true, then either is zero, or is only zero up to an index, which must satisfy, which by definition of implies that.

Proof of the Rice-Shapiro theorem

Let be a set of partial computable functions with semi-decidable index set. We prove the two implications separately.

Upward closedness

We first prove that if is a finite subfunction of and then. The hypothesis that is finite is in fact of no use.
The proof uses a diagonal argument typical of theorems in computability. We build a program as follows. This program takes an input. Using a standard dovetailing technique, runs two tasks in parallel.

The first task executes a semi-algorithm that semi-decides on itself. If this eventually returns true, then this first task continues by executing a semi-algorithm that semi-computes on, and if that terminates, then the task makes as a whole return.
The second task runs a semi-algorithm that semi-computes on. If this returns true, then the task makes as a whole return.

If, the first task can never finish, therefore the result of is entirely determined by the second task, thus is simply, a contradiction. This shows that.
Thus, both tasks are relevant; however, because is a subfunction of and the second task returns when is defined, while the first task returns when defined, the program in fact computes, i.e.,, and therefore.

Extracting a finite subfunction

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

Run computation steps of a semi-algorithm that semi-decides, with itself as input. If this semi-algorithm terminates and returns true, then loop indefinitely.
Otherwise, semi-compute on, and if this terminates, return the result.

Suppose that. This implies that the semi-algorithm for semi-deciding used in the first step never returns true. Then, computes, and this contradicts the assumption. Thus, we must have, and the algorithm for semi-deciding returns true on after a certain number of steps. The partial function can only be defined on inputs such that, and it returns on such inputs, so it is a finite subfunction of that belongs to.

Proof of the Kreisel–Lacombe–Shoenfield–Tseitin theorem

Preliminaries

A total function is said to be ultimately zero if it always takes the value zero except for a finite number of points, i.e., there exists such that for all. Note that such a function is always computable.
We fix a computable enumeration of all total functions which are ultimately zero, that is, is such that:

For all, the function is ultimately zero;
For all total function which is ultimately zero, there exists such that ;
The function is itself total computable.

We can build by standard techniques.

Approximating by ultimately zero functions

Let be as in the statement of the theorem: a set of total computable functions such that there is an algorithm which, given an index and a promise that is total, decides whether.
We first prove a lemma: For all total computable function, and for all integer, there exists an ultimately zero function such that agrees with until, and.
To prove this lemma, fix a total computable function and an integer, and let be the boolean. Build a program which takes input and takes these steps:

If then return ;
Otherwise, run computation steps of the algorithm that decides on, and if this returns, then return zero;
Otherwise, return.

Clearly, always terminates, i.e., is total. Therefore, the promise to run on is fulfilled.
Suppose for contradiction that one of and belongs to and the other does not, i.e.,. Then we see that computes, since does not return on no matter the amount of steps. Thus, we have, contradicting the fact that one of and belongs to and the other does not. This argument proves that. Then, the second step makes return zero for sufficiently large, thus is ultimately zero; and by construction, agrees with until. Therefore, we can take and the lemma is proved.

Main proof

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

Run computation steps of the algorithm that decides on.
If this returns in a certain number of steps, then search in parallel for such that agrees with until and. As soon as such a is found, return.
Otherwise, return.

We first prove that returns on. Suppose by contradiction that this is not the case. Then actually computes. In particular, is total, so the promise to when run on is fulfilled, and returns the boolean, which is, i.e.,, contradicting the assumption.
Let be the number of steps that takes to return on. We claim that satisfies the conclusion of the theorem: for all total computable function which agrees with until, it holds that. Assume for contradiction that there exists total computable which agrees with until and such that.
Applying the lemma again, there exists such that agrees with until and. Since both and agree with until, also agrees with until, and since and, we have. Therefore, satisfies the conditions of the parallel search step in the program, namely: agrees with until and. This proves that the search in the second step always terminates. We fix to be the value that it finds.
We observe that. Indeed, either the second step of returns, or the third step returns, but the latter case only happens for, and we know that agrees with until.
In particular, is total. This makes the promise to run on fulfilled, therefore returns on.
We have found a contradiction: one the one hand, the boolean is the return value of on, which is, and on the other hand, we have, and we know that.

Perspective from effective topology

For any finite unary function on integers,
let denote the 'frustum'
of all partial-recursive functions that are defined, and agree with,
on 's domain.
Equip the set of all partial-recursive functions with the topology generated by these
frusta as base. Note that for every frustum, the index set is
recursively enumerable. More generally it holds for every set
of partial-recursive functions:
is recursively enumerable iff
is a recursively enumerable union of frusta.

Applications

The Kreisel–Lacombe–Shoenfield–Tseitin theorem theorem has been applied to foundational problems in computational social choice. 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.