[Agda] Problem with coinduction and positivity checker

[Andreas Abel]

Hi Simon,

codata is still experimental in Agda, even more so data with \infty as 
\omegaChain below.  As discussed on the last Agda meeting, the semantics 
of data with \infty (mixed induction-coinduction) is a bit weird, I do 
not know the positivity conditions, and I think no one has done the 
theoretical work yet.

If you are confident about the soundness of your definition, just turn 
of the positivity check.

Cheers,
Andreas

Simon Foster a écrit :
> Hi,
> 
> I've been having problems with defining coinductive datatypes with
> associated constraints and the positivity checker. I found the emails
> below from 2009 which detail the same problem using an infinite Chains
> example, but the discussion does not appear conclusive. I tried the
> example and the positivity checker in the latest version of Agda still
> rejects the example.
> 
> Is this a bug in Agda or a theoretical problem?
> 
>> Darin Morrison wrote:
>>> Hi All,
>>>
>>> I'm working on a constructive domain theory module where I need a
>>> formalization of chains and ωchains but I'm having some problems with
>>> the positivity checker.
>>>
>>> Here is a snippet of the code I am using:
>>>
>>> -- Chains
>>>
>>> mutual
>>>   data Chain : ℕ → Set where
>>>     []    : Chain 0
>>>     _∷_,_ : ∀ {n} (x : carrier) (xs : Chain n) (p : x ≼ xs) → Chain (suc n)
>>>
>>>   _≼_ : ∀ {n} → carrier → Chain n → Set
>>>   _ ≼ []           = ⊤
>>>   x ≼ (x′ ∷ _ , _) = x ≤ x′
>>>
>>> head : ∀ {n} → Chain (suc n) → carrier
>>> head (x ∷ _ , _) = x
>>>
>>> -- ωChains
>>>
>>> mutual
>>>   data ωChain : Set where
>>>     _∷_,_ : ∀ (x : carrier) (xω : ∞ ωChain) (p : x ≼ xω) → ωChain
>>>
>>>   head : ωChain → carrier
>>>   head (x ∷ _ , _) = x
>>>
>>>   _≼_ : carrier → ∞ ωChain → Set
>>>   x ≼ xω = x ≤ head (♭ xω)
>>>
>>> The above encoding of Chains works great.  However, Agda complains
>>> that ωChain is not strictly positive because of (xω : ∞ ωChain).  Note
>>> that I am using the Coinduction module described by Nils in a previous
>>> post.
>>>
>>> If I change the definition of ωChain to the following, the positivity
>>> checker no longer complains:
>>>
>>> mutual
>>>   codata ωChain : Set where
>>>     _∷_,_ : ∀ (x : carrier) (xω : ωChain) (p : x ≼ xω) → ωChain
>>>
>>>   head : ωChain → carrier
>>>   head (x ∷ _ , _) = x
>>>
>>>   _≼_ : carrier → ωChain → Set
>>>   x ≼ xω = x ≤ head xω
>>>
>>> But this formulation is harder to work with for reasons discussed in
>>> several recent posts on codata.
>>>
>>> I'd rather not have to turn off the positivity checker.  Is there any
>>> way to get around this?  Perhaps the positivity checker should be
>>> modified not to complain in cases like this?
>>>
> 
> Andreas Abel wrote:
>> Surely, the positivity checker should not complain in your case, since
>> \infty is a monotone operation on Set.  Semantically,
>>
>>   \infty T = { t | \flat t \in T }
>>
>> thus, S \subseteq T implies \infty S \subseteq \infty T.
>>
>> So, your definition is perfectly positive.  Maybe you should file a bug
>> report.
>>
>> Cheers,
>> Andreas
> 
> Thanks,
> 
> --
> Simon Foster <s.foster at dcs.shef.ac.uk>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/