[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