[Agda] Positivity check

[Andreas Abel]

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
>


-- 
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/