[Agda] Nat arithmetic properties

[Sergei Meshveliani]

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