Incompletely Undecidable

7/30/2006 6:24:20 PM

Incompletely Undecidable

In one of my computer science courses, a professor prefaced his proof on the impossibility of translating from one language to another with the comment: “Next time you are ever asked to write a converter from Pascal to C, consider this.” I immediately thought, skeptically, “while arbitrary translation is impossible in general, translation between C and Pascal is actually trivial, since these two languages are virtually isomorphic.”

I have always been skeptical of the real world applicability of various proofs that place a limit of human knowledge, particularly with Godel’s Incompleteness Theorem in the mathematical realm and with undecidability in the computing realm. The standard proofs typically contain contrived, self-referential arguments. GIT states “this statement cannot be proved” cannot be proved true or false, while the classic undecidability problem, “the Halting Problem,” defines a halt function, which basically determines if any function halts on input, and uses that same function as input.

Such proofs cause people to exclude useful programs like powerful static checkers from consideration, when, in fact, most interesting inputs that occur in practice are solvable.

In this introductory paper “Extended Static Checking for Java” by the developers of ESC/Java, the authors come roughly to the same conclusion:

730esc

The horizontal line in Figure 1 labeled the “decidability ceiling” reflects the well-known fact that the static detection of many errors of engineering importance (including array bounds errors, null dereferences, etc.) is undecidable. Nevertheless, we aim to catch these errors, since in our engineering experience, they are targets of choice after type errors have been corrected, and the kinds of programs that occur in undecidability proofs rarely occur in practice. To be of value, all a checker needs to do is handle enough simple cases and call attention to the remaining hard cases, which can then be the focus of a manual code review.

Update: Interestingly, the not-so-reliable Wikipedia actually indicates the halting problem is decidable for deterministic machines with finite memory, which pretty much covers all existing computers and puts more wood into the fire.

Comments

 

Navigation

Categories

About

Net Undocumented is a blog about the internals of .NET including Xamarin implementations. Other topics include managed and web languages (C#, C++, Javascript), computer science theory, software engineering and software entrepreneurship.

Social Media