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

[Frédéric Blanqui]

Le 29/07/2014 23:26, Kirill Elagin a écrit :
> 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",
Hi.

You may be interested in the works of Bellantoni, Marion, Avanzini & 
Moser, ... See for instance
- http://dx.doi.org/10.2168/LMCS-9(4:9)2013
- http://dx.doi.org/10.4230/LIPIcs.RTA.2011.123
to cite just very few papers on this topic.

Frédéric.

> _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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140904/b51edf79/attachment.html