[Agda] practical integer/rational arithmetic?

James Deikun james at place.org
Wed May 9 17:57:40 CEST 2012

On Wed, 2012-05-09 at 11:37 -0400, Daniel Peebles wrote:
> 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

A computation like that should really be more like the aforementioned
0.015 seconds than 5 seconds, but I haven't been able to prevent
call-by-name evaluation from making the extended Euclid's algorithm
exponential in its recursion depth.  (At least it's no longer
exponential in anything else.)  Rather than continue trying to
micromanage evaluation for these particular functions, I decided to
focus my efforts on improving Agda's evaluation strategy in general, so
that's probably the next improvement that will appear.

More information about the Agda mailing list