[Agda] fast DecTotalOrder

[Sergei Meshveliani]

It is done!
Mainly, Agda is all right.

Thanks to Nils and Andrea.

This is  `sort'  of the merge method for any  xs : List A,  
A  of any DecTotalOrder.

It costs  O( n*log(n) ),  and it has proofs for that 
1) the result  ys  is an ordered list,
2) toMS xs =ms toMS ys,

where  toMS  converts a list to its Multiset.
So that this fully agrees with the notion of sorting.

Orderedness is defined as 

 data OrderedList : List C → Set _
   where
   nil    : OrderedList []
   single : (x : C) → OrderedList (x ∷ [])
   prep2  : (x y : C) → (xs : List C) → x ≤ y → OrderedList (y ∷ xs) →
                                                OrderedList (x ∷ y ∷ xs)


A Multiset  M  is defined as a member of  List (C × ℕ),  with the
conditions of that 
  a) the keys do not repeat, 
  b) all multiplicities are positive in ℕ.

The equality  _=ms_  on Multiset is defined as 

   pairs M ⊆ pairs M' ×  pairs M' ⊆ pairs M

(its computation costs O(n^2)).

The performance test forms a certain list  xs  over  Bin  of length
2^e,
where  e  is input from file at run-time.
In  xs  there are  2^(e-1)  different elements.

I define  DecTotalOder  for  Bin  by converting from  StrictTotalOder
for Bin.

There are printed  first 5 of  ys,  last 5 of ys,  and 5 elements from
the middle of  ys
(we must not print large data when measuring time).  

Putting  e = 12, 13, 14, 15, 16  shows that the time looks indeed like
O( l*log(l) ),   l = length xs

(5 seconds for  e = 16  for 2 GHz machine).
 
The condition of  toMS xs =ms toMS ys  is used further in a certain
client function  f  which only returns  "done".
f  uses the existence of this proof, but does not analyze the proof
structure. And this does not add any time cost at run-time.

And if we add printing the result of  toMS xs =ms? toMS ys
("yes" or "no"),
then this becomes  O( l^2 ),  and takes  160 sec  even for  e = 14.

The whole thing has taken of me about 5 months of work:
lists, association lists, algebra of multisets, many lemmata ...
Only full proofs, nothing is skipped.

And it is visible the following.

(a) Providing formal proofs takes a very much effort and time.
   If a method and its informal constructive proof is known, 
then composing a proof takes of me  about  50 - 100 times  longer than  
programming this proper method.

(b) Type check is rather expensive, compilation is rather expensive. 

I hope that (b) can be improved.

As to (a),  I do not expect that there is currently possible a prover
that can really help this on practice. For example:  which prover can
really help composing proofs for this particular library with multisets
and merge sorting?


Regards,

------
Sergei




On Tue, 2015-03-24 at 14:29 +0400, Sergei Meshveliani wrote:
> Can people, please, advise me on the following matter?
> (which is in fact on Standard library)
> 
> For testing the sorting function for performance, I need 
> (1) the list elements to be from some DecTotalOrder instance
>      (required by the `sort' function),
> (2) _≤?_ to perform fast,
> (3) forming a list having as many different elements as needed.
> 
> I am going to do this.
> 
> a) To implement  
>    stoToDTO : StrictTotalOrder _ _ _→ DecTotalOrder _ _ _
>    stoToDTO sto =
>                  record{ Carrier = Carrier
>                        ; _≈_     = _≈_
>                        ; _≤_     = _≤_
>                        ; isDecTotalOrder = isDecTotalOrder }
>    where
>    open StrictTotalOrder sto using (_≈_; _<_; compare ...)
>                     
>    _≤_ : Rel Carrier _
>    x ≤ y =  x < y ⊎ x ≈ y   -- **
>    ...
> 
> I expect that  DecTotalOrder  can be proved for this _≤_ instance.
> Right?
> 
> b) To use  Data.String.StrictTotalOrder,
>    in which  _<_  is by the lexicographic comparison.
>    I expect that this comparison is fast  (O(length string)).
>    Is it? 
> 
> c) To apply  stoToDTO  to  Data.String.StrictTotalOrder  with 
>    obtaining fast  DecTotalOrder  for String.
> 
> d) To implement  suc : String → String  as the lexicographically next
>    string, and to use it for obtaining fast a list  xs : List String
> with many different elements in  xs.
> 
> Is this plan correct? 
> Can the goal be achieved in a simpler way?
> 
> First I thought of  Bin,  but then discovered that  _<_  is done there
> by conversion to  Nat,  which is very expensive. 
> Right?
> So, I hope for  Data.String.StrictTotalOrder.
> 
> Who could advise, please?
> 
> Thanks,
> 
> ------
> Sergei
> 
>  
> 
> 
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>