Patricia Shanahan wrote: > Pascal Costanza wrote: >> 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. > > To prove Turing-completeness of ACL2 from Turing-completeness of Common > Lisp you would need to run the reduction the other way round, showing > that any Common Lisp program can be converted to, or emulated by, an > ACL2 program.
Sorry, obviously I was far from being clear. ACL2 is not Turing-complete. All iterations must be expressed in terms of well-founded recursion. 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