Coqで多変数多項式の簡約
変数全体の集合varを{}というように自然数の対応で与えられると考え、式expを以下のように定義する。
Inductive exp : Set := | Var : var -> exp | Const : nat -> exp | Binop : binop -> exp -> exp -> exp.
ここで binop型の値は二項演算子(binary operation)の種類(+または×)を表すものとして以下で定義されるものとし、定数項は簡単のため自然数(nat)に限るとする。
Inductive binop : Set := Plus | Times.
つまり、この定義のもとでは以下のように多項式が表現される。
多項式 | Coqでの表現 |
---|---|
Binop Plus (Var 0) (Const 1) | |
Binop Plus (Binop Times (Var 0) (Var 0)) (Binop Times (Var 1) (Var 1) |
各変数から値への対応 (var -> nat) を環境として、ある環境ctxにおける式eの意味を次で再帰的に与える。
Fixpoint expDenote (ctx: var -> nat) (e : exp) : nat := match e with | Var v => ctx v | Const n => n | Binop b e1 e2 => (binopDenote b) (expDenote ctx e1) (expDenote ctx e2) end.
そして式e1とe2の意味が同じという事を ctx, expDenote ctx e1 = expDenote ctx e2として考える事ができる。
ここで式eに対して、定数部分に関する部分的に簡単な形にする畳み込み関数を次で定義し、その健全性を示す。
Fixpoint constFold (e : exp) : exp := match e with | Var v => Var v | Const n => Const n | Binop b e1 e2 => match (constFold e1, constFold e2) with | (Const m, Const n) => Const ((binopDenote b) m n) | (e1', e2') => Binop b e1' e2' end end.
eを深さ優先に探索し、定数同士の2項演算を評価している。
ここで、この部分的な評価関数において、式eの意味が絶対変わらないことを証明する。
Lemma const_fold_preserved : forall e ctx, expDenote ctx e = expDenote ctx (constFold e). Proof.
induction e. reflexivity. reflexivity. intro ctx; simpl; rewrite IHe1; rewrite IHe2. destruct (constFold e1); destruct (constFold e2); reflexivity. Qed.
今回のネタはCPDTのExcercise 3.2 から取ってきた。CPDTはCoqでプログラムするときに必要な知識や便利な技を紹介していて非常にためになるので、Coqプログラミングをやりたい人にはぜひともオススメである。また、現在CPDTを勉強しているグループはFormal Method勉強会やProofCafe - coqグループなどあるので、参加してみてはいかがだろうか。
ソースコード全体と問題文は以下: http://ideone.com/kGLVw
第3回 Formal Methods勉強会に行ってきました。
第3回FormalMethods勉強会 : ATND
(via fm-forum @ ウィキ - トップページ)
場所は喫茶ルノアールというところの中にある会議室でした。
前半Alloyの話をid:kencobaさんが、後半はCoqの話をtmiyaさんがするという形式でした。13時から19時まで6時間でしたが興味深い話題がいろいろでて、あっという間という感じでした。
特に私が興味深いと感じたことは
- 国際規格のISO/ICE 15408 や ISO/ICE 61508 などの情報技術セキュリティ評価基準の内容にformal method(形式手法)という言葉が明記された
- Alloy検証機はシステム開発の上流工程で便利
- Coq の WHYツールは自動検証もラクラクできる
- 並列計算処理で検証を使った高信頼な開発ができたら注目されるかもしれない
- Alloy本の和訳プロジェクト進行中
- 形式手法は名古屋が熱い (自動車産業、組み込み系が活発だから)
懇親会のときにも感じましたが、高信頼なシステム開発のために より進んだ手法として形式手法に注目している方が多いように思いました。そういう意味ではCoqも形式手法の一つのツールとして特に実装面において非常に役に立つので効果的に使いたいですね。
懇親会後、3次会で一風変わった喫茶店(バー?)に行きましたが、そこでもPropとboolの違いなどについて熱く議論できて、最後まで非常に充実した時間を過ごすことができました。しかし、帰るためのバスがわからず、ご迷惑をかけてしまいました。一緒にバスを探してくださった tmiyaさん、mizoguchiさん、yshigeruさん ありがとうございました。
OCamlerのためのCoq便利モジュールを公開してみた
このBaseモジュールをインストールすれば、写真の用なコードを書くことが出来る。
ダウンロード: http://sourceforge.jp/projects/coqbase/
具体的には以下のことを定義した。
迷路の試験問題を解いてみた
参考:人材獲得作戦・4 試験問題ほか: 人生を書き換える者すらいた。
Lv4に評価されるためには、最短性の完全なチェックが必要だったのでCoqで証明してみた。
まず、accessiblesという関数を定義し、以下の性質を証明した。
ここでplengthはパスの長さを計る関数で、Path x pはpがxを起点としたパスであるという述語。endofはパスの終点を求める関数。
Fixpoint accessibles (start : node) (len : nat) : list path := match len with | O => (PUnit start) :: nil | S n' => div_equiv path_equiv_dec @@ (flat_map expand @@ accessibles start n') end.
この関数はstartから始まってlenの長さのパスが到達できる点(を終点とするパス)全体を返す関数を表現している。
Theorem soundness : forall x n p, In p (accessibles x n) -> Path x p /\ plength p = n.
この定理は「リスト(accesibles x n)のすべての元pはPath x pかつ長さがnである。」ということを言っている。
Theorem completeness : forall x p, Path x p -> exists p0, endof p = endof p0 /\ plength p = plength p0 /\ In p0 (accessibles x (plength p)).
これは「xからのパスpが存在するならば、pと同じ終点にたどり着き、pと同じ長さであるようなp0が(accesibles x (plength p))の中に存在する。」ということ。
停止しない処理をCoqで記述できないため、結果を無限リストとして定義し、OCamlに渡した。OCaml側では無限リストを順番に見ていき、解があれば出力する。
上記の定理より、パスの長さに関して同一視するとすべてのゴールへたどるパスは得られる無限リストに含まれており、無限リストは短い順に並んでいる。よって無限リストを順番にみた結果見つかった解が最短であることが保証される。
ソースコード全体は以下。
http://bitbucket.org/yoshihiro503/maze_solver/src/
実行結果
$ cat input.txt ************************** *S* * * * * * * ************* * * * * ************ * * * * ************** *********** * * ** *********************** * * G * * * *********** * * * * ******* * * * * * **************************
$ time ./run < input.txt ************************** *S* *$$$$$ * *$* *$ * $************* * *$*$$$* $$************ * *$$$ * $$$$$ * **************$*********** * $$$$$$$$$$$$$ * **$*********************** * $$$$$*$$$$$$$$$$$$$$G * * * $$$ *********** * * * * ******* * * * * * ************************** real 0m0.129s user 0m0.124s sys 0m0.000s
Coqで多重再帰のデータ構造を証明する
Coqでは一重の再帰的なデータは例えば次の様に定義できる。
Inductive list (A: Set) : Set := Nil | Cons (x: A) (xs: list A).
Coqでは再帰的データ型をInductiveコマンドで定義した場合、その型の他に list_ind というものがついでに定義される。
list_indは次の様な型を持っている。
Coq < Check list_ind. list_ind : forall (A : Set) (P : list A -> Prop), P (Nil A) -> (forall (x : A) (xs : list A), P xs -> P (Cons A x xs)) -> forall l : list A, P l
このlist_indは帰納法に関して非常に強力である。
リストを引数に持つような任意の述語Pに対して apply list_ind. をすればこのlistに関して構造的な帰納法で証明をすることができる。
また、そのための特別な induction という tactic さえ用意されている。
ただし、この *_ind は多重再帰のデータ型に関してはしょぼい物になってしまうという問題を発見した。*1
多重再帰のデータ型とは例えば相互再帰になっているものや次の様に再帰構造が入れ子になっているものだ。
module HTML. Inductive elem : Set := | PCDATA (_: string) | TAG (_: list elem).
このとき先ほどと同様に elem_ind が定義されるが、それは次の型になっている。
Coq < Check elem_ind. elem_ind : forall P : elem -> Prop, (forall s : string, P (PCDATA s)) -> (forall l : list elem, P (TAG l)) -> forall e : elem, P e
しかしこの形だとTAGの場合の帰納法の仮定で、小要素に関して帰納的に証明することができない。
この問題を解決するために以下の項を定義した。
Fixpoint elem_ind0 (P : elem -> Prop) (H1 : forall s : string, P (PCDATA s)) (H2 : P (TAG nil)) (H3 : forall e es, P e -> P (TAG es) -> P (TAG (e :: es))) (e : elem) : P e := match e as x return P x with | PCDATA s => H1 s | TAG es => list_ind (fun xs => P (TAG xs)) H2 (fun a l H => H3 a l (elem_ind0 P H1 H2 H3 a) H) es end.
ちょっと苦労したが、これで以下の型の項を得ることができた。これを使えばelem型の帰納法もばっちりだ。
Check elem_ind0 : forall P : elem -> Prop, (forall s : string, P (PCDATA s)) -> (P (TAG nil)) -> (forall e es, P e -> P (TAG es) -> P (TAG (e :: es))) -> forall e : elem, P e
*1:これはv8.2pl1時点の話。将来的にこの問題は改善するかもしれない。
Getting Started with Agda アグダを始めよう
Agda(Agda2.2.4)をインストールして hello worldプログラムを書いてみた。
OSのディストリビューションは最近リリースされた Ubuntu 9.10。
非常に簡単にインストールができたので、依存型erのみんなは Ubuntu 使うといいよ。
Agdaのインストール
AgdaはEmacs上で動作するagda-modeをインストールすれば使えるようになるみたいだ。
agda-modeはapt-getで簡単にインストールできた。
$ sudo apt-get install agda-mode
以下のパッケージが新たにインストールされます: agda-mode cpp-4.1 emacs emacs22-bin-common emacs22-common emacs22-gtk emacsen-common g++-4.1 gcc-4.1 gcc-4.1-base ghc6 haskell-mode libffi-dev libghc6-agda-dev libghc6-binary-dev libghc6-haskeline-dev libghc6-haskell-src-dev libghc6-mtl-dev libghc6-quickcheck2-dev libghc6-terminfo-dev libghc6-utf8-string-dev libghc6-xhtml-dev libghc6-zlib-dev libgmp3-dev libgmpxx4ldbl libncurses5-dev libstdc++6-4.1-dev zlib1g-dev
Agdaの標準ライブラリを使えるようにする
現時点でのAgda(Agda2.2.4)では標準ライブラリが一緒ではないみたいだったので、Agda本家からダウンロードした。
入手したライブラリを実際に使うためにはパスを通す必要がある。README.agdaに「(M-x customize-group RET agda2 RET)というEmacsコマンドを実行してね」と書いてあったのでそうしてみた。そこで、"Agda2 Include Dirs"という項目にライブラリのsrcというパスを絶対パスで指定すれば使えるようになった。
使い方はAgdaのコードで
import Data.Nat as N open import Data.List open import Data.String
とかいう風に書けばいいみたいだ。
Agdaでhello, world
じゃあ、早速Agdaでプログラムしてみよう!なんてったってAgdaはプログラミング言語だもんね。
文字列を標準出力に出力するプログラムhello.agdaは以下のように書ける。
module hello where open import IO main = run (putStrLn "Hello, あぐだworld!")
(C-c C-l)というコマンドを打てば、ソースコードに誤りがないか型チェックしてくれる。さらに、(C-c C-x C-c)コマンドでコンパイルすることもできる。
hello.agdaをコンパイルするとhelloという名前の実行ファイルができた。実行してみよう。
$ ./hello Hello, あぐだworld!
日本語もばっちりだ。こんにちはアグダ。こんにちは依存型。
ちなみにemacsを使わないコンパイラもあって、Ubuntuではagda-binというパッケージをapt-getすれば使えるようになる。
直観主義論理での二重否定除去と排中律の同値性
同値性を示すためにそれぞれの矢印を示した。論理パズルみたいな問題だが、¬を扱ういい練習問題だと思う。
Lemma p10_left : (forall A, ~~A -> A) -> (forall A B, (~B -> ~A) -> (A -> B)). Proof. intros. apply H. intro. elim (H0 H2). apply H1. Qed. Lemma p10_right : (forall A B, (~B -> ~A) -> (A -> B)) -> (forall A, ~~A -> A). Proof. intros. apply (H True A). intro. intro. elim H0. apply H1. apply I. Qed.