めぐる式二分探索
以下では、めぐる式二分探索が正しく動作する理由を探ってみる。appbird.icon 記法
$ \lbrack x; y) := \lbrack x, y) \cup (y, x\rbrack
$ x, yの間にある区間であって、$ xを含むような半開区間 （要するに$ x,yの順序を気にしたくないがために作った記法）
普通の区間と同じく、次の性質が成立する
ただし、$ y \in \lbrack x;y)
$ \lbrack x; z) \setminus \lbrack y;z) = \lbrack x; y)
$ \lbrack x; y) \setminus \lbrack x;z) = \lbrack z; y)
$ x \geq yの場合と$ x < yの場合に分けると証明しやすいappbird.icon
$ t \in X を境にして成否が変化する次の条件$ P: X \to \{T, F\}を考える。
公理i)$ P(t) = T
$ tでは真
公理ii) $ x < t < yのとき$ P(x) \neq P(y)（単調性） $ tに対して異なる側にある二点をとると、$ Pの成否は異なる
ここから、同じ側にある二点に対しては$ Pの成否が同じことが示せるappbird.icon
ただし、$ t \notin \{\min X, \max X\}*1
条件$ Pが与えられるので、$ tを求めよ。
注
*1 この制約は$ Pが全射（$ T, Fどちらも返り値として取りうる写像）なことを保証するため $ tにかけられた条件は必要以上に厳しいように見えるが（最大値・最小値ダメ）...
そうならないように、問題の制約に合わせて$ Xを取り直せばよい
アルゴリズム
1. 探索空間$ Xの端点として、$ \{ \min X, \max X\}が挙げられるが $ P(ok) = T, P(ng) = Fとなるように$ ok, ngを設定する。
以降、この$ \lbrack ok; ng)の区間...すなわち「$ ok側の端点を含めた$ ok, ngの間の区間」を探索区間と呼ぶことにする また、探索区間の長さは$ |ok - ng|として定める。
2. while$ |ok - ng| > 1:
3. $ mid = (ok + ng) / 2($ /は整数除算) 4. if $ P(mid): $ ok = mid
5. else: $ ng = mid
6. return $ ok
性質
whileループのどのステップにおいても
1. $ P(ok) = T, P(ng) = Fである。
これは代入の条件(4., 5.)から明らかである。
2. $ tは探索区間の間に存在する。つまり$ t \in \lbrack ok; ng)
3. ステップの過程で、探索区間の長さは必ず$ 1に到達する。
つまり、探索区間が突然$ 0になることはない
正当性
性質2, 3から、探索区間の長さが$ 1になる時が存在し、その時$ ok = tである。
従って、2.のwhileループが終了した地点で$ ok = tが成立し、6.の戻り値は期待した値そのものになっている。
性質2の証明
長さ$ nからアルゴリズムを始めた時に、$ tは探索区間の間に存在することを示そう。
以下、議論を単純にするため$ ok < ngとする。（符号を全て反転すれば逆の場合の証明が得られる）
i) 探索区間の長さ$ 1からアルゴリズムを始めたとき、
$ X = \{ok, ng\}であって、$ P(ok) = T, P(ng) = F
この段階で、探索区間は$ tを含んでいる。
$ X中では$ okしか$ tになり得ないため。背理法によって示せる。 このとき探索区間の長さは$ 1なので、whileループを一度も実行することなく$ okを出力して終了する
ii) 探索区間の長さ$ l \leq kからアルゴリズムを始めたとき、$ tは探索区間の間に存在し続けていたとしよう。
$ k + 1から始めたときに$ tが探索区間の間に存在し続けるかを調べる。
$ k + 1の長さでは、次の二通りを考える必要がある。（$ |ok - ng| = k + 1）
整数除算の性質より、$ mid = (ok + ng)/2は$ \lbrack ok; ng)に含まれる。 $ P(mid)が$ Tのとき
このとき、操作$ ok = midが加えられる。
この操作によって省かれた区間$ \lbrack ok; ng) \setminus \lbrack mid; ng)に$ tが含まれないことを示そう。
含まれていたと仮定する。
このとき、$ \lbrack ok; ng) \setminus \lbrack mid; ng) = \lbrack ok; mid)となる。
$ okそのもの、または$ okと$ midの間に$ tが存在することになる。
しかし、この間の区間は$ P(ok) = P(mid) = Tであったので、この間に$ tが存在すると$ Pの公理ii)に反する。
したがって、$ tは含まれておらず、省かれていない区間にまだ$ tが残留していると考えられる。
$ P(mid)が$ Fのとき
このとき、操作$ ng = midが加えられる。
この操作によって省かれた区間$ \lbrack ok; ng) \setminus \lbrack ok; mid)に$ tが含まれないことを示そう。
含まれていたと仮定する。
このとき、$ \lbrack ok; ng) \setminus \lbrack ok; mid) = \lbrack mid; ng)となる。
$ midそのもの、または$ midと$ ngの間に$ tが存在することになる。
しかし、この間の区間は$ P(ng) = P(mid) = Fであったので、この間に$ tが存在すると
$ t = midでは、$ Pの公理i)に
$ t \neq midでは、$ Pの公理ii)に反する。
したがって、$ tは含まれておらず、省かれていない区間にまだ$ tが残留していると考えられる。
これ以降、このアルゴリズムは$ l \leq kから始めた場合の動作と同等になるため、仮定より$ tは引き続き探索区間の間に存在し続けることになる。