5.3. The Halting Problem 97
Proof. Namely, letSbe the set of ASCII strings, and for any strings 2 S, letf.s/
be the set of strings recognized byPs:
f.s/WWDft 2 SjPsrecognizestg:By convention, we associated a string procedure,Ps, with every string,s 2 S,
which makesfa total function, and by definition,
s 2 No-halt iff s...f.s/; (5.7)for all strings,s 2 S.
Now suppose to the contrary thatNo-haltwas recognizable. This means there is
some procedurePs 0 that recognizesNo-halt, which is the same as saying that
No-haltDf.s 0 /:Combined with (5.7), we get
s 2 f.s 0 / iff s...f.s/ (5.8)for alls 2 S. Now lettingsDs 0 in (5.8) yields the immediate contradiction
s 02 f.s 0 / iff s 0 ...f.s 0 /:This contradiction implies thatNo-haltcannot be recognized by any string pro-
cedure.
So that does it: it’s logically impossible for programs in any particular language
to solve just this special case of the general Halting Problem for programs in that
language. And having proved that it’s impossible to have a procedure that figures
out whether an arbitrary program returnsTrue, it’s easy to show that it’s impossible
to have a procedure that is a perfect recognizer foranycomplete run time property
of programs.
For example, most compilers do “static” type-checking at compile time to ensure
that programs won’t make run-time type errors. A program that type-checks is
guaranteed not to cause a run-time type-error. But since it’s impossible to recognize
perfectly when programs won’t cause type-errors, it follows that the type-checker
must be rejecting programs that really wouldn’t cause a type-error. The conclusion
is that no type-checker is perfect —you can always do better!
It’s a different story if we think about thepracticalpossibility of writing pro-
gramming analyzers. The fact that it’s logically impossible to analyze perfectly
arbitrary programs does not mean that you can’t do a very good job analyzing in-
teresting programs that come up in practice. In fact these “interesting” programs are