Об дерево

Понадобились мне тут в хозяйстве деревья, я взял пилу, топор и пошел в гугл, нашел там AA-деревья, про которые говорится, что они по эффективности как красно-черные, но в реализации проще. Это бинарное дерево, у каждой вершины (узла) есть "уровень", ее высота. Узлы с данными есть двух видов: первый вид имеет форму /\, оба поддерева ниже текущей вершины, обозначим его буквой А. Узлы второго имеют форму Г, в них правое поддерево той же высоты, что и текущая вершина, а левое поддерево ниже; обозначим второй вид буквой H. Инвариант для АА-деревьев звучит так:
1. The level of every leaf node is one.
2. The level of every left child is exactly one less than that of its parent.
3. The level of every right child is equal to or one less than that of its parent.
4. The level of every right grandchild is strictly less than that of its grandparent.
5. Every node of level greater than one has two children.

Тут leaf node - это вершина, у которой нет поддеревьев. Четвертое условие гарантирует, что в дереве не будет цепочек из горизонтальных ребер, поэтому, двигаясь от корня к любой вершине, мы будем спускаться на уровень вниз не реже, чем в половине шагов, а значит самый длинный путь в дереве не более чем в два раза длиннее самого короткого, что дает логарифмическое соотношение высоты и общего числа вершин.

Любой нормальный язык позволяет эти инварианты выразить в типах. Вот так, например, это выглядит в Идрисе:

data Tree : Type -> Nat -> Bool -> Type where
  Null  : Tree a 0 False
  ANode : Tree a n b1 -> a -> Tree a n b2 -> Tree a (n+1) False
  HNode : Tree a n b -> a -> Tree a (n+1) False -> Tree a (n+1) True

( Read more... )