[Agda] Understanding productivity

[Andreas Abel]

Hi Dan,

it is good that your definition does not pass in Agda anymore.  ;-) 
Because, as you realized, it is not productive.

 > Each clause, in isolation, is either
 > productive or decreasing, and that's where my naive understanding of
 > termination/productivity ends.

Well, you need a common termination order.  It is not sufficient to 
consider each clause in isolation.  Consider:

   f (suc x) y = f x (suc y)
   f x (suc y) = f (suc x) y

Each clause is decreasing on some argument, but the whole thing 
diverges.  There is no common termination order.

The same applies to productivity checking.  The clauses which are not 
guarding need to exhibit a common termination order.  In your example, 
only clause 1 is guarding (because of the delay #).  Clause 4 is fine 
since it decreases both arguments.  But clause 2 is only decreasing 
argument 2 while increasing argument 1 (because of the forcing \flat). 
Clause 3 is doing the opposite.  So the whole thing should be rejected.

Hope that helps, let me know...

Cheers,
Andreas

On 02.11.12 11:20 PM, Daniel Peebles wrote:
>
> 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?

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