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 AA of all programs with a particular non-trivial semantic property. We know that there exists a program tAt \in A and a program fAf \notin A. Hence, if AA were decidable, there would be a function h(x)h(x) which yields ff if xAx \in A and tt if xAx \notin A. Per Kleene’s recursion theorem, given a function FF, a fixed point of FF is an index ee (in an admissable numbering φ\varphi) such that φe=φF(e)\varphi_e = \varphi_{F(e)}. Roger’s fixed point theorem states that if FF is a total computable function, then it has a fixed point. Now consider the program ee. If eAe \in A, then h(e)=fh(e) = f, and per the fixed point theorem φe=φF(e)=φf\varphi_e = \varphi_{F(e)} = \varphi_f. However, eAe \in A, but fAf \notin A - a contradiction. On the contrary, if eAe \notin A, then h(e)=th(e) = t, and per the fixed point theorem φe=φF(e)=φt\varphi_e = \varphi_{F(e)} = \varphi_t. However, eAe \notin A, but tAt \in A - a contradiction again. Therefore, AA 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 AA which contains the indices of programs with a certain property, then for any program φn\varphi_n, φnA\varphi_n \in A if and only if there exists a finite function fφnf \subseteq \varphi_n such that fAf \in A.

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

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