[Agda] GCD in future standard library

[mechvel at scico.botik.ru]

Dear standard library developers,

this is on developing the algebra part of the standard library.

In the _master_ library branch, we come now to treating GCD for the new 
Bin representation.
And this touches the question of possible generic GCD notion.
The two approaches are possible, and I need to agree on this point.

First, consider the GCD notion itself, without relating it to the 
computation method.

In the current _master_ library there are the three very similar numeric 
domains:

                         ℕ, Bin, ℤ.

ℕ is isomorphic to Bin, and most methods for ℤ are reduced to those for 
ℕ in a simple way, without loss of efficiency.
I think, also  ℤb  needs to join -- binary represented integers.

For most algorithms, we cannot use the toℕ/fromℕ isomorphism to compute 
things on Bin (for example, divMod, gcd).
Because this isomorphism is expensive to compute relatively to the 
method itself (even by using certain built-in primitives).

The approach of lib-1.1 is as follows.
* There are declared the two _notions_ of GCD:  for ℕ and for ℤ,
   and there needs to appear the third GCD notion -- for Bin.
* There is no provision for the GCD notion for other domains, for 
example, for polynomials over a domain with gcd.

This design does not look natural.

We need now to choice between the two approaches.


I. To continue the lib-1.1 design:
    to declare one more GCD notion -- Bin.GCD, and to compute Bin.gcd by 
using  Bin.divMod.


II. A generic approach, which I suggest.

1) To add to  Algebra.agda  the declaration of a cancellative semiring:

record CancellativeSemiring α ℓ :  Set _
   where
   field  CommutativeSemiring : CommutativeSemiring α ℓ
   ...
   field  _≟_       : Decidable _≈_
          lnzCancel : LeftNZCancellative

LeftNZCancellative means the Cancellative property already defined in 
the _master_ library, only it adds the
condition x ≉ 0# for the element being cancelled.

2) The GCD notion is defined in the module parameterized by  R : 
CancellativeSemiring _ _:

   record GCD (a b : Carrier) :  Set _   -- a result of gcd
     where
     constructor gcd′
     field  proper   : Carrier           -- proper gcd value
            divides₁ : proper ∣ a
            divides₂ : proper ∣ b
            greatest : ∀ {d} → (d ∣ a) → (d ∣ b) → (d ∣ proper)

It is similar to the definitions existing in lib-1.1, only it is 
generic.
Also in this module are declared the general notions of
                                                      IsPrime, Coprime.
All this is expressed very simply.

3) The domains ℕ, ℤ, Bin are already actually provided in the _master_ 
lib with the instances of CancellativeSemiring,
    because the cancellation law by nonzero is already implemented there 
for these domains.
Hence the above GCD declaration becomes type-checked and ready to work, 
and it will replace the three special GCD declarations in the _master_ 
lib. Also it is ready to work in many other domains.


4) About computation of GCD.

Assume that we have chosen the above generic notion of GCD.

For ℕ, ℤ, Bin, ℤb there is known a simple method which is also 
reasonably efficient: an Euclidean algorithm.
This method is also applicable to all Euclidean domains.

For the multivariate polynomial domain R[x1..xn] for a GCD-domain R, the 
Euclidean method is not correct. But
* the above generic notion of GCD is valid there,
* CA libraries apply several more complex methods that have a reasonable 
efficiency.

Now, consider GCD computing only for ℕ, ℤ, Bin, and other Euclidean 
domains.
The standard library _needs_ to implement at least the first tree.

Integer.gcd  can be trivially reduced to computing Nat.GCD.gcd, probably 
this is done so in lib-1.1 (is it?).
Bin.GCD.gcd has to be implemented separately, because the conversion ℕ 
<--> Bin is expensive.

For ℕ and Bin, we need to define the notion(s) of DivMod (division with 
remainder), to implement the algorithm(s) of divMod, and implement GCD 
by applying divMod in recursion.

We need to choose between the two approaches.

4.1. Declare the DivMod notion separately for ℕ and Bin.
      Also the library needs DivMod for ℤ, independently on computing 
GCD.
So, we shall have the three declared notions of DivMod, the two 
algorithms for the divMod implementation, and the two implementations of 
GCD.

4.2. In the environment of CancellativeSemiring described above to 
introduce a general notion

   record EuclideanSemiring _ where
     C = Carrier
     field norm : Norm

     open Norm norm
     field
       divMod    : C → (y : C) → y ≉ 0# → C × C
       divModEq< : (a b : C) → (nzb : b ≉ 0#) →
                               let (q , r) = divMod a b nzb
                               in
                               a ≈ (q * b) + r  ×
                               ((nzr : r ≉ 0#) → ∣ r ,, nzr ∣ < ∣ b ,, 
nzb ∣)

A _norm_
          ∣_,,_∣ :  (x : C) → x ≉ 0# → ℕ
is a certain operation on nonzero elements (with a couple of certain 
declared laws). Examples:
For ℕ it can be set identic,
for ℤ it can be set absolute value,
for the univariate polynomial domain it can be set the _degree_.

This is a generic notion of DivMod. It covers the instances of ℕ, ℤ, 
Bin, ℤb, univariate polynomial domain over any field, Gaussian integers, 
and some others.
It also makes it easy to provide a common gcd  implementation for all 
these domains.

In textbooks, they define _Euclidean domain_ for this purpose.
But unfortunately this requires to inherit a Ring. And this does not 
cover the case of ℕ, because ℕ is not of Ring.

Therefore I suggest a slight generalization: the above 
EuclideanSemiring.

But there are needed the four additional axioms in EuclideanSemiring 
which are not in textbooks. They are specific to Agda: congruence of 
norm and of quotient, and irrelevance on the proof for x ≉ 0# for norm 
and quotient.


Summing up all the above, I suggest the following steps in developing 
the library.

1. To declare the generic divisibility notion _∣_ for Magma (this is 
simple).
    To implement the generic GCD notion for a CancellativeSemiring, as 
above.
    To remove the existing special definitions for divisibility and GCD.

2. To have the three special definitions Nat.DivMod.DivMod, 
Integer.DivMod.DivMod, Bin.DivMod.DivMod,
    and the two different implementations for the corresponding  divMod,
    the two different implementations for the corresponding  gcd.

3. After this is settled, to decide whether to change to the above 
EuclideanSemiring and thus to arrange a common
    implementation for GCD for ℕ, ℤ, Bin, ℤb, and other domains of  
EuclideanSemiring.

The first two points are verified, they are presented by a tested 
workable code, which is also simple.
The generic branch in the third point can be verified later, if we 
decide to try it (currently I doubt about keeping the code simple).

Please, consider the suggestion.

Regards,

------
Sergei