Any interesting, general program analysis is undecidable.
Yesterday we saw that the two-input halting problem is undecidable, meaning it has no solution that works for every input. Today we see that identifying any nontrivial functional characteristic of a procedure is undecidable.
Every procedure can be considered to be a partial function. Partial functions accept one or more inputs and, for some of those inputs, yield back an output. If the procedure runs forever we say there is not output for that input. If a procedure f given input x yields output y we say x↦y the symbol “↦” is pronounced “maps to”. or f(x) = y; if the input x causes f to run forever we say x↦⊥ The symbol “⊥” is pronounced “bottom” in this context. It is also used to mean “perpendicular to” in geometry. . If there are no x for which x↦⊥ then we have a total function. All total functions are also partial functions.
Partial functions embody the work done by procedures. They don’t tell us anything about efficiency or technique but they do embody the input-output mapping a procedure computes.
Determining any property of the partial function computed by a procedure is undecidable unless the property is true of either all or no procedures.
We can prove Rice’s theorem basically the same way we proved the undecidability of the two-input halting problem. Given a candidate procedure P that is reputed to tell us some property of the partial function computed by procedures We make a pathological program that first asks P if the property holds of itself and then does the oposite of what P says it will. A few simple examples:
I can never ever write a program that can correctly identify the presence or absence of a functional property of every procedure I give it. This includes nice little properties like “doesn’t send all my data to my competitors and then misuse my hardware until it overheats and fries” or “saves my documents when I ask it to.” And since anything that can be done can be done by a computer, there is no human process that can figure out these properties. There are programs of which I can neither prove nor disprove the existence of bugs.
That said, I can write programs and design human activities that correctly identify the presence or absence of a functional property of some procedures and says “too complicated” for the rest. As long as I can identify what I mean by a bug, I can write bug-free programs Note that “can write bug-free programs” ≠ “can write program x without bugs”. and prove that they are bug-free.
The problem we face in making reliable software is that the current sophistication of programs that inspect other programs is far far below the current complexity of programs people are willing to pay money for. We also don’t really have any idea how complicated a program can get before we can’t design a process to verify it lacks a particular bug and we don’t have a very good notion of what a bug is even if we did.
As ever, the difference between theory and practice is large in practice. The problems we can’t solve in practice are far greater than the problems we can’t solve in theory. But the fact that such a broad set cannot be solved in theory puts some limits on the aspirations of computer scientists at least.
Looking for comments…