Binary-4 -- a Pure Binary Natural Number Arithmetic library for Agda
is available here on GitHub, and on
http://www.botik.ru/pub/local/Mechveliani/binNat/,
Binary-4 is a pure, regular-performance, complete, and certified binary arithmetic for natural numbers written in Agda.
It has been tested under Agda 2.5.4, MAlonzo, ghc-7.10.2.
It is also suggested as a replacement for the Bin part in Standard library lib-0.16 (the modules Data.Bin.agda, Data.Bin.Properties.agda).
-
The library of 2013 by Arseniy Alekseyev:
It seems to have all the needed functionality and proofs. Only the code. It uses different representation, different algorithms.
-
The library by Martin Escardo of 2016:
(only I do not see there divMod and gcd operations).
-
It has simpler proofs and simpler algorithms,
-
It has a faster divMod operation in the case of small divisor values (this matter has been pointed out by Arseniy Alekseyev).
-
It is used a different representation for Bin:
data Bin : Set where
0# : Bin 2suc : Bin -> Bin -- \n-> 2*(1+n) arbitrary nonzero even suc2* : Bin -> Bin -- \n-> 1 + 2n arbitrary odd -
< on Bin is defined defined by mapping to Nat (similar as in Standard library).
-
It is used a WellFounded recursion on Bin for termination proof for the functiond divMod and gcd.
`Pure'
means that Binary-4 never uses a built-in arithmetic (on Nat) to
essentially change performance.
The performance order is supposed to remain with replacing the Nat
arithmetic with the naive unary arithmetic.
`Regular performance' means that the arithmetic on Bin of Binary-4 has a regular performance cost order -- the one expected for the corresponding known naive operations with bit lists. At least this holds for <-cmp, +, -., *, divMod, gcd. Examples:
-
The comparison <-cmp x y on Bin costs O(|x| + |y|),
where |z| = bitLength z. -
Division with remainder divMod x y y/=0 on Bin costs O( |x|^2 ).
`Complete'
means that all the items are implemented that are usually required for
standard arithmetic. There are provided the following items.
- < and <= are defined by mapping to Nat,
- DecTotalOrder instance for <= on Bin,
- StrictTotalOrder instance for < on Bin,
- The bijection property for the map pair toNat, fromNat.
- Subtraction -. on Bin, with the main properties proved.
- The proofs for isomorphism for +, *, -. for toNat, fromNat.
- The monotonicity proofs for toNat, fromNat for <= and Nat.<=. A similar monotonicity for < and Nat.<= are proved.
- Various kinds of monotonicity for +, *, -. for <= and <
are proved. - The CommutativeSemiring instance for Bin.
- Binary logarithm for Bin, with its main properties proved.
- Division with remainder and GCD for Bin.
- The demonstration/test programs for divMod and gcd.
`Certified' means that everything is proved in Agda which is regularly required of the above operations.
Binary-4 has been tested under Agda 2.5.4, MAlozo, ghc-7.10.2.
It also includes the module LtReasoning.agda -- a support for inequality reasoning by Ulf Norell.
Installation:
agda -c $agdaLibOpt GCDTest.agda
Performance tests:
LogarithmTest.agda, DivModTest.agda, GCDTest.agda ("readme"-s are included).
Comments and improvements are welcome.
Sergei D. Meshveliani mechvel@botik.ru