[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
More information about the Agda
mailing list