iczelia :: Rice and Rice-Shapiro theorems.

Programs have semantic and syntactic properties. For example, a syntactic property of a certain program could be that it contains a loop, while a semantic property could be that it halts. A trivial property is satisfied by all programs or none. For example, the property "halts" is non-trivial, as it is satisfied by some programs and not by others. The property "domain has zero or more elements" is trivial, as it is satisfied by all programs. According to Rice's theorem, non-trivial semantic properties of a program are undecidable. The theorem is named after Henry Gordon Rice, who proved it in his doctoral dissertation of 1951 at Syracuse University.

Suppose that we have a set $A$ of all programs with a particular non-trivial semantic property. We know that there exists a program $t \in A$ and a program $f \notin A$ . Hence, if $A$ were decidable, there would be a function $h(x)$ which yields $f$ if $x \in A$ and $t$ if $x \notin A$ . Per Kleene's recursion theorem, given a function $F$ , a fixed point of $F$ is an index $e$ (in an admissable numbering $\varphi$ ) such that $\varphi_e = \varphi_{F(e)}$ . Roger's fixed point theorem states that if $F$ is a total computable function, then it has a fixed point. Now consider the program $e$ . If $e \in A$ , then $h(e) = f$ , and per the fixed point theorem $\varphi_e = \varphi_{F(e)} = \varphi_f$ . However, $e \in A$ , but $f \notin A$ - a contradiction. On the contrary, if $e \notin A$ , then $h(e) = t$ , and per the fixed point theorem $\varphi_e = \varphi_{F(e)} = \varphi_t$ . However, $e \notin A$ , but $t \in A$ - a contradiction again. Therefore, $A$ is undecidable.

A more general version of this claim is the Rice-Shapiro theorem. While Rice's theorem proves that all non-trivial semantic property is undecidable (i.e. there is no algorithm that can decide whether a program has a certain non-trivial semantic property and halt), the Rice-Shapiro demonstrates that finitary properties are recursively enumerable (i.e. there is an algorithm which decides if a program has a property which depends on a finite number of inputs by either accepting or diverging). Formally speaking, the The Rice-Shapiro theorem states that given a recursively enumerable set $A$ which contains the indices of programs with a certain property, then for any program $\varphi_n$ , $\varphi_n \in A$ if and only if there exists a finite function $f \subseteq \varphi_n$ such that $f \in A$ .

A more elementary variant of this theorem states that if the set $A$ is recursively enumerable, then for every $g \in A$ , there is an $j \in I$ with $\text{dom}(j) \subseteq \text{dom}(g)$ and $\text{dom}(j)$ is finite. The proof of this theorem is more elementary: Suppose there is a function $k(x)$ such that $k(x)=1$ if $x \in A$ and diverges otherwise. Then, by applying the recursion theorem, there is a program $\varphi_j(n)=f(j,n)$ such that $f$ computes $g(n)$ if $k(j)$ takes more than $n$ steps to halt. Then, if $\varphi_j \notin A$ , then then $k(j)$ diverges and $f(j,n)=g(n)$ for all $n$ , but $g \in A$ - contradiction. On the other hand, if $\varphi_j \in A$ , then $k(j)=1$ and $f(j,n)$ is defined for finitely many $n$ , hence $\text{dom}(j)$ is finite. If $\varphi_j(n)$ is defined, then $\varphi_j(n) = g(n)$ , and $\text{dom}(\varphi_j)$ is a finite subset of $\text{dom}(g)$ .

A corollary of this result is that if $\Omega$ is an always-diverging program, then $\Omega \in A$ implies that $\bar H \le A$ , and further if $\Omega \notin A$ , then $H \le A$ , where $H$ is the set of tuples of programs and inputs on which they halt.