[Agda] Understanding productivity

[Daniel Peebles]

Hi all,

I've been experimenting with more constructive definitions of
Data.Nat.InfinitelyOften for some experiments with primality. I have a few
types that are progressively more informative than the one in the standard
library, but the "most informative" is the following:

data Infinite {p} (P : ℕ → Set p) (x : ℕ) : Set p where
  yes : ( px :   P x) (pxs : ∞ (Infinite P (1 + x))) → Infinite P x
  no  : (¬px : ¬ P x) (pxs :    Infinite P (1 + x))  → Infinite P x


I thought I understood how the productivity checker worked, but I guess I
don't, because my naive understanding of it allows me to write nonsense
like:

product : ∀ {x p q} {P : ℕ → Set p} {Q : ℕ → Set q} → Infinite P x →
Infinite Q x → Infinite (λ n → P n × Q n) x
product (yes px pxs) (yes py pys) = yes (px , py) (♯ (product (♭ pxs) (♭
pys)))
product (yes px pxs) (no ¬py pys) = no (¬py ∘ proj₂) (product (♭ pxs) pys)
product (no ¬px pxs) (yes py pys) = no (¬px ∘ proj₁) (product pxs (♭ pys))
product (no ¬px pxs) (no ¬py pys) = no (¬px ∘ proj₁) (product pxs pys)

In fact, my version of Agda (compiled a few months ago, admittedly) even
lets me typecheck that definition without giving me any
termination/productivity pink warnings. Attempting to prove false then
leads to Agda spinning indefinitely. Apparently a more recent version does
catch the bad definition, but I don't understand what conditions it's using
to figure it out. Each clause, in isolation, is either productive or
decreasing, and that's where my naive understanding of
termination/productivity ends. Intuitively, the above definition is clearly
false, so I'm guessing with mixed (co)inductive definitions like my
Infinite type above, the productivity checker needs to do something more
clever to catch silly definitions like this? Can someone elaborate on what
kind of reasoning it applies?

Thanks,
Dan
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20121102/f43f5cc4/attachment.html