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

[Kirill Elagin]

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> 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
>> 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/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140731/fa04bb08/attachment.html