[Agda] Theoretical limits of termination checking (reference request)

[Kirill Elagin]

Hello,

I was going through the great articles by Andreas Abel and I suddenly
started asking myself very basic questions about theoretical limits of
termination checking. The halting problem is often cited as an explanation
for impossibility of sound&complete termination checker. The termination
checking problem is not exactly the halting problem, but indeed it is quite
easy to derive impossibility of general termination checking from
impossibility of solving the halting problem.

But then, another question arises. When we encode proofs, say, in Agda, we
often have a terminating program in mind, but we have to write it down in
some specific way, so that the termination checker “sees” that the program
is fine. So, is it possible to develop a “programming style” such that
there is a sound&complete termination checker for programs “written in this
style”, _and_ any program can be “written in this style” (the “translation”
function is obviously not computable)? Formally: is there a subset of
programs, such that there is an algorithm correctly checking termination of
programs from this subset _and_ for any program there is an equivalent in
this subset (by “equivalent” I mean “extensionally equal”)?
I used to think that it is impossible, but I recently realized that my
“proof” was wrong. Turns out that when we are working with the whole
universe of programs, undecidability of termination checking follows from
undecidability of the halting problem. But if we restrict ourselves to a
subset, it is no longer necessarily true, and sound&complete termination
checking (for programs from this subset) _is_ possible for some subsets.

Then, there are more questions. How good can we become at translating
arbitrary programs to equivalents from some of those good subsets? As I
said, the translation function is clearly not computable. But can it be
that it is not computable only for programs we don't care about? Or maybe
it is not computable by algorithms, but computable by human brains? Are any
of the existing means of checking termination already “perfect” in this
sense, that is can I write _any_ terminating function, say, in MiniAgda, so
that it passes the termination check?
I haven't come up with any answers to those ones yet.

For some reason I couldn’t find any information on this topic. I guess that
either those questions are so trivial and the answers to them are so
obvious that no one even bothers to write them down, or everything about
this was published long ago in 70s, so it’s somewhat difficult to find
those papers now.
I feel that negative results are most likely to come from the computability
theory, while positive ones—from more specific fields.

Is there an ultimate source of this kind of funny, useless, purely
theoretical facts?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140730/c0a6b623/attachment.html