Coq

インタープリタ

https://github.com/kik/ICFPC2011/blob/master/src/coq/Ltg.v

ここは急いで書いたのでバグがあるかもしれない。ただ、ここはデバッグするよりも証明したほうが早いと思う。

Inductive evalue : Set :=
| EValue : value -> evalue
| EApp : evalue -> evalue -> evalue.

Inductive eresult : Set :=
| EDone : value -> list trace -> board -> eresult
| EFound : evalue -> list trace -> board -> eresult
| EFail : list trace -> board -> eresult.

step0 : player -> bool -> value -> value -> list trace -> board -> eresult.

この関数が関数適用を1つ実行する。引数は順に、プレイヤー・ゾンビ？・左の値・右の値・今までのトレース・盤面。

結果は、EDoneだと評価終了。EFoundだとまだ未評価の部分がある。EFailは失敗した。中には結果の値と追加されたトレースと評価後の盤面。

step : player -> bool -> evalue -> list trace -> board -> eresult.

この関数は次に実行すべき関数適用をみつけて、そこにstep0を適用する。実装は

Fixpoint step ev tr bd :=
  match ev with
    | EValue v => EDone v tr bd
    | EApp (EValue v0) (EValue v1) => step0 v0 v1 tr bd
    | EApp v0 ((EApp _ _) as v1) =>
      match step v1 tr bd with
        | EDone  v1' tr bd' => EFound (EApp v0 (EValue v1')) tr bd'
        | EFound v1' tr bd' => EFound (EApp v0 v1') tr bd'
        | EFail tr bd' as e => e
      end
    | EApp ((EApp _ _) as v0) ((EValue _) as v1) =>
      match step v0 tr bd with
        | EDone  v0' tr bd' => EFound (EApp (EValue v0') v1) tr bd'
        | EFound v0' tr bd' => EFound (EApp v0' v1) tr bd'
        | EFail tr bd' as e => e
      end
  end.

まさに教科書どおりに実装。引数を先に評価する正格評価では右側がEAppならそっちにすすんで、そうではなくて左側がEAppならそっちに進んで、そうでなければ両辺とも評価済みなので関数適用を評価。

eval : player -> bool -> nat -> evalue -> list trace -> board -> eval_result.

最後にこれで、step0を与えられた回数実行する。

残り評価回数を引数にした再帰関数を回さないのはなぜかというと、それはかなり難しいからです。グローバル変数にしたくなる気持ちがよくわかります。

正しく操作的意味論を書けば、動作の証明はほとんど自明だと思います。あとでやってみる。そして多分バグがみつかるはず。

詳細

https://github.com/kik/ICFPC2011

インタープリタ

ゲーム中に存在する全ての値を

type value =
  | ValNum of int
  | ValI
  | ValSucc
  | ValDbl
  | ValGet
  | ValPut
  | ValS
  | ValSf of value
  | ValSfg of value * value
  | ValK
  | ValKx of value
  | ValInc
  | ValDec
  | ValAttack
  | ValAttacki of value
  | ValAttackij of value * value
  | ValHelp
  | ValHelpi of value
  | ValHelpij of value * value
  | ValCopy
  | ValRevive
  | ValZombie
  | ValZombiei of value

といった感じで、完全に記述できる型を用意するのが常識だと思っていたんだけど、まわりのコード眺めてるとそうなってなくてびっくりした。

最初のAI

https://github.com/kik/ICFPC2011/blob/d67edcf101921b1fe72f449799b479cc9c6d8a1a/src/kamaboko.ml

まず、全力で5000と10000を作る。5000で三回攻撃して255を倒す。

次に、255をゾンビ化して0を速攻で倒す。
ゾンビ化のコードを引数つき永続化版にする。
succ zombieを繰り返す

何もしないAIは650ターンで死ぬ。動くこと優先で書いたのだが、この時点ではかなり速かったらしい。
helpで倒すようにすれば256ターン減らせるので、すでに最速の2倍ちょいくらいにはなっていたらしい。

ICFPC2011参加記録

例年のごとく一人で参加。

時刻は全てUTCで

17日

  • 00:00 問題が公開されたので読む。予想通り殴り合いゲーだ。
  • 01:00 大体問題を理解したので、インタープリタを書き始めてみる。言語はOCamlを選択。というかこれ以外に選択肢がない
  • 03:00 電車で会社に移動しながら戦略を考える。最大のダメージを与えられるのはゾンビなのが分かる
  • 04:00 インタープリタの続きを実装
  • 10:00 このころにはインタープリタはできてたはず。SKIの使い方を考え始める
  • 11:00 無限ループを参考に、S(get)(SK(dec))0が無限dec 0であることに気づくが実装できない。
  • 12:00 S(Kx)yz = x(yz)に気づく。無限dec 0の動作を確認する。
  • 13:00 lazyを発見する。これにより動的にgetできるようになる。
  • 14:00 電車で帰宅。作戦を考える。
  • 15:00 ほぼ部品は整ったので、最初のAIの作成にとりかかる。作戦はすぐに決まる。
  • 21:00 最初のAIが完成する。送信。風呂って寝る。

18日

  • 09:00 活動開始。今のリスト再生AIを拡張するのは無理なので、書きやすい記法を考えようとする。
  • 10:00 モナドが最適なことが分かる。OCamlで書こうとするがいまいちしっくりこない。
  • 11:00 OCamlの型システムと演算子定義がクソだからいけない。そういえばYnotのモナドはかっこよかった。Coqで書いてOCamlに抽出すればいいんじゃね？
  • 12:00 Coqでコード書くのたのしいお

19日

  • 12:00 いつのまにか一日たってた。眠くてしかたがない仮眠してAI書こう。
  • 15:00 AIを書こう。
  • 23:30 結局AIを書き終えられなかった。しかたないので急いで提出

A問題をやっと解けた。一週間もかかったよ

Coq

https://gist.github.com/971586

色々と工夫してみた。

ロボットと指令の定義。これは前と同じ。

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

Definition robo_inv (robo: Robo) :=
match robo with
| Blue => Orange
| Orange => Blue
end.

移動命令の定義。ボタンを押すを移動から分離した。さらにどっちのロボットへの命令なのかを型にいれることにした。

Inductive Move (robo: Robo) : Set := Left | Right | Stay.
Inductive Moves : Set :=
| moves : Move Blue -> Move Orange -> Moves
| pushmove (roboPush: Robo) : Move (robo_inv roboPush) -> Moves.

型「Move Blue」は青ロボットの移動を値として持つ。各ロボットへの命令の組は両方移動するか、片方がボタンを押して残りが移動するだけなので、上の２つだけにした。pushmoveにボタンを押すロボットを指定すると移動するほうのロボットの移動しか渡せなくなるように型を付ける。

各ロボットの座標の組の定義

Record ZZ : Set := zz {
  pB : Z;
  pO : Z
}.

(* 略 *)

Definition do_move (r: Robo) (m: Move r) (p: ZZ) :=
match m with
| Left  => paddz r p (-1)
| Stay  => p
| Right => paddz r p 1
end.

これによって、Move Blue型の値をdo_moveに渡すとBlueの座標が変化する。引数rは暗黙引数にできる。

ふたつのロボットを同時に動かす場合はこんな感じ。

Definition do_moves (mb: Move Blue) (mo: Move Orange) (p: ZZ) :=
  do_move mb (do_move mo p).

移動命令のリストが指令のリストに正しく則っているかの述語。「Correct pfrom pto os ms」は位置pfromから命令列msでロボットを動かすと、指令列osの順にボタンを押して、最終的に位置ptoにくるという述語。

Inductive Correct (pfrom: ZZ) : ZZ -> list Order -> list Moves -> Prop :=
| c_nil:
    Correct pfrom pfrom nil nil
| c_moves (mb : Move Blue) (mo : Move Orange) os ms pto:
  Correct (do_moves mb mo pfrom) pto os ms ->
    Correct pfrom pto os (moves mb mo::ms)
| c_pushmove (r : Robo) (mv: Move (robo_inv r)) os ms pto:
  Correct (do_move mv pfrom) pto os ms ->
    Correct pfrom pto (order r (pfrom r)::os) (pushmove mv::ms).

この述語が真に成るのは次の場合のみ

  • ms=nilのときは、pfrom=ptoでos=nilのとき
  • ms=moves mb mo::ms'のときは、pfromをmbとmoで動かした結果をpfrom'とすると、Correct pfrom' pto m's osが成立するとき
  • ms=pushmove r mv::ms'のときは、pfromをmvで動かした結果をpfrom'とする。さらにos=o::os'で、oはロボットrがpfrom rでボタンを押す命令であり、Correct pfrom' pto ms' os'も成立するとき

というように問題を整理しなおしたので、多少は証明が簡単にはなって、このあと700行ぐらいがんばった結果

minimum_moves : list Order -> list Moves.

という最小の移動リストを返す関数が完成して、

Example sample_2 :=
  order Orange 2::
  order Blue 1::
  order Blue 2::
  order Orange 4::
  nil.

Eval vm_compute in (minimum_moves  sample_2).

の結果

     = moves (Stay Blue) (Right Orange)
       :: pushmove (roboPush:=Orange) (Stay (robo_inv Orange))
          :: pushmove (roboPush:=Blue) (Right (robo_inv Blue))
             :: moves (Right Blue) (Right Orange)
                :: pushmove (roboPush:=Blue) (Stay (robo_inv Blue))
                   :: pushmove (roboPush:=Orange) (Stay (robo_inv Orange))
                      :: nil
     : list Moves

と、実際に動くプログラムが完成して、しかもこれが最短であることも証明できた。

標準ライブラリの有理数って、Leibniz equalityじゃないから

Coq

微妙に使いにくいじゃないですか。ssreflectを読んでたら、こういうのを簡単に Leibniz equality にする方法が分かったので書いてみた。

https://gist.github.com/971135

まず、ZP = Z * positive の上に普通に同値関係を定義する ZP_eq : ZP -> ZP -> Prop。

次に、この同値関係で割ったときの代表元を返す関数を作る。canceled: ZP -> ZP。普通に約分しつくした形を代表元にする。

そして、魔法のような eq_irrelevance を証明する。

最後に ZP の部分集合 { x | canceled x = x } をQとする。これはもちろん代表元全体の集合だ。
仕上げに魔法のように Q_eq_dec を ZP_eq_Q_eq を証明する。

最後に実際の手順と比較する

ここまでくれば、どんな手順を渡されても、最初の一手は基本的にロボットを一歩動かすだけなので、簡単な作業になります。

最初の一手は青の動かし方が４通りあって、橙の動かし方が４通りありますから全部で

(coq Scripting *16 SUBGOALS* Holes)---------

残り時間は２時間を切っていたので諦めました。

ゆとり変換

ここまで証明できればあと少しです。初期位置の違いはゆとりポイントの初期値の違いと等価なはずです。

Lemma min_trans_1_0:
  forall (os: list Order) (bp op bp' op' bd:Z),
  Zabs bd = 1 ->
  exists d, Zabs d = 1 /\
    min_trans bp op (bp'+bd) op' os = min_trans (bp+d) op bp' op' os.

青のロボットの初期位置が1だけずれてるのは、ゆとりポイントを１だけ増やすか減らすかしたのと同等である。これくらいのことになってやっと自明といえるレベルです。