[Agda] Positivity check

[Daniel Peebles]

This sort of reminds me of my earlier email to this list from a while ago
about relaxing the positivity check. It feels a bit like some notion of
"decreasingness" should be relevant to whether a not-strictly-positive
definition is safe or not, but I don't have a good formal description of
what I mean by that.

If you're interested in the earlier thread, you can find it here:
https://lists.chalmers.se/pipermail/agda/2011/003611.html


On Tue, Nov 13, 2012 at 2:27 PM, Andreas Abel <andreas.abel at ifi.lmu.de>wrote:

> Yes, but please do not expect Agda to see this... :)
>
> Basically, what you are saying is that the mu' in the second clause of [[
> ... ]] is never the "same" mu' you started with in the constructor of mu'.
>  But can you make this formal by a static analysis?
>
> Cheers,
> Andreas
>
>
> On 13.11.2012 20:15, Andrew Cave wrote:
>
>> Hi all,
>>
>> The following fails the positivity check, but it seems to me that it
>> could be allowed to pass without introducing inconsistency. Thoughts?
>>
>> Regards,
>> Andrew
>>
>> open import Data.Nat
>> open import Data.Fin
>>
>> data functor (n : ℕ) : Set where
>>   ▹ : (X : Fin n) -> functor n
>>   μ : (F : functor (suc n)) -> functor n
>>   _⇒_ : (A : functor zero) (F : functor n) -> functor n
>>
>> env : ℕ -> Set₁
>> env n = ∀ (X : Fin n) -> Set
>>
>> extend : ∀ {n} -> env n -> Set -> env (suc n)
>> extend ρ A zero = A
>> extend ρ A (suc i) = ρ i
>>
>> mutual
>>   data μ' {n} (F : functor (suc n)) (ρ : env n) : Set where
>>    ⟨_⟩ : ⟦ F ⟧ (extend ρ (μ' F ρ)) -> μ' F ρ
>>
>>   ⟦_⟧ : ∀ {n} -> functor n -> (ρ : env n) -> Set
>>   ⟦ ▹ X ⟧ ρ = ρ X
>>   ⟦ μ F ⟧ ρ = μ' F ρ
>>   ⟦ A ⇒ F ⟧ ρ = ⟦ A ⟧ (λ ()) → ⟦ F ⟧ ρ
>>
>>
>>
>> ______________________________**_________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/**mailman/listinfo/agda<https://lists.chalmers.se/mailman/listinfo/agda>
>>
>>
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
>
> andreas.abel at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~**abel/ <http://www2.tcs.ifi.lmu.de/~abel/>
> ______________________________**_________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/**mailman/listinfo/agda<https://lists.chalmers.se/mailman/listinfo/agda>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20121113/8bb7bfae/attachment-0001.html