On Sep 30, 3:45 pm, RG <rnospa...@flownet.com> wrote: > In article <7xr5gbxfry....@ruckus.brouhaha.com>, > Paul Rubin <no.em...@nospam.invalid> wrote: > > > > > > > RG <rnospa...@flownet.com> writes: > > > Yes, I know I could have used lint. But that misses the point. For any > > > static analyzer, because of the halting problem, I can construct a > > > program that either contains an error that the analyzer will not catch, > > > or for which the analyzer will produce a false positive. > > > Can you describe any plausible real-world programs where the effort of > > complicated static is justified, and for which the halting problem gets > > in the way of analysis? By "real world", I meanI wouldn't consider > > searching for counterexamples to the Collatz conjecture to qualify as > > sufficiently real-world and sufficiently complex for fancy static > > analysis. And even if it did, the static analyzer could deliver a > > partial result, like "this function either returns a counterexample to > > the Collatz conjecture or else it doesn't return". > > > D. Turner wrote a famous paper arguing something like the above, saying > > basically that Turing completeness of programming languages is > > overrated: > > > http://www.jucs.org/jucs_10_7/total_functional_programming > > > The main example of a sensible program that can't be written in a > > non-complete language is an interpreter for a Turing-complete language. > > But presumably a high-assurance application should never contain such a > > thing, since the interpreted programs themselves then wouldn't have > > static assurance. > > There are only two possibilities: either you have a finite-state > machine, or you have a Turning machine. (Well, OK, you could have a > pushdown automaton, but there are no programming languages that model a > PDA. Well, OK, there's Forth, but AFAIK there are no static type > checkers for Forth. Besides, who uses Forth? ;-) > > If you have a finite state machine everything is trivial. If you have a > Turing machine everything is generally impossible. This is an > oversimplification but not far from the fundamental underlying truth. > > My favorite practical example is the square root function. The standard > C library defines a square root function on floats (actually on > doubles), which is to say, over a finite-state model with 2^64 states. > The model is not well defined over half of that range (negative > numbers), which the static type checker cannot catch because there is no > such thing as an unsigned double. > > But the fun doesn't stop there. Doubles >= 0.0 are not the only thing > one might reasonably want to take a square root of, and indeed C++ > overloads sqrt to work on complex and valarray types in addition to > floats of various lengths (though you still have to manually keep track > of whether or not the argument to sqrt might be a negative real). But > what if I want an exact integer square root? Or a square root of a data > type that represents irrational numbers not as floating point > approximations but as exact symbolic representations? I haven't worked > out the details, but I'd be surprised if none of these variations turned > out to be Turing complete. > > The Turner paper is right on point: there's a fundamental distinction > between the (known) finite and the (potentially) infinite. In my > experience most of the cool interesting stuff has been found in the > latter domain, and trying to shoehorn the latter into the former is more > trouble then it's worth. >
The FA or TM dichotomy is more painful to contemplate than you say. Making appropriate simplifications for input, any modern computer is a FA with 2^(a few trillion) states. Consequently, the gestalt of computer science seems to be to take it on faith that at some very large number of states, the FA behavior makes a transition to TM behavior for all possible practical purposes (and I mean all). So what is it--really--that's trivial to analyze? And what is impossible? I'm sorry this is drifting OT and will stop here. -- http://mail.python.org/mailman/listinfo/python-list
