[Agda] Nat arithmetic properties

[Ulf Norell]

The one in the standard library is very slow, but if you're willing to use
'erase' [1] you
can implement a fast one that just needs a call to the builtin boolean
equality on nats.
See the agda-prelude library for an implementation [2].

/ Ulf

[1]
https://github.com/agda/agda-stdlib/blob/e3893da/src/Relation/Binary/PropositionalEquality/TrustMe.agda#L25-L26
[2]
https://github.com/UlfNorell/agda-prelude/blob/48d1b8e8/src/Prelude/Nat.agda#L67-L70

On Thu, Sep 22, 2016 at 10:16 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> And how much does it cost  m ≟ n
> for Nat ?
>
>
> On Fri, 2016-09-23 at 00:08 +0400, Sergei Meshveliani wrote:
> > Another reason for necessity of n-ary provable arithmetic:
> >
> >   _≤?_  of Data.Nat.decTotalOrder  is slow.
> >
> > Probably this is because it is not built-in
> > (and how can it? assuming that the result may contain a proof made of
> > many certain constructors).
> >
> > This leads, for example, to that sorting of the list  [10000 ... 1]  is
> > done many times faster when the numbers are binary-coded
> > (and it is applied _≤?_ of DecTotalOrder for Bin).
> >
> > ------
> > Sergei
> >
> >
> >
> > On Thu, 2016-09-22 at 22:30 +0400, Sergei Meshveliani wrote:
> > > On Thu, 2016-09-22 at 12:38 -0400, Wolfram Kahl wrote:
> > > > Sergei,
> > > >
> > > > On Wed, Sep 21, 2016 at 02:34:28PM +0200, Ulf Norell wrote:
> > > > > How is this better than what we do at the moment? It seems to me
> that
> > > > > your postulated properties of the macro digit operations are going
> to be
> > > > > more
> > > > > complicated than what we postulate right now (namely that Haskell
> Integer
> > > > > arithmetic implement the expected functions on natural numbers).
> > > >
> > > > Indeed.
> > > >
> > > > One possibly interesting avenue to expore in this direction,
> > > > and requiring no modification of Agda, would be starting from the
> fact
> > > > that GHC supports two implementations of Haskell Integer:
> > > >
> > > >  * The default implementation calls the GPL-licenced GMP library via
> the FFI
> > > >
> > > >  * An alternative implementation (called SimpleInteger?)
> > > >    for GPL-averse contexts is, if I remember correctly, implemented
> in Haskell.
> > > >    (So that would be some kind of lists of Macrodigits already.)
> > > >
> > > > You could go and implement your lists of Macrodigits in Agda, and
> > > > use Agda's reverse FFI to export this to Haskell to replace
> SimpleInteger.
> > > >
> > > > And try to be faster! ;-)
> > >
> > >
> > > 1) In principle:  Agda Standard library needs a proved arithmetic for
> > > Nat which is several times faster that the existing one of Data.Bin.
> > >
> > > 2) For example, Bin._+_ is  2^n times  faster than Nat._+_ (unary),
> > > and can be supplied with all the necessary proofs
> > > (mainly: a proof for that the ring of Nat is isomorphic to the ring of
> > > Bin, this is enough).
> > >
> > > 3) Further, _+_ for the  Hexa -coded naturals is can be programmed in
> > > Agda, so that it will be several times faster than Bin._+_, and will be
> > > supplied with the proof for that the ring of Nat is isomorphic to the
> > > ring of Hexa).
> > > And this does not need any built-ins (no postulates) for digits.
> > > But it will be about 8 times slower than Integer._+_ in GHC
> > > (because 4-Hexa-digit numbers are summed by one macrodigit operation in
> > > GHC, and because a digit operation in Hexa in Agda is not in one step).
> > >
> > > 4) As to doing the same for lists of large macrodigits (say 64 bit
> > > digit), there it will have sense to make the digit operations built-in
> > > (with several postulated properties) an all the rest written in Agda,
> > > with proofs.
> > >
> > >
> > > But  I am not currently going to implement any of these things.
> > > These are only my notes, comments.
> > >
> > > []
> >
> >
> >
> >
>
>
> _______________________________________________
> 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/20160922/25be26fa/attachment.html