6
$\begingroup$

Most proofs of Rice theorem seem to be based on the undecidability of the halting problem. They are "reduction-based".

Are there "direct" elementary proofs, perhaps based on diagonalization?

I think that the answer is "YES there are".

However most textbooks I know (such as [Odifreddi, Moret, Jones, Phillips] present reduction-based proofs.

$\endgroup$
1
  • 6
    $\begingroup$ Well, the undecidability of the halting problem is proved via diagonalization, so unwinding the standard proof of Rice's theorem will give you a purely diagonalization-based proof. Presumably, though, this isn't what you mean? $\endgroup$ Commented Jan 22, 2014 at 18:35

2 Answers 2

7
$\begingroup$

Here is a proof based on the recursion theorem, rather than a reduction of an undecidable problem.

Rice's Theorem. Suppose that $P$ is any set of computable functions, which is not empty and not all computable functions. Then the set $\{ e\mid \varphi_e\in P\}$ is not decidable, where $\varphi_e$ is the function computed by program $e$.

In other words, there is no general procedure to determine from a program whether the function it computes has property $P$ or not.

Proof. Suppose that the set were decidable. Fix a computable function $f$ that is in $P$, and another computable function $g$ that is not in $P$. Now, for any program $e$, let $h(e)$ be the program that on input $n$ first determines whether $\varphi_e\in P$; if so, it outputs $g(n)$, and otherwise $f(n)$. So $\varphi_{h(e)}$ is either $g$ or $f$, depending on whether $\varphi_e\in P$ or not, respectively (but note that we are using the opposite function). In particular, we'll have $$\varphi_e\in P\quad\iff\quad\varphi_{h(e)}\notin P.$$ Meanwhile, by the recursion theorem, there is a program $e$ such that $\varphi_e=\varphi_{h(e)}$, which now gives an immediate contradiction, since $\varphi_e$ and $\varphi_{h(e)}$ are supposed to be opposite with respect to $P$. QED

$\endgroup$
4
$\begingroup$

Here is a proof in a more 'constructive' form that can be directly applied to any real-world programming language. Just to make clear, a property of programs must be a predicate that only depends on the halting and output behaviour, in other words two equivalent programs will have exactly the same properties. I will use $X \equiv Y$ to denote that two programs are equivalent, and so $P$ is a property iff $P$ is a predicate and $P(X)=P(Y)$ for any programs $X \equiv Y$.

For any property $P$ of programs such that $P(T)$ and $\neg P(F)$ for some programs $T$,$F$:

  If $P$ is decidable:

    Let $D$ be a program that decides $P$

    Let $M$ be the following program on input $x$:

      Create $N$ to be the following program on input $y$:

        If $x$ is an invalid program: Return "" [may be unnecessary in some languages]

        Return $x(x)(y)$ [using closures or some interpreter written in the language itself]

      If D(N): Return F

      Return T

    Let $R$ be the program that $M(M)$ creates in the variable $N$

    Clearly $R \equiv M(M)$

    Also $M(M)$ halts because $D$ halts on all inputs

    Thus $M(M) \equiv T \vee M(M) \equiv F$

    $P(M(M)) \Leftrightarrow P(R) \Leftrightarrow D(R) = True \Leftrightarrow M(M) \equiv F \Leftrightarrow \neg P(M(M))$

    Contradiction

  Therefore $P$ is not decidable

$\endgroup$
3
  • $\begingroup$ Isn't this what you would get if you "unfold" the reduction to the halt problem? (as suggested by Noah's comment) $\endgroup$
    – Daniel
    Commented Feb 1, 2020 at 18:55
  • $\begingroup$ @Daniel: Well, in the end every proof of Rice's theorem must pass through some kind of diagonalization. If you look at Joel's proof, the 'diagonalization' is right there in the use of the recursion theorem. I posted my version some time afterward, but it too uses 'diagonalization' right in the "$x(x)$" part. The main advantage of my version is that it corresponds directly to an explicit program I can write (in say Javascript) to defeat any claimed decider. I am not too sure what Noah's comment means, because there are many proofs of Rice's theorem that use the halting problem undecidability. $\endgroup$
    – user21820
    Commented Feb 2, 2020 at 3:09
  • $\begingroup$ In particular, one proof that I have seen in many places (for example see here) is more complicated than mine, so unfolding it will give a different longer proof. $\endgroup$
    – user21820
    Commented Feb 2, 2020 at 3:12

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .