David Hopwood <[EMAIL PROTECTED]> writes: > Patricia Shanahan 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. > > I don't think Vesa was talking about trying to solve the halting problem. > > A type system that required termination would indeed significantly restrict > language expressiveness -- mainly because many interactive processes are > *intended* not to terminate.
Most interactive processes are written in such a way that they (effectively) consist of an infinitely repeated application of some function f that maps the current state and the input to the new state and the output. f : state * input -> state * output This function f itself has to terminate, i.e., if t has to be guaranteed that after any given input, there will eventually be an output. In most interactive systems the requirements are in fact much stricter: the output should come "soon" after the input has been received. I am pretty confident that the f for most (if not all) existing interactive systems could be coded in a language that enforces termination. Only the loop that repeatedly applies f would have to be coded in a less restrictive language. -- http://mail.python.org/mailman/listinfo/python-list
