4/23 第15回 Formal methods 勉強会

Formal Methods

目次

全国技術系勉強会マップにFM_Forumが紹介されました

今後毎年やっていきたいそうです。
勉強会のクロス検索サイトを開発しようとしているそうな。

普通のいわゆるIT系の勉強会はあんまり入ってないです。
雑誌に載せる都合上だと思われます。

「勉強会マップ読んで来ました」という方は・・・いなかった。
今後に期待。

Coqチュートリアル
  • 型のついた言語触ったことある人・・・全員OK

*** 形式手法2.0&証明付きDSL

  • 自然言語仕様だと機械検証できないからダメなんだな（あいまいだからとかいうわけでなく）

*** Coq入門

  • 目的
    • Coqの操作に慣れる
    • Coqのプログラミングについて知る
  • 定理証明系は、証明できる事柄には何にでも適用できる
    • 関数の定義Definition

定義は上書きできません。関数型言語の特徴。
Definition x := 1.
Definition x := 2.

coqtopではResetが使えるけど、coqIDEではできません。

nat -> nat -> nat (* nat -> (nat -> nat) *)
natを渡すと関数がかえってくる、という意味。

適用空白。うまく動かなかったら空白を入れよう。
scopeとして何を設定してるかによって、型の判断が変わる。

Check Set.
ってやるとTypeが帰る。

Eval computeのcomputeにはいろんな指定ができるよ。

引数ありのコンストラクタの例。
Definition And(b1 b2:Bool):Bool :=
match b1,b2 with

tru,tru => tru
_,_ => fls

end.
_は「それ以外」。

bool以外のand,or,negもあるよ。

unit型は何に使うか？値がないことを示す。

destructは場合分けをする。
simpl.はevalしてるみたいに計算してくれるよ。

Admittedされたものも証明の中で使えるけど、実体がないので実装にはならない。

  • 関数の中で_アンダースコアは使うべき？
    • 結局内部的には全部展開してるはず。

証明の流れとして、同じ流れが使えるのならセミコロンでつなげられます。
destruct b1; destruct b2; simpl; reflexivity.
パターンが使えなかった場合に特別なtacticをかます記述もできる。

なんでOなのか。識別子なので数字だと都合が悪い。
3とか表示されるのは、Coqが（人間に都合の良いよう）表示を変えてくれてる。

  • CoqIDEで日本語化けるときがあるよ。
    • utf-8でやってる限り動いてるみたい。

{struct n}という記述は、について再帰的に定義していることを示す。

ライスの定理
余再起、余帰納を使えば無限リストとかも書けます。
CoInductive,CoRecursion

CoqでCコンパイラを書いた場合、そのCコンパイラの生成するコードが無限ループしてもそれは良い。

Coqでは、任意の割り算を定義するのは難しい（整楚帰納法が必要）

(** 再帰関数の停止性 *)
Fixpoint add'(n m:nat){struct n}:nat :=
match n with
| O => m
| S n' => S (add' n' m) (* add'に直す *)
end.
  • 数値計算系の証明をするには？具体的な値を当てはめたらテストと同じだよなぁ。
    • 効率の良い関数と、間違いなくかける計算を比較する
    • 掛け算なら掛け算の公理を満たすことを証明するとか

mult.がmul関数と同じ実装になってる。(Print mult.)

  • 多相型

{A:Set}のところが多相型。

Definition cond{A:Set}(c:bool)(vt vf:A) : A :=
match c with
| true => vt
| false => vf
end.

@cond nat　とか具体的に指定もできる

Eval compute in (@cond nat false 2 3).

空リストの要素の型とか、推論しようがないものに使うことがある。

  • option型

null(C),option(OCaml),Maybe(Haskell)に対応してsumor(sum or)型がある。

prodはproduct。
(s:sum nat bool)は、natかboolの値を返す。

olastはそもそも空リストにolastするとNoneを返す.
リストの処理の場合は、nilの場合とリストの場合に分けて再帰処理する

all_trueの再帰の処理

|x::xs' => andb x (all_true xs')
end.
  • 証明の話

Propは真偽で場合わけできない（直観論理）。
プログラムを書く立場では排中律が役に立たないことがある。
排中律で証明できても、それをもとにプログラム（処理）を記述できないことがある。

計算機では、ゴールを仮定に近づけていく考え方で証明を進める。

仮定にゴールと同じものがある場合：assumption | exact | trivial
exactは既に存在する定理を使用するときに使う。
intros (implies 導入)
introsでは名前をつけよう。命名規則がCoqのバージョンによって変わることがある。
apply (implies除去)

仮定に/\を含む場合

  • destruct pq as [p q].

ゴールに/\を含む場合

  • split

仮定に\/を含む場合

  • destruct pq as [p | q].

ゴールに\/を含む場合

  • left. または right.

否定を含む場合
Inductive False : Prop :=
となっている。そもそも値が存在しない。
ゴールが~Pの場合はintro.するとゴールがFalseになる。
仮定にFalseが存在する場合は、elim H.を実行すると証明終了。

~A
のとき、
intro a.
とすると、
a:A
-----
False

これは、~Aというのは、AからはFalseが導ける、ということ。
だからa導入によって、Falseがゴールになる。

否定をunfold not.で展開してしまう例。

Section UnfoldNot.
Variables A : Prop.

Theorem ex4_2 : ~~~A -> ~A. 
Proof.
unfold not.
intros.
apply H.
intros.
apply H1.
assumption.
Qed.

End UnfoldNot.
  • 証明とは

仮定=引数
ゴール=戻り値

  • 命題論理

Javaでも証明できるよ（型レベルプログラミング）。
c++のテンプレートプログラミングがそんな感じ。

  • 述語論理

forall,exists
Coqは高階述語論理。TrueやFalseを返す関数ならば良い。

  • forall -> intros
  • 仮定にexists -> destruct.

= の証明

  • SearchAbout ____.
  • 帰納法
    • むやみにintroしないほうがいい。
      • forall l2 ...という、任意の値について成り立つ式にすることができる。
  • 依存型

引数として証明を要求する。
Definition sub(m n:nat)(H:le n m) : {x:nat|x+n=m}.
コンパイル時にチェックできる。

  • generalize dependent m. 仮定をゴールに引き戻せる。
  • eapply.引数を推論してくれるapply.
  • 関数定義時には、Qedではなくて、Defined.で終了する。
  • OCamlにextractionすると、Obj.magicとか使う関数になる。Obj.magicは型を無視してキャストする。
  • Coqでの関数と証明を扱う場合
    • refine tacticも使える。
  • 本コースで扱わなかった事

omega。ライブラリ。inversion,refine。tactic開発。型クラスやModule。

  • 本コースは、大学のCoq教程4,5週間分くらいになってます。
Coqで数学の証明
  • 数学の証明をするのは結構大変です。
    • 実数の値にたいしての証明とか。
9月25日定理証明系イベントをやります
  • 詳細がまったく決まっていない
    • 趣旨
    • 背景
      • ICFP2011,CUFP2011が、相次いで東京にて開催されるので、そのついでに。
    • 状況
      • 豆蔵会場仮押さえした。
Monad攻略戦

次回やります！

QCon Tokyo 2011発表振り返り

飲み会にて。