[Agda] practical integer/rational arithmetic?

Jacques Carette carette at mcmaster.ca
Wed May 9 18:00:27 CEST 2012


On 09/05/2012 11:55 AM, Nils Anders Danielsson wrote:
> On 2012-05-09 17:28, Jacques Carette wrote:
>> 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.
>
> In GHCi, on an older machine:
>
>   Prelude> let fac n = product [1..n] in gcd (fac (fac (fac 3)) ^ 5) 
> (2^26892 + 1)
>   1774001
>   (0.10 secs, 39859272 bytes)
>
> I wonder why the results are different.

Because I made a mistake in my cut-and-paste.  GHCi is correct.

To Daniel:
 > time(igcdex(3!!!^5, 2^26892+1, 's', 't'));
                                     0.109

So that is 10 times slower, but I do get a "certificate", i.e. the 2 
co-factors for the diophantine equation from that.

Jacques



More information about the Agda mailing list