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

[Andreas Abel]

To make things a bit more concrete, one could ask

   Given a program in specific Turing-complete language (say, a WHILE 
program), is there an extensionally equivalent program in a specific 
total language (say, a LOOP program).

I'd guess this question (of a WHILE-program being LOOP-representable) is 
undecidable, but I have not come across a proof yet (was not looking 
actively, though).


On 29.07.2014 23:26, Kirill Elagin wrote:
> 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?
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/