[Agda] Data.Rational
Andreas Abel
andreas.abel at ifi.lmu.de
Tue Mar 11 20:58:15 CET 2014
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.
--Andreas
On 11.03.2014 17:57, Li Nuo wrote:
> For the efficient problem, what you mentioned is right, but I think
> maybe I didn't make it more precise how this approach works. In fact,
> what we have done is to have both definitions, but for the operations
> for the normal forms (Ra), we define them by lifting from the ones for
> the non-reduced forms(Ra0) via using embedding functions from R -> R0
> and reducing functions from Ra0 -> Ra. In practise it only helps you
> defining functions and proving properties, and you can use the lifted
> operations which will reduce the fractions whenever you do one operation
> on Ra (because every lifted function just computes a non-reduced
> fraction and reduce it).
>
> I hope this explains what I meant before.....
>
> Cheers,
> Nuo
>
>
>
> 2014-03-11 15:29 GMT+00:00 Sergei Meshveliani <mechvel at botik.ru
> <mailto:mechvel at botik.ru>>:
>
> On Tue, 2014-03-11 at 14:28 +0100, Andreas Abel wrote:
> > Such a development would also be welcome for the standard library...
> >
> > On 11.03.2014 11:43, Li Nuo wrote:
> > > Hi,
> > >
> > > I think you can use an alternative approach to make the definition
> > > simpler. You could define the setoid version (namely fractions
> which
> > > doesn't have to be reduced) and use what we call "definable
> quotient
> > > structure" to relate the setoid definition with the normal form
> > > definition (which you can find here
> > > http://www.cs.nott.ac.uk/~txa/publ/defquotients.pdf). Generally
> > > speaking, it contains a set of operations and properties like
> > > normalisation functions (in this case, the fraction-reducing
> functions)
> > > and representative selection functions.
> > >
> > > The advantage of it is to lift functions in a more systematic way,
> > > benefiting from "quotients" without "quotient types". Here in
> this case,
> > > it reduces the complexity of checking coprime property all
> through which
> > > is unnecessary when doing operations on fractions（It is only
> needed if
> > > we want to check whether they are normal form fractions i.e.
> reduced
> > > fractions).
> > > [..]
>
>
> >> Here in this case,
> >> it reduces the complexity of checking coprime property all through
> >> which is unnecessary when doing operations on fractions
>
>
> I do not precisely follow the subject. But I would note for any
> occasion:
>
> if one needs to compute efficiently with fractions, then a good
> tactic is to cancel each fraction to coprime as earlier as possible.
>
> If one does not follow this rule, then computation will remain
> theoretically correct, but for most practicable examples it will become
> somewhat hundreds of times more expensive (the size of intermediate
> denominators in a loop will explode).
>
> This feature does not depend on the choice a programming language or
> programming technique.
>
> As to the below example of ℚ- : ℚ → ℚ,
> its main part is a matter of proving
>
> -- (1)
> lemma : {m d : ℕ} → Coprime ∣ - (+ m) ∣ d → Coprime ∣ (+ m) ∣ d
>
> And I think, it is by applying PropositionalEquality.subst for
> (\x -> Coprime x d)
>
> with using the identity ∣ - x ∣ ≡ ∣ x ∣ for x : ℤ
>
> (for absolute value). This latter identity can be taken from
> Data.Integer.
>
> Probably, the lemmata like (1) need to be in Standard library.
>
> Regards,
>
> ------
> Sergei
>
>
> > >
> > >
> > > 2014-03-11 4:38 GMT+00:00 Amr Sabry <sabry at soic.indiana.edu
> <mailto:sabry at soic.indiana.edu>
> > > <mailto:sabry at soic.indiana.edu <mailto:sabry at soic.indiana.edu>>>:
> > >
> > > Hi,
> > >
> > > I need some decent Rational library and since the current
> Data.Rational
> > > looks like it needs quite a bit of extension, I started
> writing a few
> > > small functions. I am getting stuck very quickly though.
> Here is a small
> > > example that should work:
> > >
> > > -- unary negation
> > > ℚ- : ℚ → ℚ
> > > ℚ- p with ℚ.numerator p | ℚ.denominator-1 p | toWitness
> (ℚ.isCoprime p)
> > > ... | -[1+ n ] | d | c = (+ ℕ.suc n ÷ ℕ.suc d) {fromWitness
> {!!}}
> > > ... | + 0 | d | _ = p
> > > ... | + ℕ.suc n | d | c = (-[1+ n ] ÷ ℕ.suc d) {fromWitness
> {!!}}
> > >
> > > In the first line, c has type:
> > >
> > > c : {i : ℕ} → Σ (i ∣ ℕ.suc n) (λ x → i ∣ ℕ.suc d) → i ≡ 1
> > >
> > > The goal is:
> > >
> > > ?0 : Coprime (ℕ.suc n) (ℕ.suc d)
> > >
> > > where Coprime is defined in Data.Nat.Coprimality as:
> > >
> > > Coprime m n = ∀ {i} → (i ∣ m) × (i ∣ n) → (i ≡ 1)
> > >
> > > As far as I can see, the type of the goal expands directly
> to the type
> > > of c and in fact, "giving" c to the hole works but then the
> file doesn't
> > > reload after that?
> > >
> > > Any suggestions? --Amr
> > >
> > > _______________________________________________
> > > Agda mailing list
> > > Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
> <mailto:Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>>
> > > https://lists.chalmers.se/mailman/listinfo/agda
> > >
> > >
> > >
> > >
> > > _______________________________________________
> > > Agda mailing list
> > > Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
> > > https://lists.chalmers.se/mailman/listinfo/agda
> > >
> >
> >
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
--
Andreas Abel <>< Du bist der geliebte Mensch.
Depeartment of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden
andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/
More information about the Agda
mailing list