[Agda] practical integer/rational arithmetic?

[Daniel Peebles]

Granted, Maple doesn't need to compute a witness of GCD-ness along the way
:)

I think James's new witness-carrying GCD takes about 5 seconds to normalize
the GCD of 14303480934 and 44934319042, which seems pretty respectable. If
you want to see the code, it's at
https://github.com/xplat/potpourri/tree/master/Fast

Dan

On Wed, May 9, 2012 at 11:28 AM, Jacques Carette <carette at mcmaster.ca>wrote:

> 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<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.
>
> ______________________________**_________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/**mailman/listinfo/agda<https://lists.chalmers.se/mailman/listinfo/agda>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120509/31ba00d9/attachment-0001.html