[Agda] Data.Rational

[Li Nuo]

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>:

> 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>>:
> > >
> > >     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>
> > >     https://lists.chalmers.se/mailman/listinfo/agda
> > >
> > >
> > >
> > >
> > > _______________________________________________
> > > Agda mailing list
> > > Agda at lists.chalmers.se
> > > https://lists.chalmers.se/mailman/listinfo/agda
> > >
> >
> >
>
>
> _______________________________________________
> 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/20140311/ecf577a8/attachment-0001.html