1
$\begingroup$

Let $B$ be a recursive enumerable set and $B = W_n$, where $W_n = \{x \in \mathbb N \mid \Phi(x,n)\downarrow\}$ and $\Phi^{(n)}(x_1, \ldots, x_n, y)$ is the value of the function at the terminal snaphot.

There is a definition that leaves me really confused: $$n \in W_n \Leftrightarrow \Phi(n,n)\downarrow \Leftrightarrow \text{HALT}(n,n)$$

the thing is we know that $\text{HALT}$ is not computable, therefore is is undefined so how is it possible that it is equivalent to $\Phi(n,n)\downarrow$ which is actually a defined function? What am I missing here?

$\endgroup$
  • 1
    $\begingroup$ A function may be defined but not computable. $\endgroup$ – Andrej Bauer Sep 4 '13 at 12:06
2
$\begingroup$

The function HALT is perfectly defined, it's just not computable - there is no program that computes it. Similarly, $\Phi(n,n) \downarrow$ is not a condition that can be computed by a program. The situation is asymmetric: if $\Phi(n,n) \downarrow$ then a program can verify that, but in the other case you're at loss. This is because HALT is recursively enumerable (partially computable).

$\endgroup$
  • $\begingroup$ Basically the equivalence expresses the impossibility to check with an algorithm whether a program will eventually stop, which is definition for HALT. — I apologize in advance, here it comes the dumb question. — So if $\Phi(n,n) \downarrow$ is defined so is $\text{HALT}(n,n)$ and they are both true. But doesn't it also mean that $\Phi(n,n)$ computes $\text{HALT}(n,n)$? (I know the answer is no, but can't see the underlying reason.) $\endgroup$ – haunted85 Sep 4 '13 at 13:07
  • 1
    $\begingroup$ It's true that $\Phi(n,n)$ partially computes $\mathrm{HALT}(n,n)$. The problem is that to know whether $\mathrm{HALT}(n,n)$ is true or not, you need to wait for $\Phi(n,n)$ to (possibly) terminate, and you cannot foresee in advance how long you should be waiting. A program $P$ computes a predicate $Q$ if $P(x)$ always halts and returns the truth value of $Q(x)$. In contrast, $\Phi(n,n)$ doesn't always halt. $\endgroup$ – Yuval Filmus Sep 4 '13 at 13:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.