[Agda] nontermination and Sized types

[vlad]

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

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