[Agda] Nat arithmetic properties

[Ulf Norell]

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).

/ Ulf

On Wed, Sep 21, 2016 at 2:20 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> On Wed, 2016-09-21 at 12:52 +0200, Ulf Norell wrote:
> >
> > On Wed, Sep 21, 2016 at 11:51 AM, Sergei Meshveliani
> > <mechvel at botik.ru> wrote:
> >         Ulf Norell wrote recently
> >
> >         > [..]
> >         > natural number operations (_+_, _*_ etc) are compiled to the
> >         > corresponding Haskell Integer operations.
> >
> >         But this means that the properties of these operations on Nat
> >         become postulated.
> >         Do they?
> >
> >         For example, the commutativity property  +-comm  of
> >         Data.Nat.Properties.Simple
> >         is proved in this module for Nat represented in unary system
> >         and for the algorithm for _+_
> >         given in Data.Nat.
> >         Now as _+_ is compiled to  +-via-Haskell-Integer,  the proof
> >         for +-comm  is not a proof for
> >         +-via-Haskell-Integer.
> >
> >         Can somebody explain, please?
> >
> >
> > Operationally, the proof of +-comm carries no bits of information, and
> > so can be erased at runtime.
> >
> >
> > If you're concerned about correctness, there is indeed an implicit
> > assumption that the Haskell
> > Integer arithmetic functions are semantically equivalent to the unary
> > natural number functions
> > defined in Agda (and so that the proof of +comm for unary numbers
> > implies +comm for Haskell
> > Integers). I feel pretty confident that this is the case. Certainly
> > more confident than I am in there
> > being no inconsistency bugs in the type checker, for instance.
> >
>
> Being not able to provably verify the type checker
> (and also MAlonzo, GHC, linker, and hardware) does not mean that one
> needs to assume/postulate the properties of all the upper levels. The
> more levels are verified the better
>
> (by the way, one can imagine a provably verified type checker, provably
> verified Agda interpreter ... -- may such have sense?).
>
> Adding proofs to efficient programs for a generic fraction arithmetic,
> polynomial arithmetic, etc, allows it to preserve performance.
> As to natural numbers, the provable part can cover without performance
> loss everything besides macrodigits.
>
> Namely, suppose that we represent Natural as  Nat' = List Macrodigit,
> map Macrodigit to Int of Haskell and make arithmetic operations on
> Macrodigits built-in, postulate several properties of the Macrodidit
> arithmetic, program in Agda arithmetical operations on Nat' by
> processing lists of macrodigits, add the proofs for the properties (like
> say +-comm) for Nat'.
> With this approach the arithmetic in Nat  a) will be fast enough,
> b) the postulated part will be restricted to operations on Macrodigit,
> so that the programs will be more verified.
>
> Has this approach sense?
>
> Regards,
>
> ------
> Sergei
>
>
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160921/aa70b1b0/attachment.html