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

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.

Answer 2

See the papers related to the Terminator project:

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

Answer 3

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 4

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 5

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 6

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 7

Termination Analyzer H is Not Fooled by Pathological Input D

When the halting problem is construed as requiring a correct yes/no answer to a contradictory question it cannot be solved. Any input D defined to do the opposite of whatever Boolean value that its termination analyzer H returns is a contradictory input relative to H.

In this case the best that any decider can possibly do is recognize that its input is contradictory (relative to itself) and reject it on that basis.

When H returns 1 for inputs that it determines do halt and returns 0 for inputs that either do not halt or do the opposite of whatever Boolean value that H returns then these pathological inputs are no longer contradictory and become decidable.

Can D correctly simulated by H terminate normally?
The x86utm operating system based on an open source x86 emulator. This system enables one C function to execute another C function in debug step mode. When H simulates D it creates a separate process context for D with its own memory, stack and virtual registers. H is able to simulate D simulating itself, thus the only limit to recursive simulations is RAM.

// The following is written in C
//
01 typedef int (*ptr)(); // pointer to int function
02 int H(ptr x, ptr y)   // uses x86 emulator to simulate its input
03
04 int D(ptr x)
05 {
06   int Halt_Status = H(x, x);
07   if (Halt_Status)
08     HERE: goto HERE;
09   return Halt_Status;
10 }
11
12 void main()
13 {
14   H(D,D);
15 }

Execution Trace
Line 14: main() invokes H(D,D);

keeps repeating (unless aborted)
Line 06: simulated D(D) invokes simulated H(D,D) that simulates D(D)

Simulation invariant:
D correctly simulated by H cannot possibly reach past its own line 06.

H correctly determines that D correctly simulated by H cannot possibly terminate normally on the basis that H recognizes a dynamic behavior pattern equivalent to infinite recursion. H outputs: "H: Infinitely Recursive Simulation Detected Simulation Stopped" indicating that D has defined a pathological (see above) relationship to H.

The x86utm operating system (includes several termination analyzers)
https://github.com/plolcott/x86utm

It compiles with the 2017 version of the Community Edition
https://visualstudio.microsoft.com/thank-you-downloading-visual-studio/?sku=Community&rel=15