<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>