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!
Best Answer
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.