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

[Andreas Abel]

On 1/7/11 5:57 PM, Daniel Peebles wrote:
> 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.

No, increasing the depth does not help, since guardedness is destroyed 
by zipWith.

MiniAgda can track that zipWith preserved guardedness, so you can define 
fibonaccis more or less like you wanted.

sized data SNat : Size -> Set
{ zero : [i : Size] -> SNat ($ i)
; succ : [i : Size] -> SNat i -> SNat ($ i)
}

let Nat : Set = SNat #

fun add : Nat -> Nat -> Nat
{ add (zero .#)   = \ y -> y
; add (succ .# x) = \ y -> succ # (add x y)
}

sized codata Stream ++(A : Set) : Size -> Set
{ cons : [i : Size] -> (head : A) -> (tail : Stream A i) -> Stream A ($ i)
}
fields head, tail

cofun zipWith : [A : Set] -> [B : Set] -> [C : Set] ->
                 (A -> B -> C) -> [i : Size] ->
		Stream A i -> Stream B i -> Stream C i
{
   zipWith A B C f ($ i) (cons .A .i a as) (cons .B .i b bs) =
	cons C i (f a b)  (zipWith A B C f i as bs)
}

let n0 : Nat = zero #
let n1 : Nat = succ # n0

cofun fib : [i : Size] -> Stream Nat i
{
   fib ($ i) = cons Nat i n0 (zipWith Nat Nat Nat add i
     (cons Nat i n1 (fib i)) (fib i))
}

> On Fri, Jan 7, 2011 at 11:47 AM, Wolfgang Jeltsch
> <g9ks157k at acme.softbase.org <mailto: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

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/