Is there a "good enough" solution for the halting problem?

Question

It is known that the halting problem cannot have a definite solution, one that a) returns true <==> the program does indeed halt, and b) handles any input, but I was wondering if there are good enough solutions to the problem, ones that can maybe handle certain types of program flows perfectly, or are able to identify when it cannot correctly solve the problem, or one that is right a high percentage of times, and so on....

If so, how good are they, and what ideas/limitations do they rely on?

Answer 1

See the papers related to the Terminator project:

http://research.microsoft.com/en-us/um/cambridge/projects/terminator/

Answer 2

ones that can maybe handle certain types of program flows perfectly

This is easy, and the easier the more narrow your "certain types" are. Primitive example: decide whether the following piece of code terminates, for arbitrary starting values of x:

void run(int x)
{
    while(x != 0)
    {
        x = x > 0 ? x-2 : x+2;
    }
}

The solution is shorter than the code itself.

or are able to identify when it cannot correctly solve the problem

Again easy: take program above, make it reply "no" when the program does not fit the fixed narrow schema.

or one that is right a high percentage of times

How do you define a "high" percentage over an infinite set of possible inputs?

Answer 3

One way to prove a loop halts is to identify some integer variable (not necessarily explicitly in the program) that always decreases each time the loop is executed, and that once that variable is less than zero, the loop will terminate. We can call this variable a loop variant.

Consider the following little snippet:

var x := 20;
while (x >= 0) {
    x := x - 1
}

Here, we can see that x decreases each time the loop is executed, and that the loop will exit once x < 0 (obviously, this isn't very rigorous, but you get the idea). Therefore, we can use x as a variant.

What about a more complicated example? Consider a finite list of integers, L = [L[0], L[1], ..., L[n]]. in(L, x) is true if x is a member of L. Now consider the following program:

var x := 0;
while (in(L, x)) {
    x := x + 1
}

This will search through the natural numbers (0, 1, 2, ...), and stop once it has found a value for x that is not in L. So, how do we prove that this terminates? There has to a maximal value in L -- call it max(L). We can then define our variant as max(L) - x. To prove termination, we first have to prove that max(L) - x is always decreasing -- not too hard since we can prove x is always increasing. We then to have prove that the loop will terminate when max(L) - x < 0. If max(L) - x < 0, then max(L) < x, which means that x cannot possibly be in L, and so the loop will terminate.

Answer 4

Sometimes it's obvious whether a machine will halt or not, even if it's very large. Once you identify a pattern, like the presence of a "countdown" variable, you can write a small machine that will work for any machine that has it. That's an infinite family, but a negligible sliver of all possible machines. Most human-written machines have very simple behavior for their size, so it wouldn't surprise me too much if a lot of them could be solved in practical time/space, but I have no idea how to measure that.

To give you an idea of how tough the "how good are they" problem is, here's is a question of great theoretical interest: for a given size N, how many machines of size N halt? This is uncomputable (because a machine that could compute it could be used to solve the halting problem) and not known for N>4.

Answer 5

Yes, just make the state space finite, and it's (theoretically) possible for all inputs. (Simply iterate over all possibilities.)

So it's theoretically possible for any program running on a real computer. (You may have to use a computer with a greater amount of RAM, than the one which should execute the program, to do the analysis. And of course, the analysis would take incredibly long.)

Probably you want something more practical though. In this case, think about languages. The problem of syntactical correctness/incorrectness can be determined pretty quickly (depending on the kind of language, and on the input length), although there are infinitely many programs you could supply as input. (Note: We're not talking about executing the input program, just determining if it's syntactically correct or not.)

Answer 6

Isn't the halting problem more of a though experiment to demonstrate the limits of computability than an actual problem?

Answer 7

The normal approach is to constrain program behavior to an effectively calculable algorithm. For example, the simply typed lambda calculus can be used to determine that an algorithm always halts. This means that the simply typed lambda calculus is not Turing complete, but it is still powerful enough to represent many interesting algorithms.