<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&data=02%7C01%7Cguillaume.allais%40strath.ac.uk%7C2621c4e07e464f077c5508d866cfd38d%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637372390376274061&sdata=b8TfnaT0geUFasxnk37guF9xVws%2F%2FZuV8Dn%2BOTn4fBg%3D&reserved=0">https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=02%7C01%7Cguillaume.allais%40strath.ac.uk%7C2621c4e07e464f077c5508d866cfd38d%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637372390376274061&sdata=b8TfnaT0geUFasxnk37guF9xVws%2F%2FZuV8Dn%2BOTn4fBg%3D&reserved=0</a>
</pre>
</blockquote>
<br>
</body>
</html>