Pascal Costanza <[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. > > Not quite. See http://en.wikipedia.org/wiki/ACL2
What do you mean "not quite"? Of course, Patricia is absolutely right. Termination-guaranteeing languages are fundamentally less expressive than Turing-complete languages. ACL2 was not mentioned in the newsgroup header. -- http://mail.python.org/mailman/listinfo/python-list
