<div dir="ltr">Isn’t this just deciding whether a given program computes a primitive-recursive function?<br>I think so, because the programs expressible in LOOP are exactly the primitive-recursive ones, right?<br><br>Assume the problem is decidable.<br>
Given a program `q` define a program `f_q`:<br><br> def f_q(x):<br> q(q)<br> return 1<br><br>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.<br>
So, `f_q` computes a primitive-recursive function <=> `q(q)` halts. This solves the halting problem.<br></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Thu, Jul 31, 2014 at 12:13 PM, Andreas Abel <span dir="ltr"><<a href="mailto:abela@chalmers.se" target="_blank">abela@chalmers.se</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">To make things a bit more concrete, one could ask<br>
<br>
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).<br>
<br>
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).<div><div class="h5"><br>
<br>
<br>
On 29.07.2014 23:26, Kirill Elagin wrote:<br>
</div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5">
Hello,<br>
<br>
I was going through the great articles by Andreas Abel and I suddenly<br>
started asking myself very basic questions about theoretical limits of<br>
termination checking. The halting problem is often cited as an<br>
explanation for impossibility of sound&complete termination checker. The<br>
termination checking problem is not exactly the halting problem, but<br>
indeed it is quite easy to derive impossibility of general termination<br>
checking from impossibility of solving the halting problem.<br>
<br>
But then, another question arises. When we encode proofs, say, in Agda,<br>
we often have a terminating program in mind, but we have to write it<br>
down in some specific way, so that the termination checker “sees” that<br>
the program is fine. So, is it possible to develop a “programming style”<br>
such that there is a sound&complete termination checker for programs<br>
“written in this style”, _and_ any program can be “written in this<br>
style” (the “translation” function is obviously not computable)?<br>
Formally: is there a subset of programs, such that there is an algorithm<br>
correctly checking termination of programs from this subset _and_ for<br>
any program there is an equivalent in this subset (by “equivalent” I<br>
mean “extensionally equal”)?<br>
I used to think that it is impossible, but I recently realized that my<br>
“proof” was wrong. Turns out that when we are working with the whole<br>
universe of programs, undecidability of termination checking follows<br>
from undecidability of the halting problem. But if we restrict ourselves<br>
to a subset, it is no longer necessarily true, and sound&complete<br>
termination checking (for programs from this subset) _is_ possible for<br>
some subsets.<br>
<br>
Then, there are more questions. How good can we become at translating<br>
arbitrary programs to equivalents from some of those good subsets? As I<br>
said, the translation function is clearly not computable. But can it be<br>
that it is not computable only for programs we don't care about? Or<br>
maybe it is not computable by algorithms, but computable by human<br>
brains? Are any of the existing means of checking termination already<br>
“perfect” in this sense, that is can I write _any_ terminating function,<br>
say, in MiniAgda, so that it passes the termination check?<br>
I haven't come up with any answers to those ones yet.<br>
<br>
For some reason I couldn’t find any information on this topic. I guess<br>
that either those questions are so trivial and the answers to them are<br>
so obvious that no one even bothers to write them down, or everything<br>
about this was published long ago in 70s, so it’s somewhat difficult to<br>
find those papers now.<br>
I feel that negative results are most likely to come from the<br>
computability theory, while positive ones—from more specific fields.<br>
<br>
Is there an ultimate source of this kind of funny, useless, purely<br>
theoretical facts?<br>
<br>
<br></div></div>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
<br><span class="HOEnZb"><font color="#888888">
</font></span></blockquote><span class="HOEnZb"><font color="#888888">
<br>
<br>
-- <br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Department of Computer Science and Engineering<br>
Chalmers and Gothenburg University, Sweden<br>
<br>
<a href="mailto:andreas.abel@gu.se" target="_blank">andreas.abel@gu.se</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~<u></u>abel/</a><br>
</font></span></blockquote></div><br></div>