|
| 1 | +% Part: computability |
| 2 | +% Chapter: recursive-functions |
| 3 | +% Section: halting-problem |
| 4 | + |
| 5 | +\documentclass[../../include/open-logic-section]{subfiles} |
| 6 | + |
| 7 | +\begin{document} |
| 8 | + |
| 9 | +\olfileid{cmp}{rec}{hlt} |
| 10 | +\olsection{The Halting Problem} |
| 11 | + |
| 12 | +The \emph{halting problem} in general is the problem of deciding, |
| 13 | +given the specification~$e$ (e.g., program) of a computable function |
| 14 | +and a number~$n$, whether the computation of the function on input~$e$ |
| 15 | +halts, i.e., produces a result. Famously, Alan Turing proved that |
| 16 | +this problem itself cannot be solved by a computable function, i.e., |
| 17 | +the function |
| 18 | +\[ |
| 19 | +h(e, n) = |
| 20 | +\begin{cases} |
| 21 | +1 & \text{if computation $e$ halts on input $n$} |
| 22 | +0 & otherwise |
| 23 | +\end{cases} |
| 24 | +\] |
| 25 | +is not computable. |
| 26 | + |
| 27 | +In the context of partial recursive functions, the role of the |
| 28 | +specification of a program may be played by the index~$e$ given in |
| 29 | +Kleene's normal form theorem. If $f$ is a partial recursive function, |
| 30 | +any $e$~for which the equation in the normal form theorem holds, is an |
| 31 | +index of~$f$. Given a number~$e$, the normal form theorem states that |
| 32 | +\[ |
| 33 | +\cfind{e}(x) \simeq U(\mu s \; T(e, x, s)) |
| 34 | +\] |
| 35 | +is partial recursive, and for every partial recursive $f\colon \Nat |
| 36 | +\to \Nat$, there is an $e \in \Nat$ such that $\cfind{e}(x) \simeq |
| 37 | +f(x)$ for all~$x \in \Nat$. In fact, for each such $f$ there is not |
| 38 | +just one, but infinitely many such~$e$. The \emph{halting function}~$h$ |
| 39 | +is defined by |
| 40 | +\[ |
| 41 | +h(e, x) = |
| 42 | +\begin{cases} |
| 43 | +1 & \text{if $\cfind{e}(x) \defined$} |
| 44 | +0 & otherwise. |
| 45 | +\end{cases} |
| 46 | +\] |
| 47 | +Note that $h(e, x) = 0$ if $\cfind{e}(x) \undefined$, but also |
| 48 | +when~$e$ is not he index of a partial recursive function at all. |
| 49 | + |
| 50 | +\begin{thm} |
| 51 | +\ollabel{thm:halting-problem} |
| 52 | +$h$ is not partial recursive. |
| 53 | +\end{thm} |
| 54 | + |
| 55 | +\begin{proof} |
| 56 | +If $h$ |
| 57 | +were partial recursive, we could define |
| 58 | +\[ |
| 59 | +d(y) = |
| 60 | +\begin{cases} |
| 61 | +1 & \text{if $h(y, y) = 0$} |
| 62 | +\umin{x}{x \neq x} & \text{otherwise.} |
| 63 | +\end{cases} |
| 64 | +\] |
| 65 | +From this definition it follows that |
| 66 | +\begin{enumerate} |
| 67 | +\item $d(y) \defined$ iff $\cfind{y}(y) \undefined$ or $y$ is |
| 68 | + not the index of a partial recursive function. |
| 69 | +\item $d(y) \undefined$ iff $\cfind{y}(y) \defined$. |
| 70 | +\end{enumerate} |
| 71 | +If $h$ were partial recursive, then $d$ would be partial recursive as |
| 72 | +well. Thus, by the Kleene normal form theorem, it has an index |
| 73 | +$e_d$. Consider the value of $h(e_d, e_d)$. There are two |
| 74 | +possible cases, 0 and 1. |
| 75 | +\begin{enumerate} |
| 76 | +\item If $h(e_d, e_d) = 1$ then $\cfind{e_d}(e_d) \defined$. But |
| 77 | + $\cfind{e_d} = d$, and $d(e_d)$ is defined iff $h(e_d, e_d) = 0$. |
| 78 | + So $h(e_d, e_d) \neq 1$. |
| 79 | +\item If $h(e_d, e_d) = 0$ then either $e_d$ is not the index of a |
| 80 | + partial recursive function, or it is and $\cfind{e_d}(e_d) |
| 81 | + \undefined$. But again, $\cfind{e_d} = d$, and $d(e_d)$ is undefined |
| 82 | + iff $\cfind{e_d}(e_d) \defined$. |
| 83 | +\end{enumerate} |
| 84 | +The upshot is that $e_d$ cannot, after all, be the index of a partial |
| 85 | +recursive function. But if $h$ were partial recursive, $d$ would be |
| 86 | +too, and so our definition of $e_d$ as an index of it would be |
| 87 | +admissible. We must conclude that $h$ cannot be partial recursive. |
| 88 | +\end{proof} |
| 89 | + |
| 90 | +\end{document} |
| 91 | + |
| 92 | + |
0 commit comments