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

[Andreas Abel]

Or simply

   q;
   return 1

Yes, I guess the answer to my question is trivially reducible to the 
halting problem.

On 31.07.2014 14:17, Kirill Elagin wrote:
> Isn’t this just deciding whether a given program computes a
> primitive-recursive function?
> I think so, because the programs expressible in LOOP are exactly the
> primitive-recursive ones, right?
>
> Assume the problem is decidable.
> Given a program `q` define a program `f_q`:
>
>      def f_q(x):
>          q(q)
>          return 1
>
> Now, if `q(q)` halts, `f_q` is equivalent to `const 1`, which is
> primitive-recursive. Otherwise it is equivalent to infinite loop which
> is not primitive-recursive.
> So, `f_q` computes a primitive-recursive function <=> `q(q)` halts. This
> solves the halting problem.
>
>
> On Thu, Jul 31, 2014 at 12:13 PM, Andreas Abel <abela at chalmers.se
> <mailto:abela at chalmers.se>> wrote:
>
>     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 <mailto:Agda at lists.chalmers.se>
>         https://lists.chalmers.se/__mailman/listinfo/agda
>         <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 <mailto:andreas.abel at gu.se>
>     http://www2.tcs.ifi.lmu.de/~__abel/ <http://www2.tcs.ifi.lmu.de/~abel/>
>
>
>
>
> _______________________________________________
> 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/