[Agda] Nat arithmetic properties

[Sergei Meshveliani]

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.
> > 
> > []
> 
> 
> 
>