Weighted balanced binary tree の平衡条件をWolfram Engineで

注: ガチ誰得記事

Weighted balanced binary treeという平衡二分探索木があります。詳細はwikipedia(Weight-balanced tree - Wikipedia)が詳しいのですが、ざっくり言うと

  • 「子のサイズが親のサイズの少なくとも $\alpha$ 倍」
  • もしくは同値な表現として「左右の子のサイズが高々 $\frac{1}{\alpha} - 1$ 倍しか違わない」

という平衡条件の木です。ここで、サイズというのは葉にのみ値を載せる木ならば葉の個数、全部の頂点に値を載せる木ならば(頂点の個数) + 1とします。

$\alpha$ を大きくすればするほど回転が増える代わりに強く平衡(=木の高さが低くなる)し、$\alpha$ を小さくすればするほど回転が減る代わりに平衡が弱くなります。

このサイズ情報はまず間違いなく競技プログラミングだと管理する(K番目のアクセスに必要なため)ので、赤黒木等と違い追加メモリが実質0と言う利点があります。カロリー0!

この木は強そうなのですが、うまく動く証明が難しいです。葉にのみ値を載せる木の場合のmerge関数はたとえば次のようになります。

Node* merge(Node* l, Node* r) {
    if (is_balanced(l->size, r->size)) return make_node(l, r);
    if (l->size > r->size) {
        auto x = l->l;
        auto y = merge(l->r, r);
        if (is_balanced(x->size, y->size)) return make_node(x, y);
        if (is_balanced(x->size, y->l->size) && is_balanced(x->size + y->l->size, y->r->size)) return make_node(make_node(x, y->l), y->r);
        return make_node(make_node(x, y->l->l), make_node(y->l->r, y->r));
    } else {
        ...
    }
}

このコードはどういうことかというと、lとrをマージしたい時、

  • lとrをそのままマージして問題ない: マージする
  • lがrに対してデカすぎてマージできない場合は、l->rとrを再帰的にmergeする。そしてl->lをx、merge(l->r, r)をyとする。
  • a = x, b = y->l->l, c = y->l->r, d = y->rとして、下図の3つの木のうち、少なくともどれか一つはうまくバランスしている。

という、大変魔法のようなマージ関数になります。

もちろん、任意の $\alpha$ についてこのmerge関数が動くわけではなく、wikipediaにあるように $0 \lt \alpha \lt 1 - \frac{1}{\sqrt{2}}$ ならば動きます。

今日はこの事実をWolfram Engine (Wolfram Engine) を利用して確かめていきましょう。

  • 変数 t を $\frac{1}{\alpha} - 1$ とします、つまり左右の子は高々 t 倍しかサイズが違わないという意味です。
  • 変数 a, b, c, d を上図の a, b, c, d のサイズとします
  • 変数 er のサイズとします。つまり l のサイズは a + b + c + d - e です。

まず、次のことが言えます

  • lr より t 倍以上大きい: (a+b+c+d-e) > t e
  • 元々 l->ll->rはバランスしていた: a <= t(b+c+d-e) && t a >= (b+c+d-e)
  • bcはバランスしている: b <= t c && t b >= c
  • b + cdはバランスしている: (b+c) <= t d && t(b+c) >= d

そしてこの条件下で

  • 図の一番上のマージが失敗する = (ab+c+dがバランスしていない): (t a < b+c+d || a > t(b+c+d))
  • 二番目のマージが失敗する = (ab+cがバランスしていない OR a+b+cdがバランスしていない): (t a < b+c || a > t(b+c) || t(a+b+c) < d || a+b+c > t d)
  • 三番目のマージが失敗する = (ab / cd / a+bc+d のどれかがバランスしていない): (t a < b || a > t b || t(a+b) < c+d || a+b > t(c+d) || t c < d || c > t d )

これを全てまとめてwolfram engineに投げると次のようになります

In[1]:= Resolve[Exists[{a, b, c, d, e}, 1 <= t && 0 <= a && 0 <= b && 0 <= c && 0 <= d && 0 <= e && (a+b+c+d-e) > t e && a <= t(b+c+d-e) && t a >= (b+c+d-e
) && b <= t c && t b >= c && (b+c) <= t d && t(b+c) >= d && (t a < b+c+d || a > t(b+c+d)) && (t a < b+c || a > t(b+c) || t(a+b+c) < d || a+b+c > t d) && (t
 a < b || a > t b || t(a+b) < c+d || a+b > t(c+d) || t c < d || c > t d )], t]

Out[1]= 1 <= t < 1 + Sqrt[2]

というわけで、$1 + \sqrt{2} \le t$、つまり$\alpha \le \frac{1}{2 + \sqrt{2}} = 1 - \frac{1}{\sqrt{2}}$ならば正しく動くことがわかりました。

結論: wolfram engineってすごい