Matthias Blume wrote: > 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.
ACL2 is a subset of Common Lisp, and programs written in ACL2 are executable in Common Lisp. comp.lang.lisp is not only about Common Lisp, but even if it were, ACL2 would fit. Pascal -- 3rd European Lisp Workshop July 3 - Nantes, France - co-located with ECOOP 2006 http://lisp-ecoop06.bknr.net/ -- http://mail.python.org/mailman/listinfo/python-list
