[Agda] Data.Rational

[Noam Zeilberger]

For what it's worth (which granted is not much given my limited
experience), the performance issues I ran into really had more to do with
Agda in general than with a specific strategy for rationals (hence my
eventual approach of giving up and calling the FFI).  In particular,
Euclid's algorithm was taking an absurdly long time to run, apparently
because of Agda's call-by-name evaluation strategy (see
https://lists.chalmers.se/pipermail/agda/2012/003988.html, as well as
https://code.google.com/p/agda/issues/detail?id=426).

Noam


On Wed, Mar 12, 2014 at 2:04 PM, Sergei Meshveliani <mechvel at botik.ru>wrote:

> On Wed, 2014-03-12 at 16:37 +0400, Sergei Meshveliani wrote:
> > On Tue, 2014-03-11 at 20:58 +0100, Andreas Abel wrote:
> >
> > > I have no personal experience, but I listened to a talk by Anders
> > > M"ortberg who presented his joint work with Cyril Cohen. He said that
> > > if you want to be efficient you should *not* try to cancel the common
> > > primfactors in fractions each time.  The cost of making things
> > > coprime repeatedly seems to be higher than computing with larger
> > > integers.
> >
> > My experience is very different.
> >
> > [..]
>
>
> If one computes   m/n + m'/n'   for large random integers  m,n,m',n',
> than it is better to delay cancelling by  gcd.
> Because the average gcd for two large random integers occurs small.
>
> Due to this consideration, I had once (in about 1990) an illusion of
> that the (Delay) approach is good.
>
> But in most practical computation methods, the current  m  and  n  are
> not random, they are somehow accumulated from some root in a long loop.
>
> This is why (C) occurs more practicable than (Delay).
> I cannot prove this, I only provide practical examples and
> considerations in my previous letter.
>
> Just follow  D.Knuth:  in   m/n + m'/n'
>
> the first step is to find  gcd n n' ...
>
> Regards,
>
> ------
> Sergei
>
>
> > 1. GHC Rational
> > ---------------
> > As I recall, I tried this in earlier GHC versions (in 1990-ies)
> >
> >    sumF n =  1 + 1/2 + 1/3 + ... + 1/n,   with taking large  n
> >
> > [..]
>
>
> _______________________________________________
> 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/20140312/913b88c8/attachment.html