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

[Francisco Mota]

I meant to say "decidable subset of *terminating* programs".


On Thu, Sep 4, 2014 at 10:29 AM, Francisco Mota <fmota91 at gmail.com> wrote:

> Hi Kirill Elagin,
>
> From what I understand, you are asking whether there can theoretically be
> a decidable subset of programs such that all total recursive functions have
> a corresponding program in this subset, even if we don't know how to
> translate them. The answer to that question is no, and the proof follows by
> diagonalization.
>
> Here's a reference:
> http://www.haskell.org/pipermail/haskell-cafe/2003-May/004343.html
>
> Best,
> Francisco Mota
>
>
> On Thu, Sep 4, 2014 at 10:06 AM, Frédéric Blanqui <
> frederic.blanqui at inria.fr> wrote:
>
>>
>> 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 listAgda at lists.chalmers.sehttps://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>>
>> _______________________________________________
>> 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/c716ac0e/attachment-0001.html