Pixel Pedals of Tomakomai

北海道苫小牧市出身の初老の日常

トップ > 技術 > 第16回FormalMethods勉強会に行ってきた

第16回FormalMethods勉強会に行ってきた

技術

「Monad攻略戦」と聞いたので、参加してきました。

Type Class in Coq / @tmiya_ さん

  • On Understanding Types, Data Abstraction, and Polymorphism
    • universal Polymorphism 個別実装なし
      • parametric : ML系の多層型
      • inclusion : サブタイプ、継承
    • ad-hoc Polymorphism 個別に実装が必要
      • overloading 名前が同じだが無関係
      • coercion 期待される型に自動で変換
    • 今日の話は、ad-hoc の方
  • Hask圏におけるモノイド対象
  • Coqでは、型クラスとして定義できる
    • M:Type -> Type, 公理もモナド型に含められる
      • left_unit, right_unit, assoc を公理とする
    • >>=, と do は Notation で定義可能
  • 一番簡単なモナド id'
    • 【演習】return' と bind を定義後、Proofモードでモナド測を証明する
    • 最後はDefined で閉じる(Qed だと、内部が見えなくなるらしい)
  • Maybe モナド (Coqではoption型のこと)
    • 【演習】同様に証明
    • 【演習】None >>= (fun x => Some (x + 1)) を実行してみる → None になる
  • Listモナド (flat_map を使う)
    • 【演習】同様に証明
  • MonadPlus ・・・ :> にてMonadを拡張。
  • MaybePlus(Maybeをmonadフィールドに持つ)
    • 【演習】MonadPlus測の証明
  • 「@」は明示的に型を指定するの意
  • 同様に、ListPlus
  • 継続モナド
    • CPS変換は、(A->R)->R。Rを⊥とすると、¬¬Aのこと。
  • eta_expansion → f = (fun x => f x)
  • extensionality → functional_extensionality により定義。
    • (forall x : A, f x = g x) -> f = g 外延性
  • まとめ : Type ClassはJavaのインタフェースのようなもの。公理を入れられるのが強力。

Coq への道 - 道なかば編 / 佐藤 大輔さん

  • 初めてのCoq (intros、apply などなど)→ さっぱりわからない
  • 証明とは？ → 公理 Pi(i = 1, 2, ...) と 推論規則
    • 例: 星形の頂点の角度の和は180度
    • Coqの証明は、公理の列には見えない・・・
    • 公理群を操作しているのではないか
    • 指摘『「公理」ではない*1』
  • 証明の手順
    • 公理や定理、推論規則を適用する
    • よく使われるtacticsの紹介 → intro(s?), split, right, left, apply, rewrite, destruct ,unfold, assert, replace, exact, assumption, reflexivity, exists
    • split 連言の分離, right 宣言の選択, apply 三段論法, rewrite 置き換え
    • destruct 仮定の分離, unfold 定義の展開, assert レンマの導入, replace A with B 変数の導入
    • exact 前提とゴールが一致, reflexivity A=Aの形
  • Coqの難しさ
    • 天才幼稚園児に数学を教える気分 → 実数における100<>0も厳密な証明が必要
    • 補足『ユークリッド幾何はライブラリがあるが、壮大』
  • 例: 調和級数が発散することの証明 (未完成)
    • ∞の定義がない → 補足『∀n, ∃N, x > N → P x > n』
    • 自然数と実数が混ざっている
    • Function は証明しにくい
      • 補足『Function より帰納的に定義するといいかも。』
    • 微積がCoqでは使えない(微分のライブラリはあるけど積分が見つからない)
  • 数列の全要素が正であることの証明ができてない
    • 補足『P 1 -> ((∀n, P(div2 n)→P n)→∀n, P n みたいな帰納法の方が合いそう』
    • 補足『Rsigma は使えないのか。級数のライブラリ。』
  • 補足『Coqのライブラリサイトはしばしば落ちるので、DLしておいた方がよい』

monads.clj / @kencobaさん

ProofSummit2011のお話

ProofSummit2011にどなたに登壇して頂きたいか、など。

合わせて読みたい

*1:premises