ゆとりポイントの逆襲

とりあえずロボットの初期位置をひとつだけずらした状態でmin_transを呼び出すと値が２以上減ることはないということを証明しましょう。

Lemma min_trans_le:
  forall (os: list Order) (bp op bp' op' bd od :Z),
    -1 <= bd <= 1 -> -1 <= od <= 1 ->
    min_trans bp op (bp'+bd) (op'+od) os <= min_trans bp op bp' op' os + 1.

初期位置がひとつ違うということは、最初にボタンを押すロボットが１ターン早くボタンを押せる場合があるわけです。１ターン早くボタンを押すと、もう片方のロボットにたまるゆとりポイントが１だけ少なくなります。ゆとりポイントが減ると、そのロボットが次のボタンを押すのにかかるターン数が１ターン余計にかかる場合があるわけです。ボタンを押すのに１ターン余計にかかると最初のロボットにたまるゆとりポイントが増える場合があります。ゆとりポイントが増えるとボタンを１ターン早く押せます。もはやわけがわかりません。

このようにループ間で参照される変数というのを特徴付けるのは非常に難しいのです。

というわけで、問題はゆとりポイントの増減が結果にどう影響するのかということになりました。結論からいうと

Lemma min_movesRel_aux_1_1:
  forall (os: list OrderRel) (bp op: Z) (bd od: Z),
    0 <= bd <= 1 -> 0 <= od <= 1 ->
      min_movesRel_aux (bp+bd) (op+od) os <= min_movesRel_aux bp op os <= min_movesRel_aux (bp+bd) (op+od) os + 1.

ようするに、各ロボットのゆとりポイントを高々１だけ増やしても、結果は変わらないか１減るかの場合しかないわけです。この不等式を定式化するのにほとんどの時間を費やしました。前に書いたようにゆとりポイントが増えると、後で他のロボットのポイントが減ることになったりするので、この不等式を両方同時に帰納法で証明しないといけません。

適当に１ターン動かすと

状態Ａから適当に１ターン動かして状態Ｂになったとします。Ａでの結果をmin_trans(A)としてＢのときをmin_trans(B)と書くことにすると

min_trans(A) ≦ min_trans(B) + 1

であることを証明できれば、min_transより短い手順で解くことは出来ません。どんなにがんばって１ターンすすめても、この関数を１より多く減らすことは出来ないのです。たったこれだけを証明するだけでこれより短い手順がないことを証明できるのです(ゴールに到達したときに値がゼロになるもいるけど)。

逆に、この不等号を等号にするような一手が必ず存在することを証明できれば、この手数を実現するような手順が存在することを証明できます。

とりあえず、これより短い手順がないこと

これより短い手順がないことを証明するには、手順とはなにかを定義しないといけません。

Inductive Move : Set := Left | Right | Push | Stay.
Inductive Moves : Set := moves : Move -> Move -> Moves.

各ロボットは１ターンに４種類の行動ができて、青のと橙のとの行動のペアが１ターンの手になります。list Movesが手順になります。

この手順が命令列を正しく実行するかの述語が必要です。

Definition correct_moves (bp op: Z) (ms: list Moves) (os: list Order) := (* 略 *).

この述語はロボットの初期位置と手順と命令列を引数にとって、その手順でロボットを動かすと命令列の通りにボタンが押されることをあらわす述語です。中身はかなりめんどくさいです。

証明したいことは、正しい手順の長さはさっきの関数の返り値以上であること

Lemma correct_moves_min:
  forall (ms: list Moves) (bp op: Z) (os: list Order),
    correct_moves bp op ms os ->
    min_trans 0 0 bp op os <= Z_of_nat (length ms).

うわあ。こんなのどうやって証明するんだよ

何をとち狂ったか

なんとなく、押すボタンの位置を前回の位置からの相対距離で覚えておいたほうが簡単かなあと思っちゃったんですよ。で、相対位置に変更した命令の型と相対位置に変換する関数。

Inductive OrderRel : Set := orderRel : Robo -> comparison -> Z -> OrderRel.

Fixpoint translateRel_aux (bp op: Z) (os: list Order) : list OrderRel :=
match os with
| nil => nil
| order Blue bp'::os' =>
  orderRel Blue   (bp ?= bp') (Zabs (bp - bp')) :: translateRel_aux bp' op os'
| order Orange op'::os' =>
  orderRel Orange (op ?= op') (Zabs (op - op')) :: translateRel_aux bp op' os'
end.

Definition translateRel (os: list Order) := translateRel_aux 0 0 os.

というのができたわけです。どう考えても問題を複雑にしてるだけです。これを使ったときの最小手数関数は

Definition Zmax0 := Zmax 0.

Fixpoint min_movesRel_aux (bp op: Z) (os: list OrderRel) :=
match os with
| nil => 0
| orderRel Blue   _ bp'::os' =>
  let n := Zmax0 (bp' - bp) + 1in
  n + min_movesRel_aux 0 (op + n) os'
| orderRel Orange _ op'::os' =>
  let n := Zmax0 (op' - op) + 1in
  n + min_movesRel_aux (bp + n) 0 os'
end.

Definition min_trans bp op bp' op' os :=
  min_movesRel_aux bp op (translateRel_aux bp' op' os).

もはや、再起呼び出しの中で現在位置を覚えておく必要はありません。ゆとり引数だけ回していたらいいわけです。完成した「min_trans」関数は現在のゆとりポイントの初期値と初期位置と命令列を引数にとって、最小手数を返します。

何を証明するのか？

証明することは、この関数が最小手数を返していることです。最小手数であるというのはどういうことかというと、

どんな手順でロボットを動かしても、これより短くできない手数

のことです。というのは残念ながらよくある間違いです。

ある手順でロボットを動かせばその手数が達成できて、どんな手順で動かしても、それより短くできない手数

のことです。上の関数が最小手数を返すことを証明するには、実際にその手数でロボットを動かす手順を構成することと、それより短い手順がないことの２つを証明しないといけません。

A問題が如何に難しかったか

Coq

起きたらすでに残り14時間とかどこかおかしい。

A問題はこんなかんじ

青と橙のロボットがいます。ロボットを動かして指令通りの順番でボタンを押させます。

指令は「O 2, B 1, B 2, O 4」のようにどのロボットがどのボタンを押すかの列で与えられます。

各ロボットは最初に1の位置にいて、各々1ターンに「左右に一歩移動」「ボタンを押す」「何もしない」の行動ができます。

指令通りのボタンを押し終えるまで最短で何ターンかかるでしょう？ただしボタンを同時に押してはいけません

はいはいグリーディー。貪欲にやれば正解です。こんなのグリーディーにやる以外にないし、あまりに自明すぎて証明する必要も感じられません。しかし、今回は最近話題のCoqで解くことにしたので、こんな当たり前のことでも証明しないといけないのです。証明すればバグに悩むこともありません。

とりあえず、ロボットのenumを作りましょう。命令はロボットと位置を表す整数のペアです。

Inductive Robo : Set := Blue | Orange.
Inductive Order : Set := order : Robo -> Z -> Order.

で、list Orderを受け取って最短手数を返す関数を書けばいいんですよ

(* 距離を計算してゆとりポイントを負にならないように引く *)
Definition yutori_minus (x y z: Z) := Zmax 0 (Zabs (x - y) - z).

Fixpoint minimum_aux (bp op bx ox: Z) (os: list Order) :=
match os with
| nil => 0
| order Blue bp'::os' =>
    let n := yutori_minus bp' bp bx + 1 in
    n + minumum_aux bp' op 0 (ox + n) os'
| order Orange op'::os' =>
    let n := yutori_minus op' op ox + 1 in
    n + minumum_aux bp op' (bx + n) 0 os'
end.

Definition minimum (os: list Order) := minimum_aux 1 1 0 0 os.

開始地点とゆとり引数と命令列を引数にとって、次にボタンを押すロボットは全力で押しに行って、その間もう一個のロボットは何かする代わりにゆとりポイントを貯めて、次にそのロボットを動かすときはゆとりポイントを消費するようにすればできあがり。

あとはこれが最小値を返してることを証明すれば終わり！こんな綺麗な再起呼び出ししかしてない関数の証明なんて簡単です！

確率の神の話

Math

http://d.hatena.ne.jp/nishiohirokazu/20110217

こういう話は確率の問題をどのように数学で定義しているかっていう哲学的な話が繋がってないから、数式だけ見てこれとこれの違いが分からないってことになってるんだと思う。

確率は突き詰めていくと、いつかは人間には分からない領域まで到達するわけで、例えば計測の誤差みたいなものは、人間が観測できるのは誤差の総和だけで、各々の誤差の要素はよく分からないとかそういうもの。

でも、人間に分からない領域だからなんでもありというのでは何も進まないわけで、以下のことぐらいは保証されてるとみなそう。これが第１の原理になる。

全ての確率的な現象はさいころと同等の現象である:
  起こりうる結果全てからなる集合Aが定まる(さいころだと#A=6)
  Aからランダムに一つ結果が選ばれる
  どの元が選ばれやすいかはA上の測度で定まる

一つの現象だけ考えるならこれで十分だけども、複数の現象がある場合はこれだと困る。
もしかしたら現象Aと現象Bにはなにか関連があるかもしれない。それを表現する方法もないといけない。それは集合A×Bというより大きなさいころがあると思って、AとBの結果は大きなさいころの結果の一部だと思えばよい。

そうやってどんんどん大きなさいころが必要になってこれではきりがないので、十分に大きなさいころが最初から一つ与えられていることにしよう。これが第２の原理になる。

神だけがさいころを振る:
  神のさいころがひとつだけある
  神が一回さいころを振るだけで、ほかの全ての現象の結果がひとつに定まる

この神のさいころのことをΩと呼ぶ。

神の結果には全ての確率的現象がエンコードされてるので普通は理解できない。
神のさいころの目から人間にも理解できる結果を読み出す装置が確率変数である。

では、確率分布というのはなんだろう。

それは人間にも理解できる確率測度のことだと思えばよい。
(Ω,F,P)のPはΩ上の確率測度ではあるがこれを分布とは呼ばない。神のさいころの法則などは人間には理解できないものだからだ。

人間にも理解できる測度というのはもっと制限されたもので、R上の確率測度(正規分布とか)、N上の確率測度(ポアソン分布とか)。確率変数も基本的に人間が理解できる結果なので、対応する分布を考えることができる。

という風に世界を二つに分けた見方が必要だと思う。

ωを省略するのは、もちろん全部書いてるととてもじゃないが大変なんだからなんだけども。見方によってはωは定数だと思ってもよい。
それは神はさいころを一度しか振らないからで、それだけですべてのランダムな結果が確定してしまうから。
ωが動いているように見えるのはたんに人間側に情報が不足しているだけで、その無知な部分だけぶれてるって見方もある。