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. A language for which the halting problem is decidable must also be a language in which it is impossible to simulate an arbitrary Turing machine (TM). Otherwise, one could decide the notoriously undecidable TM halting problem by generating a language X program that simulates the TM and deciding whether the language X program halts. One way out might be to depend on the boundedness of physical memory. A language with a fixed maximum memory size cannot simulate an arbitrary TM. However, the number of states for a program is so great that a method that depends on its finiteness, but would not work for an infinite memory model, is unlikely to be practical. Patricia -- http://mail.python.org/mailman/listinfo/python-list
