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!
 A: 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.
A: 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.
A: 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).
A: 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.
A: 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}$).
A: 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.
A: 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
[3] Problems in number theory from the busy beaver competition Michel
A: 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. 
A: 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.
A: 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:


*

*Take 3 arguments:


*

*The program you wish to test for a halting problem.

*The program's accept-state.

*The program's reject-state.


*Run the program on the original machine, and record the current state of that machine after every clock cycle.

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

*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).
