Chris Smith wrote: > Patricia Shanahan <[EMAIL PROTECTED]> wrote: >> Vesa Karvonen wrote: >> ... >>> An example of a form of informal reasoning that (practically) every >>> programmer does daily is termination analysis. There are type systems >>> that guarantee termination, but I think that is fair to say that it is not >>> yet understood how to make a practical general purpose language, whose >>> type system would guarantee termination (or at least I'm not aware of such >>> a language). It should also be clear that termination analysis need not >>> be done informally. Given a program, it may be possible to formally prove >>> that it terminates. >> To make the halting problem decidable one would have to do one of two >> things: Depend on memory size limits, or have a language that really is >> less expressive, at a very deep level, than any of the languages >> mentioned in the newsgroups header for this message. > > Patricia, perhaps I'm misunderstanding you here. To make the halting > problem decidable is quite a different thing than to say "given a > program, I may be able to prove that it terminates" (so long as you also > acknowledge the implicit other possibility: I also may not be able to > prove it in any finite bounded amount of time, even if it does > terminate!) > > The fact that the halting problem is undecidable is not a sufficient > reason to reject the kind of analysis that is performed by programmers > to convince themselves that their programs are guaranteed to terminate. > Indeed, proofs that algorithms are guaranteed to terminate even in > pathological cases are quite common. Indeed, every assignment of a > worst-case time bound to an algorithm is also a proof of termination. > > This is, of course, a very good reason to reject the idea that the > static type system for any Turing-complete language could ever perform > this same kind analysis. >
Of course, we can, and should, prefer programs we can prove terminate. Languages can make it easier or harder to write provably terminating programs. Patricia -- http://mail.python.org/mailman/listinfo/python-list
