第19回Formal Methods勉強会

FM_Forum

4月以降のやりたいこと

参加者を増やしたいなぁ
  • 勉強会でシリーズ化して「話すこと」をあらかじめ広告しておく。
    • Software Foundation(by 候補いなければ、_tmiyaさん)
    • 「プログラミング言語の基礎概念」毎月1章で1年(by 候補いなければ、_tmiyaさん)
    • Alloy演習問題の実施計画(by kencoba)
  • Coq
    • Software Foundation和訳をネタに分割開催する?
      • Coq入門って感じじゃない・・・
    • 巷にはCoqの資料はたくさんある。
    • あとはだれかが「講師やります」って手をあげるだけじゃないの?
    • 毎回これをやりますというネタをあらかじめ出しておくといいかも。
      • 4回分先に計画するとか。
  • Alloy
    • 今は演習を毎回勉強会でやってる。
  • 「プログラミング言語の基礎概念」
    • これをCoqに翻訳しながら読むっていうネタがあるか。
    • 本に載ってない演習課題がある。
    • 全10章。毎回コツコツやるか。
  • Coq,Alloy以外の何か
    • MAUDE
    • Bisimulation
    • Modelica
      • QCon Tokyo 2012でお話があるから、フィードバックしましょう。
その他
  • 勉強会の取材のお話は?
    • まだ行動に移してないや。
    • シリーズ化して勉強会やるときには宣伝したい。
  • 東京のTAPLは
    • sub typingまで終わった。

Coqセミナー振り返り

  • 盛りだくさんでした。
  • EDUBASEくらうどのキーボード設定。ハードとソフトで違ってたよ。
  • 受講者の様子
    • ほとんどが関数型言語知ってる。
    • 半数が定理証明系知ってる。
  • injectionタクティック
    • 大抵inversion H.を使ってしまう。(等式の左右が同一のコンストラクタのとき)
  • 1.6.2 の b = (r1 + e - r2) っていう不変条件が良くわからん。
    • 間違ってるんじゃないか?会計の話が良くわからんかった。
  • Recordの要素には型が書けるということは、命題も書けるということ。
    • 命題も書けるなら不変条件もRecord自体に書ける。
  • 2.1.1 {measure length xs}は削除。
    • 停止性がはっきりしないときは、Functionコマンドで定義する。
    • 証明をしたものが関数として呼べるようにするのに、Defined.を使う。
  • CoInductive
    • Inductiveなコンストラクタ
      • A -> A -> list A
    • CoInductiveなコンストラクタ
      • list A -> A -> A
      • CoInductiveの証明は難しかったりする。
    • sig型は、Haskellのリスト内包表記とは違うよ。{x : A | P x}は、xという値と、Pという命題のタプルだよ。

ヒルベルト流公理系をCoqで証明する。

  • Hint Constructors で試してみたけどだめだった。
    • 公理の数を減らすとか?
    • Maudeでやってみるか。

Coqで様相論理

  • "Metareasoning for multi-agent epistemic logics"
  • Coqでの解法

http://ideone.com/s7UJa

論理学の参考

Alloy本演習問題続き

A1.3 (e) sameGroup

編集中にセッションが切れた・・・

A1.4
assert union {
  all s: set univ, p, q: univ -> univ |
    s.(p + q) = s.p + s.q
  }
//check union for 4

/*
等式の左辺は、集合と「関係の差」を結合している。
右辺は、集合同士の差になっている。
*/
assert diff {
  all s: set univ, p, q: univ -> univ |
    s.(p - q) = s.p - s.q
  }
//check diff for 2

assert inter {
  all s: set univ, p , q: univ -> univ |
    s.(p & q) = s.p & s.q
  }
check inter for 2
次回はA1.5から!