[Agda] nontermination and Sized types

[guillaume allais]

Hi Vlad,

I agree with you: to prevent inconsistencies Agda rejects more programs than
necessary. In the case we are interested in, Agda has a notion of "trusted"
sources of `Size< i` that may be use to prove termination of a definition
using sized types. And arbitrary functions are not one such trusted sources
(they're essentially inductive types & projections out of record IIRC).

Best,
gallais

On 02/10/2020 13:36, vlad wrote:
>
> Dear Agda users,
>
> 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.
>
> Consider the following piece of code (V1) :
>
> /{-#  OPTIONS --size #-}//
> //open import Size//
> //postulate//
> //  P : Size → Set//
> //  P-Size :  (∀ (i : Size) → (∀ (j : Size< i) → P j) → P i)//
> //nonterminating : ∀ (i : Size) → P i//
> //nonterminating i = P-Size i λ { j → nonterminating j } /
>
> The recursive call to /nonterminating/ is /j /of type /Size< i/, 
> where/i : Size/ is the argument of /nonterminating/. So, I would 
> expect Agda to accepts this, since the Size argument /j/ of the 
> recursive call is less than the Size argument /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) :
>
> /nonterminating' :  (P : Size → Set)//
> //                              (P-Size :  (∀ (i : Size) → (∀ (j : 
> Size< i) → P j) → P i)) →//
> //                              ( ∀ (i : Size) → P i)//
> //nonterminating' P P-Size i = P-Size i λ    { j → nonterminating' P 
> P-Size j  }/
>
> Looking at (V2) one can notice that /nonterminating' / looks like a 
> well-founded induction principle for the /_<_///relation on /Size/, 
> defined by /j < i /iff/(t : Size< i)./ Which is strange since /_<_/ is 
> *not* well founded, as /∞ < ∞ /holds. Indeed, if /nonterminating'/ 
> were accepted then it could be used to prove that /_<_ /is well  
> founded: just take /P s = "there is no infinite <-decreasing sequance 
> starting at s"/. So, I believe the Agda termination checker rightfully 
> rejects the definition (V2).
>
> 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 /P/ with such-and-such 
> properties, whereas (V1) just postulates the properties for *some* 
> (also postulated) predicate 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 : /_<_//is well 
> founded/ vs. /∞ < ∞/. 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).
>
>  Does any of this make sense ?
>
>  Thanks in advance for any explanations !
>
> - Vlad Rusu
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> 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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201002/8ffa62f7/attachment.html>