二分探索

二分探索は，値の探索に使うという認識が一般的だと思いますが，実際にはもっと守備範囲が広いです。ということでなるべく一般的な形で書くとどうなるのかを整理した話を書いてみることにしました。why3 で書いて正しいことを検証してみたらけっこうすっきり理解できた気がします。

int 上の述語 f があるとします。f を真にする a と偽にする b がひとつずつわかっていて，a < b であるとしましょう（requires のところ）。そうすると，f x だが f (x+1) ではない x を求めることができる（ensures のところ，result が戻り値），というのが関数の仕様です。

中身はまあ普通の二分探索なのですが，上限 ub は必ず f を満たさないように，下限 lb は必ず f を満たすようにするとわかりやすくて不変条件が簡単に書けます。

ソートされた列 A から値 v のインデックスを求めるよくある二分探索は，f x として A[x] <= v をとった場合になります。

ちなみにコード中では f に特に条件を付けていませんが，真偽が頻繁に入れ替わるような述語に対して使うケースはあまり見た記憶がありません。ある値を境にしてそれより下で真，上で偽（あるいはその逆）になる述語を考えて，その境界の値を求めるのに使うことが多いです。また a, b は自分で与えないといけませんが，たいてい自明な上界と下界があります。

上のコードが正しいことのチェックは，例えば手元の環境では why3 prove -P cvc4 binsearch.mlw を実行すると

binsearch.mlw BinSearch WP_parameter binsearch : Valid (0.03.s)

と出て，正しいことが自動証明できました。int の長さが限られている言語だと足し算がオーバーフローした場合に正しく動かない気がしますが，そこまではチェックしてないようです。

今回は整数上でやりましたが，実数上でも適当なεに対して f x だが f (x+ε) ではない x を求める，のような形で書けるでしょう（たぶん正確にはちょっと違う）。