<div dir="ltr">Hi Noam,<div><br></div><div>Here is my understanding of the situation.</div><div><br></div><div>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.</div><div>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).</div><div><br></div><div>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.</div><div><br></div><div>Best,</div><div>Guillaume</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Mar 14, 2017 at 2:59 PM, Noam Zeilberger <span dir="ltr"><<a href="mailto:noam.zeilberger@gmail.com" target="_blank">noam.zeilberger@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hello Agda List,<br>
<br>
This might be a FAQ, but I was wondering why the canonical<br>
implementation of the stream of Fibonacci numbers using copatterns<br>
does not pass Agda's termination checker? By "canonical<br>
implementation" (cf. section 2.3 of<br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/popl13.pdf" rel="noreferrer" target="_blank">http://www2.tcs.ifi.lmu.de/~<wbr>abel/popl13.pdf</a>), I mean the following:<br>
<br>
====<br>
open import Agda.Builtin.Nat public<br>
<br>
record Stream (A : Set) : Set where<br>
  coinductive<br>
  field<br>
    hd : A<br>
    tl : Stream A<br>
open Stream<br>
<br>
zipWith : {A B C : Set} → (A → B → C) → Stream A → Stream B → Stream C<br>
hd (zipWith f xs ys) = f (hd xs) (hd ys)<br>
tl (zipWith f xs ys) = zipWith f (tl xs) (tl ys)<br>
<br>
fib : Stream Nat<br>
hd fib = 0<br>
hd (tl fib) = 1<br>
tl (tl fib) = zipWith _+_ fib (tl fib)<br>
====<br>
<br>
which yields the following warning:<br>
====<br>
Termination checking failed for the following functions:<br>
  fib<br>
Problematic calls:<br>
  fib<br>
    (at .../Fib.agda:19,27-30)<br>
  tl fib<br>
    (at .../Fib.agda:19,35-38)<br>
====<br>
<br>
Any hints as to why Agda is complaining?<br>
<br>
Noam<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</blockquote></div><br></div>