[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