[Epigram] epigram tells me fibs

[neil]

Hi All,






     ( A : * ;  B : A -> * !        (   a : A ;  b : B a   !
data !---------------------!  where !----------------------!
     !    Sigma A B : *    )        ! pair a b : Sigma A B )

     (   A, B : *   !
let  !--------------!
     ! Pair A B : * )

     Pair A B => Sigma A (lam x : A => B)




Now we define a little auxiliary function, fibber:


     ( n : Nat ;  p : Pair Nat Nat !
let  !-----------------------------!
     !  fibber n p : Pair Nat Nat  )

     fibber n p <= rec n
     { fibber n p <= case n
       { fibber zero p => p
         fibber (succ n) p <= case p
         { fibber (succ n) (pair a b) => fibber n (pair (plus a b) a)
         }
       }
     }





     (   n : Nat   !
let  !-------------!
     ! fib n : Nat )

     fib n <= case (fibber n (pair (succ zero) zero))
     { fib n => a
     }


And then we check that fib works:


inspect fib (succ (succ (succ (succ (succ (succ (zero)))))))
          =>

           : Nat










a : Nat ;  b : Nat ;  n : Nat

q : pair a b = fibber n (pair (succ zero) zero)
|-
fib n : Nat

Anyhow, I'm confused (and so will my students be).

Cheers,
Neil


Dr Neil Leslie
Director, Centre for Logic, Language and Computation
Victoria University
P. O. Box 600
Wellington                                         Tel +64 4 463 6732
New Zealand                          mailto:[EMAIL PROTECTED]

I'm think of using epigram to teach some dependently typed programming to my 4th year functional programming student next year, so I'm having fun writing and trying to understand little programs just now. Once we have defined Nat, and written plus and fac, we go on to write fib. In order to get a structurally recursive fib we define the Sigma types, and then Pairs: ------------------------------------------------------------------------ ------ ------------------------------------------------------------------------ ------ ------------------------------------------------------------------------ ------ Question 1: is there a better way to make definitions, i.e. is there a built in notion of definitional equality? ------------------------------------------------------------------------ ------ ------------------------------------------------------------------------ ------ and then we define fib itself (letting epigram help us elaborate the definition): ------------------------------------------------------------------------ ------ ------------------------------------------------------------------------ ------ ------------------------------------------------------------------------ ------ succ (succ (succ (succ (succ !!!! ! ! ! !% (succ !!!!! ! ! ! ! !% (succ !!!!!! ! ! ! ! ! !% (succ !!!!!!! ! ! ! ! ! ! !% (succ !!!!!!!! ! ! ! ! ! ! ! !% (succ !!!!!!!!! ! ! ! ! ! ! ! ! !% (succ !!!!!!!!!! ! ! ! ! ! ! ! ! ! !% (succ !!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! !% (succ !!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! !% zero)))))))))))) ------------------------------------------------------------------------ ------ You can check this for yourself because the script is attached. Or rather you can't, because epigram doesn't know any longer what a is when asked to return a value for fib n. So I seem to have a script which I can elaborate interactively and which I can't successfully load. I don't think is desirable. Question 2: Should I have expected this behaviour? Is there some dumb error I have made? For what it is worth, the interesting interaction with *Horace* involves:

fibbing.epi
Description: Binary data