<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
  </head>
  <body>
    <tt>Hi Vlad,<br>
      <br>
      I agree with you: to prevent inconsistencies Agda rejects more
      programs than<br>
      necessary. In the case we are interested in, Agda has a notion of
      "trusted"<br>
      sources of `Size< i` that may be use to prove termination of a
      definition<br>
      using sized types. And arbitrary functions are not one such
      trusted sources<br>
      (they're essentially inductive types & projections out of
      record IIRC).<br>
      <br>
      Best,<br>
      gallais<br>
    </tt><br>
    <div class="moz-cite-prefix">On 02/10/2020 13:36, vlad wrote:<br>
    </div>
    <blockquote type="cite"
      cite="mid:3c463a2e-9c62-82b9-c8be-5d3698aba055@inria.fr">
      <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
      <p>Dear Agda users,</p>
      <p>I am new to this list and fairly new to Agda as well. While
        attempting a certain development I've run into an issue about
        non-termination, in a setting where I was expecting Sized types
        to ensure termination. I think I have an explanation why this
        happens, but I would like to see what specialists have to say.
        Apologies in advance for the long post.</p>
      <p>Consider the following piece of code (V1) :</p>
      <p><i>{-#  OPTIONS --size #-}</i><i><br>
        </i><i>open import Size</i><i><br>
        </i><i>postulate</i><i><br>
        </i><i>  P : Size → Set</i><i><br>
        </i><i>  P-Size :  (∀ (i : Size) → (∀ (j : Size< i) → P j) →
          P i)</i><i><br>
        </i><i>nonterminating : ∀ (i : Size) → P i</i><i><br>
        </i><i>nonterminating i = P-Size i λ { j → nonterminating j } </i><br>
      </p>
      <p>The recursive call to <i>nonterminating</i> is <i>j </i>of
        type <i>Size< i</i>, where<i> i : Size</i> is the argument
        of <i>nonterminating</i>. So, I would expect Agda to accepts
        this, since the Size argument <i>j</i> of the recursive call is
        less than the Size argument <i>i</i> of the function. However,
        Agda rejects this as, well, ... nonterminating. While trying to
        understand what's going on I modified the code as follows : I've
        replaced the postulate by hypotheses in the definition (V2) :<br>
      </p>
      <p><i>nonterminating' :  (P : Size → Set)</i><i><br>
        </i><i>                              (P-Size :  (∀ (i : Size) →
          (∀ (j : Size< i) → P j) → P i)) →</i><i><br>
        </i><i>                              ( ∀ (i : Size) → P i)</i><i>
          <br>
        </i><i>nonterminating' P P-Size i = P-Size i λ    { j →
          nonterminating' P P-Size j  }</i></p>
      <p>Looking at (V2) one can notice that <i>nonterminating' </i>
        looks like a well-founded induction principle for the <i>_<_</i><i>
        </i>relation on <i>Size</i>, defined by <i>j < i </i>iff<i>
          (t : Size< i).</i> Which is strange since <i>_<_</i> is
        *not* well founded, as <i>∞ < ∞ </i>holds. Indeed, if <i>nonterminating'</i>
        were accepted then it could be used to prove that <i>_<_ </i>is 
        well  founded: just take <i>P s = "there is no infinite
          <-decreasing sequance starting at s"</i>. So, I believe the
        Agda termination checker rightfully rejects the definition (V2).
        <br>
      </p>
      <p>However, the termination checker also rejects (V1), which to me
        looks not obviously problematic. It is not, I believe,
        equivalent to to (V2) : (V2) says something about *all*
        predicates <i>P</i> with such-and-such properties, whereas (V1)
        just postulates the properties for *some* (also postulated)
        predicate P<i>.</i></p>
      <p>So, I'm assuming the following happens. The Agda termination
        checker, presumably based on some type system, rejects (V2), and
        rightly so because accepting it would leads to an inconsistency
        : <i>_<_</i><i> is well founded</i> vs. <i>∞ < ∞</i>.
        Now, termination is undecidable, so the termination
        checker/underlying type system necessarily rejects more
        definitions than it theoretically should. So, it also rejects 
        (V1), as, due to inevitable approximations in this undecidable
        setting,  it it does not distinguish the possibly unproblematic
        (V1) from the definitely problematic (V2).</p>
      <p> Does any of this make sense ? <br>
      </p>
      <p> Thanks in advance for any explanations !<br>
      </p>
      <p>- Vlad Rusu<br>
      </p>
      <br>
      <fieldset class="mimeAttachmentHeader"></fieldset>
      <pre class="moz-quote-pre" wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&amp;data=02%7C01%7Cguillaume.allais%40strath.ac.uk%7C2621c4e07e464f077c5508d866cfd38d%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637372390376274061&amp;sdata=b8TfnaT0geUFasxnk37guF9xVws%2F%2FZuV8Dn%2BOTn4fBg%3D&amp;reserved=0">https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&amp;data=02%7C01%7Cguillaume.allais%40strath.ac.uk%7C2621c4e07e464f077c5508d866cfd38d%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637372390376274061&amp;sdata=b8TfnaT0geUFasxnk37guF9xVws%2F%2FZuV8Dn%2BOTn4fBg%3D&amp;reserved=0</a>
</pre>
    </blockquote>
    <br>
  </body>
</html>