Sergei Meshveliani

2018-01-13 15:25:57 UTC

Announcement

------------

Binary-3.0 -- a Pure Binary Natural Number Arithmetic library

for Agda

is available on

ftp://ftp.botik.ru/pub/local/Mechveliani/binNat/

(see license.txt and the manual README.agda in the archive).

Binary-3.0 is a pure, regular-performance, complete, and certified

binary arithmetic for natural numbers

written in Agda.

It has been tested under Agda 2.5.3, MAlonzo, lib-0.14.

It is also suggested as a replacement for the Bin part in

Standard library lib-0.14

(the modules Data.Bin.agda, Data.Bin.Properties.agda).

`Pure'

means that Binary-3.0 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-3.0 has a regular performance

cost order -- the one expected for the corresponding known naive

operations with bit lists.

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 is implemented as a

loop

of {s = shift n dr for certain n; dd := dd -. s} repeated O(|x|)

times.

So that it 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.

* DecTotalOrder instance for Bin,

for x <= y defined on Bin as x < y or x == y.

* StrictTotalOrder instance for Bin, _<_.

* The bijection property for the map pair toNat, fromNat.

* Subtraction _-._ on Bin, with the needed 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.

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

Usage of Standard library lib-0.14

-----------------------------------

Bin0.agda _copies_ the following items from Data.Bin of Standard

lib-0.14:

Bin⁺, data Bin, 2^_, toBits, ⌊log₂_⌋, _*2,

_*2+1, ⌊_/2⌋, Carry, addBits, addCarry, _+_,

_*_, fromBits, addBitList,

The last three have a slight change in implementation.

Nothing else about Bin is taken from Standard lib-0.14.

The definition for inequalities on Bin is totally changed in Bin0, Bin1.

More detailed explanations are given in README.agda.

Binary-3.0 has been tested under Agda 2.5.3,

and it relies on Standard library lib-0.14.

It also includes the module LtReasoning.agda -- a support for

inequality reasoning by Ulf Norell.

Installation:

agda -c $agdaLibOpt GCDTest.agda

Comments and improvements are welcome.

---------------------

Sergei D. Meshveliani

***@botik.ru

------------

Binary-3.0 -- a Pure Binary Natural Number Arithmetic library

for Agda

is available on

ftp://ftp.botik.ru/pub/local/Mechveliani/binNat/

(see license.txt and the manual README.agda in the archive).

Binary-3.0 is a pure, regular-performance, complete, and certified

binary arithmetic for natural numbers

written in Agda.

It has been tested under Agda 2.5.3, MAlonzo, lib-0.14.

It is also suggested as a replacement for the Bin part in

Standard library lib-0.14

(the modules Data.Bin.agda, Data.Bin.Properties.agda).

`Pure'

means that Binary-3.0 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-3.0 has a regular performance

cost order -- the one expected for the corresponding known naive

operations with bit lists.

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 is implemented as a

loop

of {s = shift n dr for certain n; dd := dd -. s} repeated O(|x|)

times.

So that it 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.

* DecTotalOrder instance for Bin,

for x <= y defined on Bin as x < y or x == y.

* StrictTotalOrder instance for Bin, _<_.

* The bijection property for the map pair toNat, fromNat.

* Subtraction _-._ on Bin, with the needed 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.

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

Usage of Standard library lib-0.14

-----------------------------------

Bin0.agda _copies_ the following items from Data.Bin of Standard

lib-0.14:

Bin⁺, data Bin, 2^_, toBits, ⌊log₂_⌋, _*2,

_*2+1, ⌊_/2⌋, Carry, addBits, addCarry, _+_,

_*_, fromBits, addBitList,

The last three have a slight change in implementation.

Nothing else about Bin is taken from Standard lib-0.14.

The definition for inequalities on Bin is totally changed in Bin0, Bin1.

More detailed explanations are given in README.agda.

Binary-3.0 has been tested under Agda 2.5.3,

and it relies on Standard library lib-0.14.

It also includes the module LtReasoning.agda -- a support for

inequality reasoning by Ulf Norell.

Installation:

agda -c $agdaLibOpt GCDTest.agda

Comments and improvements are welcome.

---------------------

Sergei D. Meshveliani

***@botik.ru