<div dir="ltr">Hi <span style="font-family:arial,sans-serif;font-size:12.8000001907349px">Kirill Elagin</span>,<br><br>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.<br>
<br>Here's a reference: <a href="http://www.haskell.org/pipermail/haskell-cafe/2003-May/004343.html">http://www.haskell.org/pipermail/haskell-cafe/2003-May/004343.html</a><br><br>Best,<br>Francisco Mota</div><div class="gmail_extra">
<br><br><div class="gmail_quote">On Thu, Sep 4, 2014 at 10:06 AM, Frédéric Blanqui <span dir="ltr"><<a href="mailto:frederic.blanqui@inria.fr" target="_blank">frederic.blanqui@inria.fr</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div bgcolor="#FFFFFF" text="#000000">
<br>
<div>Le 29/07/2014 23:26, Kirill Elagin a
écrit :<br>
</div>
<blockquote type="cite">
<div dir="ltr">
<div>Hello,<br>
<br>
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.<br>
<br>
</div>
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”,</div>
</blockquote>
Hi.<br>
<br>
You may be interested in the works of Bellantoni, Marion, Avanzini
& Moser, ... See for instance<br>
- <a href="http://dx.doi.org/10.2168/LMCS-9(4:9)2013" target="_blank">http://dx.doi.org/10.2168/LMCS-9(4:9)2013</a><br>
- <a href="http://dx.doi.org/10.4230/LIPIcs.RTA.2011.123" target="_blank">http://dx.doi.org/10.4230/LIPIcs.RTA.2011.123</a><br>
to cite just very few papers on this topic.<br>
<br>
Frédéric.<br>
<br>
<blockquote type="cite">
<div dir="ltr"> _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”)?<br>
<div>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.<br>
<br>
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?<br>
I haven't come up with any answers to those ones yet.<br>
<div><br>
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.<br>
I feel that negative results are most likely to come from
the computability theory, while positive ones—from more
specific fields.<br>
<br>
Is there an ultimate source of this kind of funny, useless,
purely theoretical facts?<br>
</div>
</div>
</div>
<br>
<fieldset></fieldset>
<br>
<pre>_______________________________________________
Agda mailing list
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</div>
<br>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>