2012-04-15

B問題

やるきがなくなってきたので、後の問題は適当にやった。B問題はやるだけ。

https://gist.github.com/2391806

2012-04-15

A問題

https://gist.github.com/2391779

ヒントの制約からなんとか関数を自動で生成したかった。

eexists (fun ch =>
  match ch with
    | "a" => _  | "b" => _  | "c" => _  | "d" => _
    | "e" => _  | "f" => _  | "g" => _  | "h" => _
    | "i" => _  | "j" => _  | "k" => _  | "l" => _
    | "m" => _  | "n" => _  | "o" => _  | "p" => _
    | "q" => _  | "r" => _  | "s" => _  | "t" => _
    | "u" => _  | "v" => _  | "w" => _  | "x" => _
    | "y" => _  | "z" => _
    | _ => ch
  end).

このへんまではまあ手で書いてやっても許されるだろう。で、ヒントをこの関数に食わせて reflexitivity で決定していく。
あれ、一個文字が確定しないぞ、しかたがないからほかの条件から埋めていくか。

しかし、ほかの条件はすごく重い。計算させようとしてすぐにemacsが凍りつく状態にないやがったので諦めて手で指定する。
ほかのプロパティーも重いのでかなり妥協して、Permutationだけにしたんだけど、やっぱり計算では証明できなくて非常に悲しい証明を書いてしまった。

OCamlを抽出して実行してもよかったんだけどめんどくさいから、trを抽出する。

tail -n +2 | tr ynficwlbkuomxsevzpdrjgthaq a-z | awk '{printf "Case #%d: %s\n", NR, $0}'

最終的にone liner

2012-04-15

GCJ予選

Prog

証明できそうな問題がないかなと探したところA問題だけだった。BとCもできるかもしれないけどめんどくさいからいいや

2011-12-13

ssreflect ライブラリ紹介(eqType編)

この記事はTheorem Proving Advent Calendar 2011の13日目の記事です。

ssreflectライブラリ紹介

この前はssreflectのtacticの紹介をやったので、ライブラリの紹介をします。ライブラリの概要は http://coqfinitgroup.gforge.inria.fr/ssreflect-1.3/ を見れば何か数学寄りだなというのが分かると思いますが、まあ完全に数学寄りです。しかもtrunkでは http://coqfinitgroup.gforge.inria.fr/ のように大変膨大になっております。

eqType

というわけで、一番根っこの部分にあるeqTypeを今回のメインにしましょう。

Coqを使い始めると、まあ誰でもこんな感じに書きたくなるでしょう。

Definition nat_gt0 := { x : nat | x > 0 }.
Definition nat_gt1 := { x : nat | x > 1 }.
Definition nat_gt0_succ : nat_gt0 -> nat_gt1 := (* うんたらかんたら *).

これにより、定義域を正の自然数に限定した関数 nat_gt0_succ が定義できました。プログラミングならこれでいいのですが、数学になると困ったことが起こります。例えば、この関数が単射であること:

Lemma nat_gt0_succ_inj : forall x y, nat_gt0_succ x = nat_gt0_succ y -> x = y.

これの証明は大変です。なぜかというと、xとyには各々が正であることの証明がくっついていますが、その証明が等しいことを示すのが困難だからです。すなわち、次のことを証明する必要があります。

Goal forall x (p1 p2 : x > 0), p1 = p2.

p1とp2はそれぞれxが正であることの証明で、それらが等しいことを示したいわけです。このように証明が等しいという性質をProof irrelevanceといいます。この問題の一番簡単な解決策は公理を導入することです。標準ライブラリの「Coq.Logic.ProofIrrelevance」を使うと「任意の命題がProof irrelevantである」が公理に追加されます。

ほとんどの場合で、この公理は不要です。eqTypeライブラリを使うとこの問題をほとんど解決してくれます。eqTypeは型クラスのようなもので、Canonical StructureというCoqの機能を使っています。まあほとんど型クラスのようなものです。eqTypeを実装した型Tは次の二つの値を持っています。

eq_op : T -> T -> bool.
eqP : forall x y, reflect (x = y) (eq_op x y).

ここで、「reflect」は一つ目の命題と二つ目のbool値が同値であることを示します。すなわち、等値性を計算できるというのがeqTypeのもっている特長です。もちろん

eq_dec : forall x y, { x = y } + { x <> y }.

は上の二つと同値です。たったこれだけなので、導ける定理も少ないというか重要なのはただ一つだけで、「eq_irrelevance」はeqTypeを実装していれば、命題「x = y」はProof irrelevantであるになります。系として、

Lemma bool_irrelevance : forall (x y : bool) (p1 p2 : x = y), p1 = p2.

が得られます。よって、{ x : T | P x } の述語の部分を「f x = true」の形に書ける場合はこの型の値を簡単に比較できるわけです。ssreflectではbool -> PropのCoercionを「is_true」で定めているので、これは単に { x : T | f x } と書くことが出来ます。

subType

型 { x : T | f x } の持っているインターフェースを抽出した型クラスが subType になります。そして、eqTypeのsubTypeは自動的にeqTypeを実装します。他にもtupleとかmatrixなんかがsubTypeを使ってeqTypeを実装していたりします。

次回予告

次はchoiceライブラリ？ exists x, P xから { x | P x }を取り出せる性質をもった型クラスを紹介するかも。

2011-06-21

モナドのインタープリタ

モナドを実行するインタープリタを書かないといけません。必要なのは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 を呼び出します。

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

2011-06-21

セクション

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。

2011-06-21

モナド

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で読み書きします。