HiveBrain v1.2.0
Get Started
← Back to all entries
patternModerate

Constructive proof of decidability of finite Halting-problem-style set that does not use table lookup

Submitted by: @import:stackexchange-cs··
0
Viewed 0 times
problemfinitetableconstructivehaltingstylethatdecidabilitydoeslookup

Problem

I tried to prove that the following language is recursive: for $\Sigma=\{0,1\}$, $k$ a positive integer:
$$
L_k= H_{\mathrm{TM},\varepsilon}\cap \Sigma^k
$$
where $H_{\mathrm{TM},\varepsilon}=\{\langle M\rangle\mid M \text{ is a TM that halts on an empty input}\}$

It is easy to prove because $L_k$ is finite, but I didn't notice this and tried to prove it by finding a decider TM for it.
I thought that since the encoding of the TM is of length $k$ then it can't have more than $2^k$ states, and by running it on epsilon for $2^k$ steps, if it halts by then than accept otherwise reject.
I was told that it's incorrect - is it a wrong solution. How can I prove this using this method (and not the way I mentioned about $L_k$ being finite)?

Solution

There is no general way to find a decider TM for $L_k$

You are correct that $L_k$ is recursive because, being a subset of the
finite set $\Sigma^k$, it is also finite.

You would like to rather find a decider TM for $L_k$, and you suggest
some techniques. Without even going into the details of these
techniques and why they do not work, you do not stand any chance of
ever succeeding.

The first thing you should notice is that the finiteness argument
tells you that there exists a decider TM $M_k$ for the language $L_k$,
but it does not tell you what this TM is. It is an example of a
non-constructive proof: you prove that a decider exists, but you
cannot tell which it is.

Now, suppose that, given $k$, you have a procedure $\mathcal P(k)$ to
find such a decider $M_k$ for the language $L_k$ (rather than just
prove it exist). Then, given any Turing machine $M$, then there is an
integer $k'$ such that $|\langle M\rangle|=k'$, so that $\langle
M\rangle\in \Sigma^{k'}$. Then you can use the procedure $\mathcal P$
to find a decider TM $M_{k'}$ that can determine whether $\langle
M\rangle\in L_{k'}$. So you have a way to decide whether the TM $M$
halts on empty input. And this works for any TM $M$. However, this is
not possible, because it is undecidable whether a given TM $M$ halts
on empty input.

So the procedure $\mathcal P$ cannot exist.

Since you are looking for a general way to find the decider TM
$M_{k'}$, you cannot succeed because that method would be precisely a
procedure such as $\mathcal P$.

Note that this proof could still leave the (very remote) possibility
of finding a decider for some specific values of $k$, but you would
have to identify precisely the concerned values, and the method would
not work for all values of $k$. I am not advising you to try.

Context

StackExchange Computer Science Q#44458, answer score: 10

Revisions (0)

No revisions yet.