[Agda] Nat arithmetic properties

[Ulf Norell]

Right, sure. I'd still argue that if you are worried about trust, then
between
the Agda type checker, the Agda to Haskell compiler, the Haskell compiler,
and the implementation of Haskell Integer arithmetic, I trust the Integer
arithmetic the most, by several orders of magnitude.

If you want to experiment with this approach, however, you can implement
macro digits using the normal Agda natural numbers for now and swap them
out later if (when?) we add builtin machine integers.

/ Ulf

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

> On Wed, 2016-09-21 at 14:34 +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).
> >
>
> I do not understand this argument. Let me describe some details.
>
> I expect that a macrodigit is about a half of a  machine word.
> For example, for a 64 bit machine, a macrodigit is (probably) 31 bit,
> and it is represented as  Int  (small integer) in Haskell
> (something of this sort, I do not know details).
> And  Integer  is probably represented in GHC implementation as a list
> (array?) of macrodigits.
>
> Currently the Agda library postulates certain properties of complex
> arithmetical programs in GHC, written (probably) in C, that process
> lists (arrays?) of macrodigits.
> Right?
>
> And I suggest for Agda: to postulte only the properties of a few
> operations on Macrodigit. For example:
> _+m_ is commutative on Integer/M  (Integer modulo M), where M = 2^31.
> And _+m_ is done by a hardware, by a single processor instruction, it
> has not any program structure, in any language. So it cannot be
> subjected to a proof.
> So, postulated are only a few properties of a few hardware operations.
> And all the complex C programs for arithmetic on Integer to be replaced
> with Agda programs (in Agda library) processing lists of macrodigits,
> and also being accompanied with proofs.
>
> So, a larger part is made explicit for Agda and proved, and a smaller
> part remains postulated.
>
> ?
>
> ------
> Sergei
>
>
> >
> >
> > 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/c4fa94de/attachment.html