[Agda] practical integer/rational arithmetic?

[Jacques Carette]

On 09/05/2012 11:06 AM, Noam Zeilberger wrote:
> For
> example, computing the gcd (Data.Nat.Gcd) of 2012 and 1984 takes about
> three and a half minutes on my laptop.

I can't help you with how to make Agda faster, but I can at least show 
you what the bar ought to be.  In Maple, on a 3 year old machine, 
computing   gcd(3!!!^5, 2^26892+1)  [which is 1446241] takes 0.015 
seconds.  3!!!^5 (3 factorial factorial factorial to the 5th) is a 8732 
decimal digits number, while 2^26892+1 is a 17125 digit number.

To get into the 3 1/2 minutes ballpark, one has to go to millions of digits.

<shameless plug> The CICM conference 
(http://www.informatik.uni-bremen.de/cicm2012/cicm.php) in Bremen hosts 
a lot of people whose aim is to combine correctness [via theorem 
proving] and efficient computation [via computer algebra].  Programming 
Languages are, unfortunately, sorely under-represented.  Please help us! 
</shameless plug>

Jacques

PS: Mathematica and SAGE (via PARI) would be just as fast for these 
computations, I just happen to be most comfortable with Maple.