Coqで型クラス(Haskell風 モナドの定義)
Coq version 8.2以降からHaskell風の型クラスが使えるようになったから使ってみることにした。
Haskellで型クラスといえばMonadが有名な気がするのでHaskell風のモナドHMonadを定義しよう。
Coqでの型クラスは次のように宣言するみたいだ。
Class HMonad (M: Type -> Type) := { mreturn : forall {A}, A -> M A ; mbind : forall {A B}, M A -> (A -> M B) -> M B }.
この定義だとHaskellのモナドとあんまり変わらないが、Coqは証明も第一級の値なので、なんらか満たしてほしい性質を型で指定することができる。モナドはモナド則を満たしてほしいので、モナド則をみたしていないといけないクラスにしよう。
モナド則を加えるとちょうどこんな感じになった。
Class HMonad (M: Type -> Type) := { (* fields *) mreturn : forall {A}, A -> M A ; mbind : forall {A B}, M A -> (A -> M B) -> M B (* axioms モナド則 *) ; left_identity : forall A B (a: A) (f: A -> M B), mbind (mreturn a) f = f a ; right_identity : forall A (m: M A), mbind m mreturn = m ; associativity : forall A B C (m:M A) (f: A -> M B) (g: B -> M C), mbind (mbind m f) g = mbind m (fun x => mbind (f x) g) }.
よし、じゃあ早速なにかインスタンスを作ってみよう。とりあえず簡単そうなMaybeにしよう。
証明の実装とか言われてもよくわかんないので、とりあえずmreturnとmbindの二つの関数だけを定義してみる。
Instance Maybe: HMonad option := { mreturn A x := Some x ; mbind A B m f := match m with | None => None | Some x => f x end }.
Coqのインスタンス定義では足りないフィールドがあっても対話的に与えることができる。モナド則の証明とかは対話的に証明した方が簡単そうなので、残りは対話的に与えよう。
coqtopのトップレベルでソースコードを書くか、ソースファイルを作って "-l" オプションで起動しよう。対話的な定理証明の始まりだ。
$ coqtop -l HMonad.v Coq < 3 subgoals ============================ forall (A B : Type) (a : A) (f : A -> option B), f a = f a subgoal 2 is: ... subgoal 3 is: ...
今回の証明はゴールにmatch式が出てきて盛りだくさんに見えるけど、こういうときは場合分けをすれば簡単だ。場合分けをするにはcaseタクティックが便利だ。ガンガン使おう。証明が全て終われば、モナド則が保証されたMaybeモナドの完成だ！
証明を含むソースコード全体は以下。
*1:ここでの{}で囲われたパラメータの書き方もCoq 8.2以降で追加された構文で、Agdaのそれと同じようなことを表している。つまり、このフィールドを使う側で{}で囲われたパラメータを書かなくても推論してくれるようにする構文だ。Coq 8.1以前では、Implicit Argumentsほげほげとか書かなくてはいけなかったのが、ちょっとシンプルに書けるようになっている。
しりとりの圏をCoqで実装してみた
Coq で しりとりの圏を形式化した記事を見つけた。
型によるしりとりの成立判定 - コンピュータってすごいらしい
via 完全実装付きでもう一度お送りします、しりとりの圏 - 檜山正幸のキマイラ飼育記
すばらしかったので、私もちょっと真似して実装してみた。亜鉛さんと同様に依存型を使ったのでしりとりが可能なときにのみ定義される合成(composition)をいい感じに実装できた。依存型グレイト！
comp関数は依存型が複雑で直接定義する事が難しかったので型だけ宣言してあとから証明木をtacticで作って実装した。
ただ、最後にQed.としてしまうと隠蔽されちゃってunfoldとかができなくなるみたい(http://www.lix.polytechnique.fr/coq/distrib/current/refman/Reference-Manual009.html#@default423 の6.9.1Opaque 参照)だったのでDefined.で締めくくる必要があるみたいだった(このことは依存型を扱う上で重要そうだが、今まで知らなかった)。
(** Shiritori Category *) Set Implicit Arguments. (* 対象 object *) Inductive Obj : Set := こ | ぶ | た | ぬ | き | つ | ね. (* 射 morphism *) Inductive Mor : Obj -> Obj -> Set := | single : forall A, Mor A A | cons : forall A' B (A: Obj) (tl: Mor A' B), Mor A B. (* 合成 composition *) Definition comp A B C (f: Mor A B) (g: Mor B C) : Mor A C. intros. induction f. exact g. exact (cons A (IHf g)). Defined. (* 恒等射 identity *) Definition id A : Mor A A := single A. (* 単位元律 unit law 01 *) Theorem unit_l : forall (A B: Obj) (f: Mor A B), comp (id A) f = f. Proof. intros; simpl. reflexivity. Qed. (* 単位元律 unit law 02 *) Theorem unit_r : forall (A B: Obj) (f: Mor A B), comp f (id B) = f. Proof. intros. induction f. simpl. reflexivity. simpl. rewrite IHf. reflexivity. Qed. (* 結合律 associative low *) Theorem assoc : forall A B C D (f: Mor A B) (g: Mor B C) (k: Mor C D), comp f (comp g k) = comp (comp f g) k. Proof. intros. induction f. simpl. reflexivity. simpl. rewrite IHf. reflexivity. Qed. (* 合成のテスト *) Definition w1 := cons こ (cons ぶ (single た)). Definition w2 := cons た (cons ぬ (single き)). Eval compute in comp w1 w2.
Coq の 応答 (Coq version 8.1pl2)
= cons こ (cons ぶ (cons た (cons ぬ (single き))))
: Mor こ き
SICPのEx 2.4 をCoqで解いてみた
SICPを読んでいたら 検証せよ という問題があったので、Coqで検証してみた。
問題はペア構造のチャーチエンコーディングの話。
Scheme (untyped λ) に比べて Coq (λC) は型が厳格なので、問題の定式化がちょっと大変だったけど、問題自体は簡単に証明できた。
CoqのコードからSchemeのコードを出力してみたら、問題で与えられているコードとだいたい一緒だったから大丈夫だろう。
Section SICP_EX_2_4. (* このセクションで使う二つの型 A, B を仮定する *) Variable A B : Type. Definition pair (X:Type) : Type := (A->B->X) -> X. Definition cons (X:Type) (x:A) (y:B) : pair X := (fun m => m x y). Implicit Arguments cons [X]. Definition car (z: pair A) : A := z (fun p q => p). (* Exercise 2.4 その1 任意の引数 x y に対して car (cons x y) が x となる事を検証する *) Theorem exercise_2_4_car : forall x y, car (cons x y) = x. Proof. auto. Qed. Definition cdr (z: pair B) : B := z (fun p q => q). (* Exercise 2.4 その2 任意の引数 x y に対して cdr (cons x y) が y となる事を検証する *) Theorem exercise_2_4_cdr : forall x y, cdr (cons x y) = y. Proof. auto. Qed. End SICP_EX_2_4. Extraction Language Scheme. Extraction cons. Extraction car. Extraction cdr.
コンパイル結果 (Coq 8.1 pl2)
(define cons (lambdas (x y m) (@ m x y))) (define car0 (lambda (z) (z (lambdas (p q) p)))) (define cdr0 (lambda (z) (z (lambdas (p q) q))))
■
Coqで高精度計算サイト
高精度計算サイトというのを見つけた。ここの電卓サービスは素晴らしく、大変感銘したのだが、一つ残念な点があった。
それは大きな数を扱うことができないということである。
例えば10^10000000のような大変大きな計算を実行すると答えは無限∞になってしまう。
このため、例えば(10^100000000)^(1/100000000)のように結果が10になるような計算式でも、途中で大きな数が含まれてしまうので結果は誤った値になってしまう。
この問題を訂正すべく、Coqの有理数演算を使って、似たようなサイトを作ってみた。↓
ここでは、どんな大きな数でも扱うことができるだけでなく、有理数体上の様々な定理が形式手法(定理証明)によって保証されているのだ。
つまりどんな入力に対しても、計算間違いが存在しないということだ。
(ただ、演算は+,-,*,/ だけしかまだ実装していない)
もちろん、入力を受け付けたり、結果を出力したりする部分はOCamlで実装していて、また、通信や表示などはブラウザなど別のプログラムが行っている。サーバーおよびクライアントのハードウェアにも依存しており、それらの部分で誤りがある可能性はゼロではない。しかし、コアの部分の計算ロジックを定理証明の力を借りることにより、システム(サービス)の信頼性を飛躍的にあげることができるのだ。
2009-01-26 追記: Mac OS X の Safari
ブラウザで表示が変になる現象を修正しました。
ソースコードは以下
Coqで依存型
最近Agdaがはやっているみたいなので、Coqでも依存型（dependent type）を使ってみた。 実装したのは長さ n のベクトル型だ。このベクトル型を使うと、空でないとか、長さが等しいとかを型の段階で保証できるので、より安全なプログラムを書くことができるのだ。
Variable A:Set. Inductive Vec : nat -> Set := | VNil : Vec O | VCons : forall n, A -> Vec n -> Vec (S n).
このベクトル型を使えば、コンパイル時に長さの整合性もチェックしてくれて、間違いがある場所を教えてくれる。コンパイルさえ通れば、OutOfBoundsExceptionのような実行時エラーは起こりえないことが保証される。
例えば、一般的にリストのhead関数は、引数が1以上の長さのときのみ定義でき、空リストの場合には値を返すことができない。しかし、このベクトル型を使えば、1以上の長さのリストのみで定義される安全なhead関数を作ることができる。
Definition head n : Vec (S n) -> A. intros n H; inversion H as [| m x _]. exact x. Defined.
*1
さらに、ベクトルの内積は同じ長さのベクトル同士でしか定義できないが、このような場合もベクトル型は便利だ。内積関数(inner_prod)を次のように実装することができる。
Definition inner_prod n : Vec Z n -> Vec Z n -> Z. intro n; induction n; intros v w. exact 0. exact (head _ v * head _ w + IHn (tail _ v) (tail _ w)). Defined.
*2
また、ベクトルのベクトルとしてm行n列の行列型を作ることができる。
Definition Matrix m n : Set := Vec (Vec Z m) n.
行列のかけ算は一方の行数ともう一方の列数が等しいときのみに定義されるが、それは次のように実装できる。
Definition mult_aux k m : Matrix k m -> Vec Z m -> Vec Z k. intros k m vs w; induction k. exact VNil. exact (VCons (inner_prod (map (head _) vs) w) (IHk (map (tail _) vs))). Defined. Definition mult k m n (vs:Matrix k m) (ws:Matrix m n) : Matrix k n := map (mult_aux vs) ws.
OutOfBoundsExceptionやInvalid_argumentエラーなどの仕組みをうれしいと思う人はいないだろう。依存型のような強力な型システムを使うことによって、実行時のエラーを防ぐだけでなく、開発者がプログラムの本質の部分だけを考えることができるようになるのである。
依存型はCoqやAgdaの便利な性質の一部であり、他にもいろいろできるのだが、依存型に関しては、Agdaは非常にうまくできている気がした。
Agdaは楽しいのでもっと触ってみよう。
*1:このようにCoqでは、型だけまず宣言して、あとからtacticを使いながら関数を構成することができる。しかし、Agdaはもっとすごくて、
head : Vec A (succ p) -> A
head x::xs = x
のように、Haskellっぽく書くことができる。コンパイラが自動的に空リストの場合が必要ないことを証明しているようだ。Coqでもこんなかんじに関数っぽく書きたいのだが、今のところどうやるのかわからない。
*2:ここも、Agdaなら
inner_prod nil nil = 0
inner_prod (x::xs) (y::ys) = x*y + inner_prod xs ys
のようなかんじにできる！Agdaすごい!
