"Cagdas Ozgenc" writes:

This may be a little off topic, but I could not get much response from = comp.theory, so here it goes:

Is it possible to have a programming language that can be used to = produce only the programs that terminate, but at the same time decide = all recursive languages? Or does such limitation automatically reduce = the class of languages that such a programming language decide to = primitive-recursive?

If you have any programming language (say Haskell), and if you have some formal system which is capable of proving termination properties of programs in your programming language (and in which proofs are machine-checkable), then you can create a new language "Terminating Haskell" simply by pairing each program with a proof of termination. Of course, if you start with a Turing-complete language, then your formal system is necessarily incomplete; this means there will be programs that do terminate but that you cannot prove terminate. So your programming language will include programs that decide all languages that you can prove recursive (in your formal system), but not all recursive languages. However, if your formal system is strong enough, it may be possible to prove termination of all the programs you really care about. Some theorem-proving systems (including ACL2 and PVS) are like this -- within the logic, you can write programs in a Turing-complete language, as long as you can prove termination. (More precisely, the language would be Turing-complete were it not for the termination requirement. In both cases, the "program" portion is fairly distinct from the "proof of termination" portion, so that it does make sense to talk about what the language would be like without the termination requirement.) It has long been a goal of mine to create a Haskell-like programming language where you could mark portions as being guaranteed to terminate. The compiler would prove termination whenever it could, but in cases where the termination proof was too complicated for automatic proofs, the programmer would be required to add an explicit proof of termination. Carl Witty