[Agda] Nat arithmetic properties

Sergei Meshveliani mechvel at botik.ru
Wed Sep 21 16:34:51 CEST 2016


On Wed, 2016-09-21 at 16:26 +0200, Ulf Norell wrote:
> 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.
> 


Well, I also do.




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

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




More information about the Agda mailing list