# Accelerating semidecision of halting problem

There is a naive semidecision algorithm for the halting problem: simply simulate the program and see if it halts. Is there an algorithm that is asymptotically faster? More precisely, suppose the naive program halts in $$f(M)$$ steps, given a halting input $$M$$, is there a semidecision algorithm that halts in $$o(f(M))$$ steps, as the size of $$M$$ tends to infinity?

First, it is trivially possible to construct a program that detects an infinite family of halting machines faster: for example, we test if the source code is $$\texttt{for i in range(1,}n\texttt{): print("a")}$$, where $$n$$ is a numeral. Then we immediately say this program halts. So we are requiring a strict speedup for all families of programs eventually.

Without specifying the naive algorithm, we can still expect cases where the "naive" algorithm is slower. For instance if the naive algorithm waits for $$t^2$$ steps on purpose after using $$t$$ steps to determine that the input halts. But I would be very surprised if this still happens when we just construct an obvious algorithm in each specific setup without maliciously slowing it down. For example, if we use some less efficient parsing algorithm, then it at most introduces some exponential slowdown with respect to the size of $$M$$, which will be dwarfed by $$f(M)$$. With this in mind, I wouldn't actually try to write down the naive algorithm, but if I'm wrong then feel free to specify the naive algorithm.

My first instinct is that, we can suppose for contradiction that there is a faster algorithm that halts in $$g(M)$$ steps, where $$g(M) < f(M)$$ when the size of $$M$$ is greater than $$N$$. Here $$N$$ is a known constant, so we might somehow exploit this to decide the halting problem, similar to how we prove that $$BB$$ is non-computable. But this doesn't seem to work out in the end. We might also try to iterate the faster algorithm on itself to somehow semidecide faster and faster. This also doesn't seem to lead to contradictions.

• While you can detect an infinite family of halting machines faster than just with simulating them, I doubt it significantly changes even the average time complexity of the algorithm. The machines that can be detected this way (primitive recursive machines in general) run for time much much less than $BB(n)$. Commented Jul 19 at 15:44
• Suppose we could speed up the decision asymptotically for every (halting) program. Now do the usual trick in this space: take your sped-up decision process, and feed it to itself. You get another asymptotic speedup for free, and you can loop this process indefinitely to get an arbitrary speedup. Sounds unlikely to me (though admittedly there is a lot of formalization work before I'd consider this a "proof"). Commented Jul 21 at 2:13
• @DanielWagner: Re: "you can loop this process indefinitely to get an arbitrary speedup": Not necessarily. Consider a sequence like $n^{2.1}, n^{2.01}, n^{2.001}, n^{2.0001}, ...$; each iteration gives you an asymptotic speedup, but you'll never reach $O(n^2)$. Commented Jul 21 at 4:07

For a trivial counterexample . . .

Consider a straightforward program that takes a string of 0s and 1s, and halts if and only if it finds an odd number of 1s:

should_halt := false
for c in input:
if c = 1:
should_halt := NOT(should_halt)
if should_halt:
halt
else:
while true:
continue


The naive algorithm, which simply simulates this program, will halt in $$Θ(|M|)$$ time if and if only if $$M$$ contains an odd number of 1s.

Any semidecider algorithm will require at least $$Θ(|M|)$$ time, because changing any character in $$M$$ will change whether the program halts, so the algorithm has to read all of them.

So it's impossible to do asymptotically faster than the naive algorithm for this program.

There is a family of explicit programs for which acceleration cannot exist, as proven by the time hierarchy theorem.

Let's unpack the proof of the time hierarchy theorem. Let $$T(n)$$ be any time-constructible function. Consider the language $$H_T = \{ (M, x) : M(x) \text{ accepts in } T(|x|) \text{ steps} \}.$$ This language can be decided by a program $$U$$ in $$O(T(n) \log T(n))$$ time. More precisely, the exact time complexity depends on the computational model, but the $$O(T(n) \log T(n))$$ simulation holds for a multi-tape Turing machine, which we use as an example here. It can be shown that $$H_T$$ cannot be decided in $$o(T(n))$$ time by diagonalization.

Now, consider two programs $$U_0$$ and $$U_1$$:

• $$U_0(x)$$ runs the program $$U(x)$$, and halts if $$U$$ rejects; otherwise, it enters an infinite loop.
• $$U_1(x)$$ runs the program $$U(x)$$, and halts if $$U$$ accepts; otherwise, it enters an infinite loop.

Suppose $$U_0$$ and $$U_1$$ both have accelerated semi-decision algorithms $$U_0'$$ and $$U_1'$$ that run in $$o(T(n))$$ time. We can then construct a program $$U'$$ that does the following:

• Run $$U_0'$$ and $$U_1'$$ simultaneously, and decide $$H_T$$ based on which program halts first.

Thus, $$U'$$ decides $$H_T$$ in $$o(T(n))$$ time, which contradicts the time hierarchy theorem.

This shows that in the multi-tape Turing machine model, there are semi-decision programs halts in $$o(T(n)\log T(n))$$ steps, but it is impossible to accelerate them to $$o(T(n))$$ steps. Similar analogues holds for other computation models.

• If I understand correctly, this argument shows that you can't guarantee a speedup from $\Theta(T(n) \log T(n))$ all the way down to $o(T(n))$; but it leaves open the possibility that you can guarantee a smaller speedup to some $o(T(n) \log T(n))$ (e.g., to $\Theta(T(n) \log \log T(n))$. So it sets an upper bound on how much speedup you can guarantee, but it doesn't directly answer the OP's question of whether you can guarantee at least some asymptotic speedup. (Nonetheless, this is a fantastic first post. Welcome to the site!) Commented Jul 21 at 4:01

There is a whole body of research on how to "quickly" semi-decide whether programs halt; in general, they fall into the area of techniques for proving liveness properties, in formal methods. Try searching for "termination analysis" or "temporal logic liveness proofs" for instance.

In particular, the functions $$f$$ and $$g$$ you mention sound like ranking functions. Ranking functions are maps from program state to some well-founded order such that (1) they monotonically decrease as program progresses and (2) the program terminates when the least element in the order is reached. What you are asking is, in essence, whether one can automatically find the best ranking function (i.e. one that decreases the fastest, in a sense) of a program.

The subject of how to find good ranking functions is altogether a research topic on its own, and a difficult one. It is very much an active area of research.

There are known facts about finding ranking functions of certain forms for programs in certain forms (usually numerical programs with restricted syntactic structure). E.g. for linear loops, it is known that one can accelerate their computations by matrix expontentiation, and this is in general true for programs expressed in logics whose transitive closure is computable. So for these classes of programs one can do better in proving termination (and indeed, other properties) than simply simulating them.

Some references: