wt-tree のバグの話題 @chaton_gauche まとめ。

Chaton Gauche @chaton_gauche

kazu: こんにちは、IIJ の山本です。 http://bit.ly/de6Xv0

Chaton Gauche @chaton_gauche

kazu: MIT Scheme のことで恐縮ですが、質問させて下さい。 http://bit.ly/9WU3mS

Chaton Gauche @chaton_gauche

shiro: ようこそ。どうぞどうぞ。 http://bit.ly/b4IAUx

Chaton Gauche @chaton_gauche

kazu: 質問は、「MIT Scheme に wttee というライブラリがありますが、これはどれくらいつかわれていますか？」です。 http://bit.ly/95Yb6o

Chaton Gauche @chaton_gauche

kazu: 長いですが、背景を書いていきます。 http://bit.ly/c1E9Wq

Chaton Gauche @chaton_gauche

kazu: Haskell には、Data.Map という finite map の実装があります。 http://bit.ly/bxlGsH

Chaton Gauche @chaton_gauche

kazu: 内部では、weight binary search tree というバランス木が使われています。 http://bit.ly/aJIZTi

Chaton Gauche @chaton_gauche

kazu: the art of computre programming 3 では、AVL の代替品として半ページぐらい紹介されている木です。 http://bit.ly/ahD7r2

Chaton Gauche @chaton_gauche

kazu: 最近、Data.Map にバグが発見されました。 http://bit.ly/bhQN3w

Chaton Gauche @chaton_gauche

kazu: 挿入はいいのですが、要素を削除すると、バランスが壊れることがあるのです。 http://bit.ly/bw1t9Q

Chaton Gauche @chaton_gauche

kazu: これをきっかけに、weight binary search tree を研究してみて、面白いことが分かったので、現在論文を書いているところです。 http://bit.ly/aWysXC

Chaton Gauche @chaton_gauche

kazu: 同じアルゴリズムが、MIT Scheme の wttree にも使われています。 http://bit.ly/9e4bFp

Chaton Gauche @chaton_gauche

kazu: wttree の亜種を考えた Stephen Adams さんが、MIT Scheme のメンテナーだったみたいなので、入っていても不思議ではありません。 http://bit.ly/b7atGZ

Chaton Gauche @chaton_gauche

kazu: Data.Map の実装も、Adams さんのテクニカルレポートに基づいています。 http://bit.ly/9147wo

Chaton Gauche @chaton_gauche

kazu: というわけで、MIT Scheme の wttree にもバグがあります。 http://bit.ly/9v58Zy

Chaton Gauche @chaton_gauche

kazu: 実際、実験してみたところ、やはり削除で簡単にバランスを崩すことができます。 http://bit.ly/9XwQAB

Chaton Gauche @chaton_gauche

shiro: 実装のバグではなくアルゴリズム上のバグだったってことですか? http://bit.ly/bPTqJ5

Chaton Gauche @chaton_gauche

kazu: 大枠のアルゴリズムはいいのですが、パラメーターの選び方がダメです。 http://bit.ly/daLrVU

Chaton Gauche @chaton_gauche

kazu: Adams さんの wttree のパラメーターは (5,1) なんですが、これは削除のことをまったく考えていません。 http://bit.ly/bWZYrD

Chaton Gauche @chaton_gauche

kazu: (x,y) の x は、バランスが取れてないか判断して回転させるかを決めるもの、y は回転させるときに一回転か、二回転かを決めるものです。 http://bit.ly/cHA3Hs

Chaton Gauche @chaton_gauche

kazu: Adams さんの方式に対しては、数学的に証明を与えられていませんが、我々のテストでは (4,2) と (3,2) のときしかバランスが成り立ちません。 http://bit.ly/dBUhbw

Chaton Gauche @chaton_gauche

higepon: http://www.google.co.jp/codesearch?as_q=wttree&btnG=Search+Code&hl=&as_package=&as_lang=&as_filename=&as_clas… http://bit.ly/9EH63Q

Chaton Gauche @chaton_gauche

higepon: slib に含まれているようですね。 http://bit.ly/biBEEA

Chaton Gauche @chaton_gauche

kazu: Adams さんが元にしていて、TAOCP でも紹介されているオリジナルの論文の方式に対しては、我々は Coq で証明を与えられそうなところまで来ています。オリジナルの論文の方式に対する整数解は面白いことに (3,2) しか… http://bit.ly/c4JFDp

Chaton Gauche @chaton_gauche

kazu: 興味があれば、我々の英語のスライドをお送りします。 http://bit.ly/cnH0eJ