[Agda] Positivity check

[Andrew Cave]

Ah, I see; it's more subtle than I initially thought. I initially thought
it was just a matter of observing that rho wasn't used to the left of the
arrow. Thanks. I see now it's exactly as you said that it would need to see
that the occurrences of mu' to the left of the arrow are in some way
"different" mus.

Regards,
Andrew

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/>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20121122/71bf6190/attachment.html