<html>
  <head>

    <meta http-equiv="content-type" content="text/html; charset=UTF-8">
  </head>
  <body>
    <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>
  </body>
</html>