why there can't be a program that checks another program

Question

Hello all

I am trying to find the logical alan turing explanation why there can't be a program that checks another programs.

I remember we learned in on the computation course but now i just can't find the solution , and i need to explain it to some one at my work .

Thanks for help.

Answer 1

You are looking for the halting problem.

Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist. We say that the halting problem is undecidable over Turing machines.

Answer 2

There's the wikipedia entry on this...

But basically, in order to determine if any sufficiently complicated program is stoppable, you'd have to run it in order to trace the execution path. That means you're back to one program running another program, and if that program doesn't stop, the program that's watching it won't stop either.

It's like calculating the digits to pi-- will it stop? How can you say it's infinite in runtime, as opposed to suffering from some computational problem? We know that that particular problem is infinite, but others that are similar have not been so proven.

Answer 3

Byron's answer should point you to the important info. As an aside, you can have a program that checks a specific program. What you can't have is a program that checks an arbitrary program for correctness.

Answer 4

"Checks another program" is very broad. In fact, some features of programs can be checked, such as whether or not a Java program type checks. However, type checking a Java program will also reject some programs which will never actually produce a type error when run, such as:

int foo() {
    if (true) return 5;
    else return null;
}

This method will never actually return null, but the type checker can't see this. But couldn't we just make a smarter type system?

Unfortunately, the answer is no. Consider the following program:

int bar() {
    if (infiniteComputation()) return 5;
    else return null;
}

The type checker can't check if infiniteComputation will ever return false, because of the halting problem.

Another related theorem is Rice's Theorem, which is probably closer to what your question was about than the halting problem.

It is worth pointing out that the theorem only state that there is no program property which can be accurately checked, it is still possible to approximate such checks well enough for practical purposes. One example is type systems, where we accept that some "correct" programs are rejected, like the snippet above. Compilers can also eliminate dead code in a lot of cases, even though it impossible to do in every case.