Matthias Blume wrote: > 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. [...] >>>>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.
This is absolutely consistent with what I said. While f could be coded in a system that *required* termination, the outer loop could not. As I mentioned in a follow-up, event loop languages such as E enforce this program structure, which would almost or entirely eliminate the need for annotations in a type system that proves termination of some subprograms. -- David Hopwood <[EMAIL PROTECTED]> -- http://mail.python.org/mailman/listinfo/python-list
