# Can We Decide Whether Small Computer Programs Halt?

The undecidability of the halting problem states that there is no general procedure for deciding whether an arbitrary sufficiently complex computer program will halt or not.

Are there some large $n$ and interesting computer languages (say C++, Scheme) for which we have a constructive halting algorithms for programs of length up to $n$? Note that for any fixed bound, there is some finite lists of zero's and one's that stores whether all the programs less than that bound halt or not, so non-constructively for any $n$ there is always a decision procedure for the bounded problem. But I would like to know whether we have some $n$ for which we can constructively write a decision procedure for programs of length less than that bound. By stipulating large $n$, I'd like to avoid $n$ and languages which are trivial in some sense, for instance, decision procedure for languages where the first number of programs all halt and we can easily see that they halt.

Note that the usual proof of the undecidability of the halting program prima facia does not apply, since the decision procedure for programs bounded by $n$ might have length much larger than $n$, so our decision procedure need not correctly apply to our diagonlization program.

What kind of work has been done on this? Are there any good references out there? Thank you!

• You are only talking about programs with no input, is that correct? The situation changes if the length of the input also needs to be considered. Dec 29 '13 at 23:32
• Yes, I have in mind programs with no input. Dec 30 '13 at 4:51
• What do you exactly mean by "constructive"? Dec 31 '13 at 7:53
• Something beyond saying an algorithm exists because it is a finite problem. For instance a specification of a decision algorithm together with a proof that procedure works. Dec 31 '13 at 22:50
• Just to clarify, definitely not a uniform way to get from $n$ to a program that decides the halting problem bounded to size less than $n$ which would impossible. I'd just like to know the real answer to which small programs halt, or at least try to get a grip on what it would take to build such a decision procedure. Dec 31 '13 at 23:05

As you noticed in your question, for any particular value of $n$, there is a constructive algorithm that solves the halting problem for instances of size at most $n$. Since for a particular value of $n$, there are only finitely many instances, one may simply hard-code the finitely many answers into the program itself. So in this sense, yes, for any particular $n$, we have a constructive solution of the halting problem for instances of size at most $n$.

Meanwhile, there can be no uniform method of describing these algorithms, since from any uniform method of describing the programs, we could extract a computable solution of the halting problem. If there were a uniform solution, then given any instance of the halting problem, we could produce the program that is suitable for that instance, and then run it, thereby solving the halting problem. So there can be no general method to describe these particular instances. This issue of uniformity was also an issue in some other MO questions, particularly Gordon Royle's question Can a problem be simultaneously polynomial time and undecidable?.

But worse, what I claim is that for any particular background theory, such as PA or ETCS or ZFC or ZFC plus large cardinals, there is a particular value of $n$ (that we can compute from the theory), such that there is a program of size at most $n$ such that the theory simply does not settle the question of whether it halts or not. This $n$ is simply the size of the program that searches for a proof of a contradiction in the background theory, halting only when one is found. We can easily design such a program for any particular theory, such as ZFC or whatever (c.e.) theory you like (as long as it was consistent), and experts could compute the particular value of $n$, although this particular value would depend on the details of the computability formalism. For this $n$, there can be no constructive algorithm that you can prove in your background theory is a computable solution of the halting problem, since if such an algorithm truly and provably solved the halting problem for the program that searched for a contradiction, then it would also settle the consistency question of the background theory, which is impossible.

So the conclusion is that there is a comparatively small value of $n$ for which no specific constructive algorithm can provably and truly settle the halting problem for instances of size at most $n$. This can be taken as a negative answer to your question, since there can be no truly large values of $n$ for which we can provably settle the halting problem by a specific algorithm.

• Furthermore, we can compute the bad value of $n$ from any specific representation of the background theory---it is just the size of the program searching for a contradiction in the theory---so the issue isn't just that there is a non-uniformity issue, but rather, there is a general phenomenon that theories can in principal not prove that specific algorithms solve large instances of the halting problem. We can uniformly go from a code computing the background theory to a number $n$ for which that theory will not correctly prove any specific solution for the size-$n$ halting problem. Dec 30 '13 at 2:19
• @Michael, for any particular $n$, the truth table is essentially a finite list of $0$s and $1$s, and all such tables can be computably constructed. (We don't have to know which sequence, to prove that there is a computable way to do it.) The number $n$ is not a part of the input, and this issue is precisely the issue of uniformity; there can be no uniform algorithm, so in general, you are right, we have no general algorithm to produce the table as a function of $n$. The issue of uniformity also comes up at mathoverflow.net/questions/48014/48031#48031. Dec 30 '13 at 13:48
• @user18447, I am saying (along with the OP) that for any $n$, the answer to the halting problem for instances of size at most $n$ is a finite pattern of yes/no responses, and any such pattern is computable, by hard-coding it into the program. This is a pure-existence proof that the halting problem of size $n$ has a constructive solution, for every particular $n$. But in the second part of my answer, I am saying that there is a small value of $n$ where the problem is more intractable than the Collatz conjecture type objection, where we cannot even in principle know the answer from our axioms. Dec 30 '13 at 14:00
• @user18447, but actually, it isn't clear to me how one would use even the full halting problem solution to come to know the Collatz conjecture, since that is a $\Pi^0_2$ assertion: every initial $n$ leads eventually to $1$. How would you deduce the answer to this from specific knowledge about whether some particular programs halt? (If it is false, you can learn this from a specific program failing to halt, but suppose it were true---how would you deduce this from knowing that a particular program halts or not?) Dec 30 '13 at 14:08
• From the comments above I feel there might be a confusion about what is a "constructive algorithm", I don't really know what the OP means by putting "constructive" in front of "algorithm", I guess a typical interpretation would be the code of the algorithm for $Halt_n$ is uniformly computable from $n$. But then the OP goes on to say that "for some $n$" that contradicts that interpretation. Dec 31 '13 at 7:51

An algorithm solving the halting problem for relatively small $n$ might not be ruled out by the diagonal argument, but it would be able to settle open problems in number theory (as The Masked Avenger also noted).

We don't know whether there are any Fermat primes beyond $2^{2^4}+1$. Consider a program based on

for(arbitrary_precision_int i = 5; ; i++)
if(isPrime(fermat(i)))
return;


If you can tell whether this halts, you can settle whether there are any other Fermat primes.

• I think we could have "return i" as part of the program, at the expense of adding 2 to n. Might as well get something indicative for those cycles. Dec 29 '13 at 21:18
• @The Masked Avenger: An algorithm for solving the halting problem for short programs does not necessarily run the program, so even if the program returns useful information, the algorithm might only say that it halts. Dec 29 '13 at 21:25
• If we had that program, we might be able to upgrade to a version that says when it halts, or with which output. (Or derive a better upper bound for n). Dec 29 '13 at 21:30

You're right that such a project is possible. Calude et al. (http://www.emis.de/journals/EM/expmath/volumes/11/11.3/Calude361_370.pdf) have some results in this direction.

• This looks very interesting, thanks! Dec 29 '13 at 21:08

On the flip side, one can write a program that does the Collatz sequence or walks through an enumeration of natural number vectors to see if it has a solution to some Diophantine equation whose solubility status is unknown. I thus expect small upper bounds on the length of n.

• In particular, I expect length of n is at most 7, so n is less than 128. Dec 29 '13 at 21:07
• 7, how do you get such a small value? Dec 30 '13 at 2:20
• Using macros, obfuscation, and guessing. Even if I am wrong, I would be surprised if the length of n were much larger than 9 (meaning n is larger than 511). Dec 30 '13 at 2:54
• I wouldn't be surprised if $n$ were smaller than $128$. However, it's not clear to me how to encode the Collatz conjecture as whether a program halts. Dec 30 '13 at 16:09
• If the Collatz conjecture is true, how could you come to know this from knowing whether a particular small program halts or not? Dec 30 '13 at 16:12

There's Coq, which has the property of being "Strongly Normalizing". Any program in Coq that type checks (i.e. that is a legal Coq program) is guaranteed to halt. Other languages have this property, such as the simply typed lambda calculus, but don't allow you to do much of interest. Coq features something called "dependent types", which enable functions to be written that can operate on arbitrarily large data structures, yet are guaranteed to halt. That's something the "simply typed lambda calculus" can't do for example.

Coq is a realization of something called the "Calculus of Constructions", which sets a top a lattice of formal systems called the "lambda cube". Apparently there are also some links between it and Algebraic Topology, although I do not begin to attempt to pretend to understand either topology or dependent types.

However, if you are looking for mathematical models of languages that are guaranteed to halt, Coq is probably a good place to start.

Also, this is only tangentially related to your question, but I highly recommend the book "Principles of Program Analysis". It shows some interesting things you can do with Lattices and Fixed points for extracting useful information from programs that don't necessarily halt.

The shift function numbers (http://en.wikipedia.org/wiki/Busy_beaver#Max_shifts_function) provides a way to do this when programs are represented as binary TMs. They are in general uncomputable (seen by reduction to general halting problem). However, for $n$ where the value of $SHIFT(n)$ is known ($n=1$, ... , $n=4$ are known I think), one can run any $n$ state TM for $SHIFT(n)$ time steps. If it hasn't halted by then, it never will.

It is known that there exists a universal 17 state binary TM and from this one can conclude that $SHIFT(17)$ must be uncomputable. The boundary of which "partial" halting problems can be solved is thus somewhere unknown between 4 and 17.

The Collatz conjecture was mentioned somewhere. Interestingly, the Collatz conjecture would be settled if $SHIFT(6,3)$ were known (where the 3 indicates the number of tape alphabet symbols).

• What does it mean to say that shift(17) is uncomputable? It is a specific number, and every particular number is computable. Do you mean to say that the particular value of shift(17) is independent of PA or some other theory? Dec 30 '13 at 22:07
• I mean that there is no algorithm (TM) which provably halts with one on the tape when run with an encoding of $n$ initially on the tape if and only if $SHIFT(17) = n$. Dec 30 '13 at 22:32
• I think what I getting at will be better explained in the links posted in the answer below: mathoverflow.net/a/153186/41654. Especially the last of the three links. Dec 30 '13 at 22:37

If instead of placing a bound on the program size, you place a bound on the size of memory it uses as $n$ bits, one can enumerate all possible states the program enters into using $2^{n}$ bits of memory. You can then simulate the program and track which states it enters. If it ever enters a state which it has previously entered, it does not halt. As there are only a finite number of possible states, you are guaranteed that either this condition occurs or the program halts in a finite number of steps.

While requiring $2^{n}$ bits of memory is quite steep for large values of $n$ there are useful classes of problems that can be solved using programs with very small quantities of memory.

• This doesn't answer the question but it does answer this one: mathoverflow.net/questions/143191 Dec 30 '13 at 15:53
• Yes, but as it is a very closely-related question it seems worth pointing it out here. Jan 4 '14 at 13:59

Let me start by saying that your question is definitely not a research-level question --- usually similar questions are asked by first/second year undergraduate students in computer science.

However, taking into account the popularity of your question, let me give two remarks.

A) "All partially recursive problems are recursive". Here is a "proof". Let me fix a partially recursive problem that is hard in the class of partially recursive functions --- for example, validity in First-Order Logic (the argument is exactly the same for any partially recursive or corecursive problem). There is an obvious partial algorithm $A$ that solves the problem --- given a formula $\phi$ it explores the derivation tree for $\phi$ in breadth-first order in a (sound and complete) proof system for FOL. Let us assume that $\phi$ is valid. By completeness of the system, for every valid formula $\phi$, there exists the shortest proof $s(\phi)$ of $\phi$ in our system. Let us denote by $l(\phi)$ the length of the proof $s(\phi)$.

The trick is to modify algorithm $A$ by introducing a counter that counts the length of our search tree --- whenever the value of the counter excesses $l(\phi)$, we break the computation process and return answer "no".

Of course, function $l$ may be uncomputable, but that is not a problem --- it suffices to bound $l$ from the above by any computable function. Functions like: $$n^n$$ $$\left.n^{n^{\cdots^n}}\right\}n$$ $$\mathit{Ackermann}(n, n)$$ grow incredibly fast, and, together with their compositions, are clearly computable. We can just carefully choose one of such functions relatively to our proof system.

(The gap in the above "proof" is in the last statement --- the length of the shortest proof of a formula, grows asymptotically faster than any computable function.)

The lesson that should be taken from the above considerations, is that the true difficulty of solving uncomputable problems is not in the fact that we cannot design an algorithm that always terminates, but in the fact that the "computational complexity" of these problems is just enormously high --- in some sense the cost of solving these problems is so big, that we cannot effectively separate it from infinity (and so, sometimes our algorithms fail to halt at all).

When people come first to the concept of computability, they usually regret the fact that some problems are uncomputable, and try to "repair" this situation --- typically by "completing" the concept of computability, or in other terms, by making the negation commute with the computation. The crucial thing to understand here is that there is nothing to regret, and that the idea of "repairing" the situation is completely crazy --- uncomputable problems are just complex in their nature.

B) One may formalize your question in the following way. Let us say that a problem $f$ is in $P/Q$ if there exists a sequence $A_1, A_2, \dotsc$ of algorithms with the following property:

• $A_k$ collectively solves $f$ in time $P$, that is --- there exists a function $p \in P$, such that for every natural $k$ and for every $x$ such that $|x| \leq k$ algorithm $A_k$ halts on $x$ in at most $p(k)$ steps and $A_k(x) = f(x)$
• sizes of algorithms $A_k$ are bounded by $Q$, that is --- there exists a function $q \in Q$ such that the size of $A_k$ is at most $q(k)$.

(In fact, the above is a hipster-way to define the non-uniform complexity hierarchy $P/Q$.)

Now, your question may be rephrased --- is the halting problem in $P/Q$, for any reasonable classes $P$ and $Q$? The answer to this question is no (assuming the natural coding of algorithms; otherwise there are silly examples --- i.e. the halting problem under unary coding is obviously in $n/\mathit{Poly}$, since every problem is in $n/\mathit{Exp}$).

• Let me remind you, that it is always a good idea to add a comment why you have voted down; otherwise such a down-vote is completely unconstructive. Dec 30 '13 at 17:59
• disagree the question is not research level & cited some research refs in my answer
– vzn
Dec 30 '13 at 21:12
• @vzn,the question "what is the smallest program in language ZXC / a smallest ZXC Turing machine / a shortest term in ZXC lambda calculus that computes QWE" is clearly non-trivial, and you may do a lot of great research answering such questions. It does not mean, however, that the initial question is not trivial. In fact, reading most of the answers given so far, makes me feel like I was completely drunk- they seem to me completely ridiculous, with the icing on the cake- let me paraphrase it: "I expect that the product of two numbers is less than 128", without saying anything about the numbers. Dec 30 '13 at 23:39
• BTW, Joel's answer is nice :-) Dec 31 '13 at 0:01

as noted in other answers this question/problem is similar/nearly equivalent to the Busy beaver problem. the short answer is that even for "small" Turing Machines even with "not that many states", there are some known to be provably universal and therefore the halting problem is uncomputable on them.[1] in fact for "small" TMs it has been shown recently that the halting problem leads to questions about number-theoretic problems similar to the unresolved Collatz conjecture (as noted in another answer).[3] a few useful refs along these lines

[1] Small TMs and the generalized busy beaver competition, Michel (note: could only find .ps fmt for this paper)

[2] Small weakly universal TMs Woods/Neary

The undecidability of the halting problem is true only for a machine with an infinite number of states (where 'state' is the current configuration of all transistors on the machine, represented by a string of 1s and 0s).

Suppose you have a machine with only 8 transistors (hence only 256 states), and a program that runs on it. You can build a larger machine that will do the following:

1. Take 3 arguments:

• The program you wish to test for a halting problem.
• The program's accept-state.
• The program's reject-state.
2. Run the program on the original machine, and record the current state of that machine after every clock cycle.

3. If accept-state or reject-state are detected within no more than 256 clock cycles, then the original machine halts on your program.

4. Otherwise, the original machine does not halt on your program.

One might claim that all machines have a finite number of states, hence the undecidability of the halting problem is "a fiction".

However, the above solution leaves us with the same problem on the larger machine (especially if the implementation of that solution is bad enough to loop forever by itself).

• This is misleading. By definition, a Turing machine has only finitely many states but it has an unbounded tape so it has infinitely many potential configurations. Dec 30 '13 at 15:51