<div dir="ltr"><div>Hi Francisco,<br><br>Thanks for the reference! I’m afraid the argument doesn’t work in this particular situation…<br>The problem is that it is assumed there that the subset we are looking for consists _entirely_ of terminating programs. But what I’m asking about is a set that might also contain some non-terminating ones. Instead I want a termination checker to exist for this subset. What this means for that proof is that `eval` is not total and neither is `evil`.<br><br>To give an idea of what I’m talking about consider the following “coding style”. (By the way, the term “programming language” usually means “Gödel numbering” in computability theory, that is, there must be a translator from any other language; that’s why I’m using the term “coding style”–it will be a numbering, but it won’t be a Gödel one.) So, take any programming language (say, C++) and add a requirement that each function definition is annotated with a boolean value saying whether the function is total or not. Clearly, any C++ program can be written this way but the translation is not computable (there is no way to know what to put in the annotation for a given function). Now the termination checker is trivial, it just takes a function and outputs its annotation. So, as I mentioned in my first post, such coding styles exist.<br><br>But, well, this stuff is totally useless, because, as already pointed out by Thomas, membership in the set of programs correctly written in this style can’t be decidable.<br><br></div>So what I learned so far:<br>1. No total language is “perfect.”<br>2. There are “perfect” “coding styles”.<br>3. If a “coding style” is perfect then it is not decidable (and I keep saying “coding style” because it is somehow a more general concept since “programming languages” implicitly include a decision procedure).<br>4. Undecidable “coding styles” are useless (this is not a formally proved proposition, but things just work this way).<br><br>The remaining questions are: how close to “perfect” a programming language or a useful (decidable) coding style can be? How good can we (or computers) become in translating programs into such a close-to-perfect coding style (note that this question is redundant for programming languages as the definition of Gödel sets actually requires existence of a computable translator)?<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Sep 4, 2014 at 6:30 PM, Francisco Mota <span dir="ltr">&lt;<a href="mailto:fmota91@gmail.com" target="_blank">fmota91@gmail.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">I meant to say &quot;decidable subset of <i>terminating</i> programs&quot;.</div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><br><div class="gmail_quote">On Thu, Sep 4, 2014 at 10:29 AM, Francisco Mota <span dir="ltr">&lt;<a href="mailto:fmota91@gmail.com" target="_blank">fmota91@gmail.com</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Hi <span style="font-family:arial,sans-serif;font-size:12.8000001907349px">Kirill Elagin</span>,<br><br>
&gt;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&#39;t know how to translate them. The answer to that question is no, and the proof follows by diagonalization.<br>

<br>Here&#39;s a reference: <a href="http://www.haskell.org/pipermail/haskell-cafe/2003-May/004343.html" target="_blank">http://www.haskell.org/pipermail/haskell-cafe/2003-May/004343.html</a><br><br>Best,<br>Francisco Mota</div>
<div><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">&lt;<a href="mailto:frederic.blanqui@inria.fr" target="_blank">frederic.blanqui@inria.fr</a>&gt;</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&amp;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&amp;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
    &amp; 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&amp;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&#39;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&#39;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" target="_blank">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>
</div></div></blockquote></div><br></div>
</div></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>