[Agda] productivity of fibonacci stream

[Adam Krupicka]

Hi,

I think Agda needs help figuring out that zipWith doesn't do something
silly, like throw away the first element of both lists before zipping,
thus making the definitin of fib unproductive.
We can ensure this by using sized types:


open import Agda.Builtin.Nat public
open import Size

record Stream (A : Set) (i : Size) : Set where
  coinductive
  field
    hd : A
    tl : {j : Size< i} → Stream A j
open Stream

zipWith : {A B C : Set} {i : Size} → (A → B → C) → Stream A i → Stream B i → Stream C i
hd (zipWith f xs ys) = f (hd xs) (hd ys)
tl (zipWith f xs ys) = zipWith f (tl xs) (tl ys)

fib : ∀ {i} → Stream Nat i
hd fib = 0
hd (tl fib) = 1
tl (tl fib) = zipWith _+_ fib (tl fib)


A.K.


Noam Zeilberger <noam.zeilberger at gmail.com> writes:

> Hello Agda List,
>
> This might be a FAQ, but I was wondering why the canonical
> implementation of the stream of Fibonacci numbers using copatterns
> does not pass Agda's termination checker? By "canonical
> implementation" (cf. section 2.3 of
> http://www2.tcs.ifi.lmu.de/~abel/popl13.pdf), I mean the following:
>
> ====
> open import Agda.Builtin.Nat public
>
> record Stream (A : Set) : Set where
>   coinductive
>   field
>     hd : A
>     tl : Stream A
> open Stream
>
> zipWith : {A B C : Set} → (A → B → C) → Stream A → Stream B → Stream C
> hd (zipWith f xs ys) = f (hd xs) (hd ys)
> tl (zipWith f xs ys) = zipWith f (tl xs) (tl ys)
>
> fib : Stream Nat
> hd fib = 0
> hd (tl fib) = 1
> tl (tl fib) = zipWith _+_ fib (tl fib)
> ====
>
> which yields the following warning:
> ====
> Termination checking failed for the following functions:
>   fib
> Problematic calls:
>   fib
>     (at .../Fib.agda:19,27-30)
>   tl fib
>     (at .../Fib.agda:19,35-38)
> ====
>
> Any hints as to why Agda is complaining?
>
> Noam
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda