-1
$\begingroup$

So the halting problem basically states that there cannot exist any finite length algorithm for automatically verifying if other finite length algorithms terminate.

But suppose I start listing out all the possible programs. I am allowed to list them as they form a countable set involving finite length permutations of a countable number of symbols. We can label each program $X_0$, $X_1$ ... where $X_n$ denotes the n'th program that is listed by some scheme of selecting and permuting symbols.

Obviously an algorithm cannot exist that is successfully able to verify if ALL of the programs halt or do not. But does there exist any program $X_i$ for which it is simply not possible to verify if it will halt or not?

My analysis of it so far:

Assume we discover a program X that isn't verifiable. In other words there is a proof that there does not exist any algorithm A to determine if X terminates or does not. Then simply running X cannot result in us finding out if it terminates.

Thus X does not terminate in any finite amount of time. Thus X doesn't halt. Therefore we have concluded that X is verifiable. Meaning there doesn't exist an undecidable program X for which there exists a proof that X cannot be verified by an Algorithm A in a finite amount of time.

This however DOES NOT Mean every program X either can be proven to halt or not. Rather it states the programs X that are undecidable themselves do not have a proof of this fact. Here is the catch, if there is a proof that a program X cannot be proven to be undecidable then it must be the case that X is decidable so if X is undecidable then even this type of a proof cannot exist.

We conclude that if X is undecidable, then there doesn't exist a proof of X is undecidable, nor a proof that there doesn't exist a proof of X being undecidable.

Here is another form of the question, if I arbitrarily continue this chain of analysis I believe I will always conclude that X doesn't exist. That is if $$\exists \text{Proof} (\nexists \text{Proof of} \left( \nexists \text{Proof of} \left( \nexists \text{Proof of} \left( ... \left(\text{Program X is undecidable} \right) \right) \right) \right) $$ Then,

X is decidable.

Whats a hint for beginning to prove this result. And if such a proof exists, what philosophical implications does that have?

|cite|improve this question
$\endgroup$
  • 4
    $\begingroup$ For any finite collection of halting instances, there is a machine that can decide that collection in linear time, since that collection can be seen as a regular language. Any yes instance of the halting problem has a finite proof that it indeed halts, namely its computation history. $\endgroup$ – Ryan Williams May 30 '15 at 4:32
  • $\begingroup$ Why so many downvotes? $\endgroup$ – frogeyedpeas May 30 '15 at 17:30
  • $\begingroup$ Your question and analysis are very confused and confusing. Of course for any finite sequence of inputs you can hardwire the correct answers into the program, so finite sets are recognizable. On the other hand, maybe by "verify" you mean prove in a given logical theory. Then it is true that for any consistent and powerful enough logical theory $T$ there is a Turing machine $M$ which does not halt but $T$ cannot prove that $M$ does not halt. $M$ simply enumerates proofs in $T$ and looks for a contradiction. Then the conclusion follows from Godel's 2nd incompleteness theorem. $\endgroup$ – Sasho Nikolov May 30 '15 at 18:33
  • $\begingroup$ What about en.wikipedia.org/wiki/Busy_Beaver_game#Notable_instances? $\endgroup$ – Solomon Ucko Nov 29 '19 at 22:59
1
$\begingroup$

One way to look at your question is the Busy Beaver Numbers.

What we will do is restrict a Turing Machine so that:

  1. The blank symbol is a $0$
  2. The tape alphabet is $\{0, 1\}$
  3. The input to our turing machine is always nothing (the tape is always initialized to only containing $0$'s)
  4. There are only $n$ internal states, for some $n \in \mathbb{N}$.

From here on out whenever I refer to Turing Machines I will be referring to Turing Machines restricted in this way, because this class of Turing Machines is just as powerful as the class of all Turing Machines, and is easier in this context to think about.

Note that given any $n=k$, the number of possible transition functions are finite. Thus if we really wanted to, we could manually iterate through every $k$-state turing machine, and figure out whether or not that Turing Machine halted. We could then run all of those halting ones and see which one runs the longest, and call this number $c_k$. Then we can solve the halting problem for any $k$-state Turing machine by simply running it and seeing if it runs for more than $c_k$ steps. If it does, then we know it doesn't halt.

We will call $\text{Busy Beaver} (n) = BB(n) = c_n$, where $c_n$ is a constant like ours computed above.

Note that if we could compute $BB(n)$ (or any function that grew faster than $BB(n)$), we could solve the halting problem. Thus $BB(n)$ is incomputable, in other words, it grows faster than any computable function.

However, for a fixed $k$, $BB(k)$ is computable, assuming you have a Turing Machine with much more than $k$ states, and a very long time to compute this.

So then if someone told you that they had a turing machine with $k$ states that you couldn't prove halted or not, you could simply compute $BB(k)$, then run their turing machine for $BB(k)+1$ steps, and then if it was still going you would know that it doesn't halt, otherwise you would know that it does halt. So then they are wrong and you can prove such a thing.

This means that the "Undecidable Single Program" you are searching for doesn't exist, sorry.

|cite|improve this answer
$\endgroup$
  • $\begingroup$ "and figure out whether or not that Turing Machine halted" How? $\endgroup$ – Solomon Ucko Oct 22 '19 at 22:50
  • $\begingroup$ While there isn't an algorithm for it (that's the halting problem), you can analyze turing machines by hand and eventually come to a solid conclusion for any given turing machine. It's like how looking at any piece of code you can (usually) figure out what it'll do and if it'll halt, but there isn't an algorithm for determing if any piece of code will halt for a given input or not. $\endgroup$ – Phylliida Oct 24 '19 at 1:12
  • $\begingroup$ Couldn't its computability be independent of the logic system (e.g. ZFC) that you're using? $\endgroup$ – Solomon Ucko Oct 24 '19 at 1:17
  • $\begingroup$ Yes, I suppose it could be, but it does have a yes or no answer (if you run it eventually it’ll stop or not), so there should be some logic system that should suffice. The practical way would be to run it for a crazy long amount of steps and see if it ever goes into cycles (of various kinds). It’s very non-trivial analysis to do, but is usually possible $\endgroup$ – Phylliida Nov 29 '19 at 22:45
  • $\begingroup$ What about en.wikipedia.org/wiki/Busy_Beaver_game#Notable_instances? $\endgroup$ – Solomon Ucko Nov 29 '19 at 22:59

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