on termination

[Carl R. Witty]

"Cagdas Ozgenc" <co19@cornell.edu> 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