[Agda] productivity of fibonacci stream

[Noam Zeilberger]

Thank you, Guillaume, for the explanation, and thank you Adam for the
example code using sized types -- both are very clear!

Noam

On Tue, Mar 14, 2017 at 8:34 PM, Guillaume Brunerie
<guillaume.brunerie at gmail.com> wrote:
> 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
>
>