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を与えられた回数実行する。

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

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