[Agda] productivity of fibonacci stream

[Guillaume Brunerie]

Hi Noam,

Here is my understanding of the situation.

In order for this definition of [fib] to be productive, the function
[zipWith] needs to have the special property that in order to produce one
element of the output, it should only look at at most two elements of its
first argument and at most at one element of its second argument.
Indeed, it’s possible to have for instance a function [Stream A -> Stream
A] which requires to look at ten elements of the input in order to produce
only one element of the output (for instance the function returning the
substream of elements with index divisible by 10). If it were the case for
[zipWith] then [fib] would clearly not be productive, as it would require
the second element of [tl fib] to produce the first element of [tl (tl
fib)] (which are the same element).

Now in your case, it happens that [zipWith] only needs one element of each
of its arguments in order to produce one element of the output, so it all
works out, but Agda does not understand this on its own. In order to make
that pass the productivity checker, you can use sized types which are
exactly a way to state things like "this function needs to look at at most
one element of the input to produce one element of the output". You can
probably find papers of Andreas about sized types and coinduction.

Best,
Guillaume

On Tue, Mar 14, 2017 at 2:59 PM, Noam Zeilberger <noam.zeilberger at gmail.com>
wrote:

> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170314/829421ec/attachment.html>