[Agda] Problem with coinduction and positivity checker

[Andreas Abel]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

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

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  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFJv9VEPMHaDxpUpLMRArbZAJ4p9fYasCjUXn2fDj2av45uXr4AgACgwQIe
nWqoWCxzB03cURYqh34dp+8=
=5l6Q
-----END PGP SIGNATURE-----