Hi Thorsten,
Thanks for the reply, and the links to documentation. Some of them I
have and some I don't. Lots of code examples are nice.
On 14/11/2005, at 11:17 PM, Thorsten Altenkirch wrote:
Hi Neil,
good to see that you are trying out Epigram.
I'm having a lot of fun...and trying out slightly silly things to see
what I understand and what I don't and to see what breaks, and what
doesn't.
I am not sure whether I understand your questions properly, but
here are some comments...
There is no need to define "fibber" because structural recursion is
built-in into Epigram, actually the elaborator translates
structural recursion into uses of standard elimination constants.
Is there documentation on exactly what the elimination constants are?
Epigram was happy with an Ackermann function, which surprised me
slightly.
That is you can just write
-----------------------------------------------------------
( n : Nat !
let !-------------!
! fib n : Nat )
fib n <= rec n
{ fib n <= case n
{ fib zero => zero
fib (suc n) <= case n
{ fib (suc zero) => one
fib (suc (suc n)) => add (fib n) (fib (suc n))
}
}
}
-----------------------------------------------------------
and let Epigram do all the fibbing...
At exponential cost, of course!
But to address your program:
( n : Nat !
let !-------------!
! fib n : Nat )
fib n <= case (fibber n (pair (succ zero) zero))
{ fib n => a
}
I am not sure why Epigram actually allows you to do this, it should
be an error.
Is the problem really with the use of case? It makes sense to me, and
although I can define split, or some other auxiliary function, it
seems a pity that I can't remove the detour. Looking at what Horace
was telling me it looks like the information was all there, just that
the name `a' had leaked out of scope. But I have no idea what is
going on internally, so this may be misguided.
Case is a program refinement tactic, not a program language
construct and it only works well for variables, not for expressions
(like "fibber ..."). What you want to use here is called the "with"
rule, which is not yet implemented - see "The view from the left"
http://www.e-pig.org/downloads/view.pdf
There are a number of work-arounds (e.g. define projections or use
an auxilliary function)... But at least in the fib case it turns
out not to be necessary.
Best wishes,
Neil
Cheers,
Thorsten
--
Dr. Thorsten Altenkirch phone : (+44) (0)115 84 66516
Lecturer http://www.cs.nott.ac.uk/~txa/
School of Computer Science & IT University of Nottingham
This message has been checked for viruses but the contents of an
attachment
may still contain software viruses, which could damage your
computer system:
you are advised to perform your own checks. Email communications
with the
University of Nottingham may be monitored as permitted by UK
legislation.
School of Mathematics, Statistics and Computer Science &
Centre for Logic, Language and Computation
Victoria University
P. O. Box 600
Wellington Tel +64 4 463 6732
New Zealand mailto:[EMAIL PROTECTED]
What you see is what you see
Frank Stella
