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/blob/master/src/coq/Ltgmonad.v

二つのモナドを用意しました。cmdexモナドとaicmdモナドです。

cmdexモナドは一つのスロットで実行される命令列を作ります。

putl;; zeror;; succl;; dbll;; getl

こんな感じに書くと、左put右zero左succ左dbl左getを順に実行します。

ExStateの型はcmdex stateiで、現在の状態を返します。stateiにはプレイヤーと盤面と実行中のスロット番号が入っています。よって

Definition p (c : card) : cmdex unit :=
  let v := value_of_card c in
  s <- ExState;
  let v' = getf (sti_board s) (sti_player s) (sti_i s) in
  if eqvalue v v' then
    ret tt
  else 
    clear;; ExRight c   

みたいに書くことで、現在の状態を見て判定するようなスロットの初期化なんてのを書けたりするわけです。

aicmdモナドはAIを作ります。arunはスロット番号を指定してcmdexモナドを実行します。

  arun 0 (putl;; zeror;; succl;; dbll;; getl);;
  arun 1 (putl;; zoerr;; getl)

AiStateはaicmd state型でスロット番号がない以外はExStateと同じです。

STモナドの機能も実装しました。

AiNew : forall T, T -> aicmd (ptr T).
AiRead : forall T, ptr T -> aicmd T.
AiWrite : forall T, ptr T -> T -> aicmd unit.

AiNewでポインタを作成して、AiRead/AiWriteで読み書きします。

セクション

Coqのセクションという機能を使うとグローバル変数みたいなのを使えます。

Section Hoge.
  Variable x : nat.

  Definition foo := x + 1.
  Definition bar := foo + 2.
  (* Section の中では x はグローバル変数みたいに使える *)
End Hoge.

(* Section を閉じると、foo と bar は x を引数にとるようになる *)
Definition baz := bar 42.

この機能とポインタを一緒に使うと変更できるグローバル変数みたいに使えます。

Section Foo.
  (* 最後にスロット8に置いた、ヒーラー。まだ置いてなければ None *)
  Variable heal_4095_at_8 : ptr (option value).

  (* スロットnにヒーラーが設置されている? *)
  Definition check_healer n : aicmd bool :=
    v <- myfld n; (* 自分とこのスロットnを読む *)
    v' <- AiRead heal_4095_at_8; (* スロット8に置いたかどうか *)
    match v' with
    | Some v'' => ret (eqvalue v v'')
    | None => ret false
    end.

  Definition make_healer :=
    ifb check_healer 8
    then
      ret tt
    else
      arun 8 (...);; (* がんばってヒーラーを作る *)
      v <- myfld 8;; (* できあがった値を読み出す *)
      AiWrite heal_4095_at_8 (Some v). (* ポインタに覚えておく *)
End Foo.

みたいな感じ。これは未来のプログラム言語に違いない!

cmdexの中ではポインタの操作はできないので、ためしにcmdexを実行してうまくいくか試すなんてことができるはず。でも本当は複数のarunをグループ化してそれをしたいわけなので、ポインタ部分はaicmdから分離すべき。

今の実装は公理の中に

Axiom ptr : Type -> Type.
Axiom make_ptr  : forall {T}, T -> ptr T.
Axiom read_ptr  : forall {T}, ptr T -> T.
Axiom write_ptr : forall {T}, ptr T -> T -> unit.

が入っているので、実はどこからでも操作できたりする。これをちゃんとモナドの中に入れた公理にするのはTODO。

モナドのインタープリタ

モナドを実行するインタープリタを書かないといけません。必要なのはaicmdを受け取って、次に実行するコマンドと残りのaicmdを返す関数です。OCaml側がその関数を順に呼び出します。

とりあえずの実装なので、動くんだけど効率とかよくないし直したい。継続を返すようにするともっと効率がよくなる気がするし、よく考えたらCoFixpointで実装してもいい気がする。多分。

最初のフェーズはモナドの先頭部分がコマンドになるまで、bindを崩していきます。

hnf_cmd : forall A, cmdex A -> cmdex A.
hnf_ai : forall A, aicmd A -> aicmd A.

がそれを行います。match in return withが飛び交う修羅場になっています。

hnf_cmdはコマンドcを受け取ると、cで場合分けして

  • c' >>= f の形でない場合はc自身を返す
  • c' >>= f の形だったら、再帰的に c' に適用する。その結果の c'' で場合分けして
    • ret v の形だったら、f v に再帰的に適用する。
    • ExState の形だったら、現在の状態をfに渡して、結果に再帰的に適用する
    • ExNop だったら、f tt に再帰的に適用する。
    • そのほかの場合は c'' >>= f を返す。

よく考えると、ExNopは必要ないです。ret ttを使えばいいので。

hnf_aiはほとんど同じですが、arun に対しては hnf_cmd を呼び出します。

あとは先頭を取り出す関数を書けばモナドインタープリタは完成です。