[Agda] practical integer/rational arithmetic?

[Daniel Peebles]

I've actually been working on rationals just recently, but the code is a
bit of a mess. I take more or less the same approach as the std lib,
though, but I use an irrelevant coprimality proof. I do prefer to keep the
rationals in reduced form to be able to use propositional equality instead
of a custom equivalence.

I haven't considered using the FFI, but using James Deikun's new Fast
natural arithmetic (including a new fast GCD implementation) we can
actually get reasonable performance out my code, even during compile-time
normalization. James can probably give you more details on that.

I've mostly focussed on non-negative rationals so far, so most of the
reasonable code is in
https://github.com/copumpkin/rational/blob/master/Rational/Nonnegative.agda.
The Rational.agda module is somewhat bitrotted.

I apologize that the code is a mess, but I've been distracted by other
things recently and haven't had a chance to continue it or tidy it up.

Dan

On Wed, May 9, 2012 at 11:06 AM, Noam Zeilberger
<noam.zeilberger at gmail.com>wrote:

> Does anyone have experience writing Agda code involving some
> non-trivial computation on the integers/rationals?  I'm writing some
> code where the goal is not formalization of arithmetic per se, but
> where I would like to be able to actually run some computations which
> might require, e.g., addition-multiplication-division of six-digit
> numbers.  I think I would be happy if there were a way to defer all
> these calculations to Haskell's builtin exact rational arithmetic and
> then reason axiomatically...which seems to be what the foreign
> function interface would provide, except that if I understand
> correctly (http://wiki.portal.chalmers.se/agda/agda.php?n=Docs.FFI) it
> only works with the Alonzo/MAlonzo backends, and not in interactive
> mode.  Ideally, I would like to be able to run arithmetic computations
> interactively, see their results, *and* have Agda verify that the
> results have a particular normal form.
>
> For now I'm using the standard library implementations of Data.Nat and
> Data.Integer with a slightly modified Data.Rational (which does not
> keep rationals in reduced form, to make it easier to do computations),
> but this seems to be unworkably slow even on small examples.  For
> example, computing the gcd (Data.Nat.Gcd) of 2012 and 1984 takes about
> three and a half minutes on my laptop.
>
> Noam
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120509/cf948fa5/attachment.html