[Agda] DTO, STO, AVL.Tree

Serge D. Mechveliani mechvel at botik.ru
Sun Oct 21 16:05:29 CEST 2012

On Sun, Oct 21, 2012 at 12:05:36PM +0200, Nils Anders Danielsson wrote:
> On 2012-10-19 21:49, Serge D. Mechveliani wrote:
[..]
>> I am not sure, but have an impression that
>> 1) STO needs to be removed and to merge to DTO, with _<_ defined via
>>     _<=_  and  \neg (x \~~ y),
>
> See Relation.Binary.Props.StrictTotalOrder and
> Relation.Binary.Props.DecTotalOrder.

Indeed, looks like relevant. Thank you.

>> 2) AVL needs to generalize from \equiv to \~~.
>
> A previous version of Data.AVL allowed arbitrary equivalence relations.
> When I added the search tree invariant to the data structure I switched
> to a less general interface in order to avoid some complications. We
> could switch back, but I believe that both the code and the interface
> would become more complicated.
>

One more note of AVL
--------------------
AVL.Indexed  has the fragment

-- Converts the tree to an ordered list. Linear in the size of the tree.
...
toDiffList : Б┬─ {l u h-> Б├▓ Tree l -> h Б├▓ DiffList KV
toDiffList (leaf _)       = []
toDiffList (node k l r _) = toDiffList l ++ k ::┬╥ toDiffList r

It is desirable to add a proof for
(1) StrictlyOrderedList? <parameters> $toList t for toList = DiffList.toList \o toDiffList, (1) means that the result KV list is ordered by the first coordinate (Key), (2) fromList$ toList (t : Tree)  \equiv  t

(1) looks easy, and I do not know about (2).

After this, it will be easy to implement a  sorting function  of
O(n*(log n))  with all the needs proofs.
This function will be almost the same as
\lambda pairs -> toList (fromList pairs : Tree)

Regards,
Sergei