第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/

具体的には以下のことを定義した。

  • 標準出力へ出力するprint, println関数
  • 命令をつなげるセミコロン演算子
  • 依存型を使った型安全なprintf関数
  • natからOCamlのint、stringからOCamlのstringへの相互変換関数
  • Coqでのbool、sumbool、list、option型をそのままOCamlの型として使うための連携

迷路の試験問題を解いてみた

参考:人材獲得作戦・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の標準ライブラリを使えるようにする
  • Agdaでhello, world

Agdaのインストール

AgdaEmacs上で動作する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

ghcやemacsどころか、まだgccすらなかったのでたくさんインストールをがんばってもらった。

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.

1階命題論理でresolutionが成り立つ事を示す

まずAかBかで場合を分けて、Aのときは¬AかCかで場合分けすればできる。Aと¬Aが同時に成り立つとなんでも証明できてしまうということを利用しよう。排中律は別に必要なく証明できる。

Proposition p09 :
  forall A B C, (A \/ B) /\ (~A \/ C) -> B \/ C.
Proof.
intros A B C H; elim H; intros.
elim H0.
 elim H1.
  intros H2 H3; elim H2.
    apply H3.
 intros H2 _; right; apply H2.
intro H2; left; apply H2.
Qed.