Hatena::ブログ(Diary)

kencobaの日記

2012-02-12

第18回Formal Methods勉強会

| 13:50

kencobaの与太話

  • Alloy Analyzerの話は、後ほど時間のあるときにしましょう。
  • Coq Tutorialやってます。
  • 数学基礎論の勉強もやってます。

Coq tutorial

話す内容は倍くらいあったんだけど、時間が足りなかったなぁ。

  • 次回は=を含む証明、帰納法の証明、Listの証明。
  • inversion使えると、初心者卒業かな。
  • 機能的定義
    • いろんな定義の仕方があるけど、Coqでは機能的な定義をするのが望ましい。
    • 証明が簡単になる。
  • 決定可能な述語
    • 必ず結果がどちらかに決まるのであれば、証明するのが望ましい。
  • 清楚帰納法の話はCoq Tutorialではできなかった。
    • 割り算の証明は難しい。
    • 特定の変数に対する帰納を証明できるようになる。
    • 帰納的証明にもっていくときは、自然数にマップする関数を作って証明すると楽。
  • 依存型の話もCoq Tutorialでは難しいかも。
    • 引数として証明を渡せる。
    • 関数と証明の統合。
  • Programコマンドを使うと、証明付き関数を作れる。
  • Notation, Type Class
  • 話さなかったことも、データは公開します。
  • Monadの定義
    • Record,Moduleでもできるよ。
    • Type Classだと型推論などもしてくれる。

次回あるなら、回数を増やしてやってくれないかな。

  • どっちかというと、Coq Tutorialで興味を持ってくれた人が、FM_Forumに来てくれないかな、と思ってます。

上級編、というと、人によって興味が分かれちゃうんですよね。

  • ツールの使い方なら菊地さんにssrefrectの話してもらうとか。
  • 8.4が出たら機能紹介してもいいかな。Language Updateのネタで話す機会がでるかも。

実際の問題を解きたい、というのがゴールにあるかも。

  • 結局、手続き型の言語の証明をしたい、ということになると、Separation Logicというのがある。
  • CoqライブラリにはSEPLOGがある。
  • もうちょっとヌルいところで、MLプログラム(ただし、破壊的代入有)なら、
    • CFML <- OCaml => Coq の証明課題生成ツール
    • Why3 これならVSTTEのcompetitionにでてくるのもできそう。
  • 依存型の理論を勉強するとか?
    • 値:Set (自己言及的な記述を許さない)
    • 命題:Prop
  • TAPLが好きなら、単純型付ラムダ計算Coqで実装とか。
  • Coq以外のツールとか
    • IsabelleはどうもCoqより強力?
    • OCL -> Isabelleとか
    • IsabelleからScala生成できる
    • Isabelleは集合ライブラリがある

1,2年目は Alloy,Coqを勉強した

  • 3年目は時相論理とかもいいのかな。UPPAALとか
  • 市販ツールなら、宣伝の機会と合わせて話を聞かせてもらうのもいいかも。
  • "Introduction to Bisimulation and Coinduction"
  • ssrefrectはまだCoq8.4版が出てない。
  • 自然演繹とか基礎の部分はあんまり丁寧にやっても・・・それよりチートシート方式の方がいいかも。
  • TAPLを読まずに「プログラミング言語の基礎概念(五十嵐)」という手もあるかも。

Why3

  • Why3のintは無限。
  • 使いこなすには、適当な課題を見つけてきて課題を解く。
  • ライブラリを作るとか。
  • 実際のコードでは、ループ不変式を上手く決定するのが難しい。
  • Bもループ不変式をやるのが難しい。

Krakatoa

  • Why3より(生成されたコードが)すごいことになってる。

今年の目標

  • Why3は、VSTTEの問題を解くところから挑戦
    • 次回VSTTEを解こう!
  • TPP参加?

Coqその他

  • Implicit Argumentsで指定する[A]とAの違いは?

Alloy Analyzer

assert ReformulateNonEmptinessOK {
	all r: univ->univ |
		some r iff (some x, y: univ | x->y in r)
	}

check ReformulateNonEmptinessOK

assert ReformulateTransitiveOK {
  all r: univ -> univ |
    (r.r in r) iff (all x,y,z :univ | x -> y in r and y -> z in r implies x -> z in r)
    //(all x,z :univ | some y :univ | x -> z in r implies x -> y in r and y -> z in r) //駄目な例
  }

check ReformulateTransitiveOK

assert ReformulateIrreflexiveOK {
  all r: univ -> univ |
    (no iden & r) iff (all x: univ | x -> x not in r)
  }

check ReformulateIrreflexiveOK

assert ReformulateSymmetricOK {
  all r: univ -> univ |
    (~r in r) iff (all x, y: univ | x -> y in r implies y -> x in r)
  }
check ReformulateSymmetricOK

assert ReformulateFunctionalOK {
  all r: univ -> univ |
    (~r.r in iden) iff
//    (all x,y :univ | y -> x in r implies x -> y in r)
    (all x,y1,y2:univ | x -> y1 in r and x -> y2 in r implies y1 = y2)
  }
check ReformulateFunctionalOK

assert ReformulateInjectiveOK {
  all r: univ -> univ |
    (r.~r in iden) iff
      (all x1,x2,y :univ | x1 -> y in r and x2 -> y in r implies x1 = x2)
  }
check ReformulateInjectiveOK

assert ReformulateTotalOK {
  all r: univ -> univ |
    (univ in r.univ) iff
    (all x :univ | some y :univ | x -> y in r) 
  }
check ReformulateTotalOK

assert ReformulateSurjectiveOK {
  all r: univ -> univ |
    (univ in univ.r) iff
    (all y :univ | some x :univ | x -> y in r)
  }
check ReformulateSurjectiveOK

A.1.3 (a) sibling
  • 同じ親を持つ子供をunivとする
  • この間の関係を兄弟関係rとする
    • 非空的:1人以上子どもがいれば、兄弟関係は存在する(自分は自分の兄弟)
    • 対称的:自分が相手の兄弟ならば、相手は自分の兄弟
    • 推移的:AがBの兄弟で、BがCの兄弟なら、AはCの兄弟
    • 非反射的×:自分は自分の兄弟としているので、反射的
    • 関数的×:「私の兄弟」は2人以上いて良い
    • 単射的×:私のことを「兄弟です」という人が2人以上いて良い
    • 全域的:全員が、全員の兄弟
    • 全射的:全員が、全員から兄弟と呼ばれる
  • 兄弟関係難しいよ。法律的?生物学的?数学的?
  • そもそもここでいう集合{r:univ->univ}は「すべての人の関係」?「ある兄弟関係」?
  • -> rが何を指しているかを言わないと答えられない?
  • 日本的に「自分は自分の兄弟」を認めないと・・・対称律と推移律をみたさないので反例がでる。
  • どう定義するか、という問題。Alloyなら反例が出て終わり、だけど、Coqだと矛盾が出たら大変なことになるね。
  • 多義性のある言葉をどう扱うか。
    • 意味が複数あるとまずいから、一意になるようにしてるんでしょうね。
    • 法律だったら?基本的な権利や義務はかなり厳密に書いてある。
    • 参考「アニメキャラが行列を作る法律相談所」
    • 法律を機械的に処理する研究してる人もいる
    • アリストテレスの「弁証論」
A.1.3 (b) links
  • これはスター型接続じゃないかな。
  • 双方向通信を認めるのか?
  • サーバクライアントじゃないよ。スター接続の中心もノードも全部「ホスト」
    • 非空的:少なくとも1つ、ホストがある。
    • 推移的×:別に必ず中継できる、としなくても良い。
    • 非反射的×:さすがに自分自身につながらないのは変な気がする。
    • 対称的×:AからBにつながるけど、BからAにつなげないのはアリ。
    • 関数的×:xを1個決めたらyが1個決まる?自分が複数の人につながっていてよい。
    • 単射的×:クライアント1と2はどちらも1台のサーバにリンクしている。
    • 全域:孤立してるノードはない。
    • 全射的:どこかから繋いでもらってる。
A.1.3 (c) contains
  • univ = {Dir + File}とする?
    • 非空的×:ディレクトリの中にファイルがない、こともある。
    • 推移的:Dir->Dir->Fileという構成があってよい。
    • 非反射的:自分は自分を含まない。(Dir1->Dir1とか、File1->File1、というのはない)
    • 対称的×:Dir->Fileとしたとき、FileはDirを「contains」してない。
    • 関数的×:Dir->{File1,File2}となっていてよい。
    • 単射的×:Dir->{File1,File2}となっていてよい。
    • 全域×:Fileは何も指さないので。
    • 全射的×:ルートをcontainsするものがないので。
A.1.3 (d) group
  • これってcontainsと何が違うの?
  • 要素 -> Groupか?これを決めないと関数的、単射的が判断できない。
  • ルートが無くてもいいということか。
  • ここではグループの階層は認めていないようだ。
  • グループは図的要素なの?グループっていうのがピンとこないなぁ。
  • グループ=図的要素の部分集合。
    • 非空的×:要素が一つもない、ということもある。
    • 推移的?:グループの階層は絶対ない。のだが、そもそも推移律の仮定が成り立たないので、「推移的」と言ってもよいのでは?推移律は成り立つが、推移的ではない。
    • 非反射的:自分は自分を含まない。
    • 対称的×:図形要素がグループを含む、ことはない。
    • 関数的:一つの要素は、選択グループに入るか、非選択グループに入るか、のどちらか。
    • 単射的×:2つの要素が、同時に一つのグループに所属してよい。
    • 全域:全ての要素が、必ず選択か、非選択のどちらかになる。
    • 全射的×:たとえば全部の要素を選択すると、非選択に所属する要素はなくなるので、全射ではない。

tMiyatMiya 2012/02/13 18:22 Coq で解きなおしてみました。
http://study-func-prog.blogspot.com/2012/02/coqalloy-properties-of-relation.html