[Agda] red background when trying to define the Fibonacci sequence

[Daniel Peebles]

Unfortunately, (to the best of my knowledge) it's not trivial. Agda uses
guarded corecursion, which essentially means that you need recursive calls
to fibonaccis to have data constructors around them. I think the usual
approach to fixing it would be to write an embedded language where zipWith
is a constructor (that takes delayed arguments) and then you'd write an
interpreter that looks at those arguments and calls the real zipWith on
them.

So basically, you'd be constructing an infinite expression that describes
how to compute the fibonaccis, and then interpreting that.

It may be possible to convince agda your fibonaccis is productive by
increasing the termination checker depth, too, but I haven't played with
that with coinduction.

Dan

On Fri, Jan 7, 2011 at 11:47 AM, Wolfgang Jeltsch <
g9ks157k at acme.softbase.org> wrote:

> Hi,
>
> I just tried to define the Fibonacci sequence as follows:
>
>    fibonaccis : Stream ℕ
>    fibonaccis = 0 ∷ ♯ (1 ∷ ♯ zipWith _+_ fibonaccis (tail fibonaccis))
>
> However, the identifier “fibonaccis” gets a red background. How can I
> fix this?
>
> Best wishes,
> Wolfgang
>
>
> _______________________________________________
> 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/20110107/73101670/attachment.html