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. <div>
<br></div><div>If you're interested in the earlier thread, you can find it here: <a href="https://lists.chalmers.se/pipermail/agda/2011/003611.html">https://lists.chalmers.se/pipermail/agda/2011/003611.html</a></div><div class="gmail_extra">
<br><br><div class="gmail_quote">On Tue, Nov 13, 2012 at 2:27 PM, Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Yes, but please do not expect Agda to see this... :)<br>
<br>
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?<br>
<br>
Cheers,<br>
Andreas<div><div class="h5"><br>
<br>
On 13.11.2012 20:15, Andrew Cave wrote:<br>
</div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5">
Hi all,<br>
<br>
The following fails the positivity check, but it seems to me that it<br>
could be allowed to pass without introducing inconsistency. Thoughts?<br>
<br>
Regards,<br>
Andrew<br>
<br>
open import Data.Nat<br>
open import Data.Fin<br>
<br>
data functor (n : ℕ) : Set where<br>
▹ : (X : Fin n) -> functor n<br>
μ : (F : functor (suc n)) -> functor n<br>
_⇒_ : (A : functor zero) (F : functor n) -> functor n<br>
<br>
env : ℕ -> Set₁<br>
env n = ∀ (X : Fin n) -> Set<br>
<br>
extend : ∀ {n} -> env n -> Set -> env (suc n)<br>
extend ρ A zero = A<br>
extend ρ A (suc i) = ρ i<br>
<br>
mutual<br>
data μ' {n} (F : functor (suc n)) (ρ : env n) : Set where<br>
⟨_⟩ : ⟦ F ⟧ (extend ρ (μ' F ρ)) -> μ' F ρ<br>
<br>
⟦_⟧ : ∀ {n} -> functor n -> (ρ : env n) -> Set<br>
⟦ ▹ X ⟧ ρ = ρ X<br>
⟦ μ F ⟧ ρ = μ' F ρ<br>
⟦ A ⇒ F ⟧ ρ = ⟦ A ⟧ (λ ()) → ⟦ F ⟧ ρ<br>
<br>
<br>
<br></div></div>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
<br><span class="HOEnZb"><font color="#888888">
</font></span></blockquote><span class="HOEnZb"><font color="#888888">
<br>
<br>
-- <br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Theoretical Computer Science, University of Munich<br>
Oettingenstr. 67, D-80538 Munich, GERMANY<br>
<br>
<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~<u></u>abel/</a><br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</font></span></blockquote></div><br></div>