书くネタが颁辞辩しかない
Download as pptx, pdf2 likes4,887 views
upcamp(私立?プログラミングキャンプ) 2012 東京大会 http://atnd.org/events/30833
书くネタが颁辞辩しかない
- 1. 书くネタが颁辞辩しかない upcamp 2012 にて
- 2. 自己紹介 ? http://qnighy.github.com/ を参照 ? いちねんせい ? 2008プログラミング組
- 3. やりたいこと ? 数学の証明を自然言語で書かなければい けないのは理不尽！ ? →Principia Mathematica 1+1の証明 (Wikipediaより) ここまで80ページ強の議論が必要
- 4. やりたいこと ? 今だったらこれをコンピューターでやれ るよね ? ↑正しさの検証も自動でできる！ ? ↑あわよくば、証明の一部は自動化
- 5. 目次 ? Coqとは何か ? Coqの根底にある理論 ? Coqで何ができるのか ? Coqをはじめる
- 6. Coqとは何か ? 純粋関数型プログラミング言語＆定理証 明言語 ? 静的型付け ? OCamlの影響を受ける ? OCamlで実装されている ? OCamlの製造元 INRIA が開発している ? 名前は計算機科学者 Thierry Coqandに由来 すると思われる
- 7. Coqの特徴 ? 停止する保証のあるプログラムしか書け ない (再帰の記述に関する制限) ? 証明モード (対話的にプログラムを組み立てるモード)
- 8. コード例 ? Karatsuba 乗算のコード ? このあと停止性証明が続く
- 10. Coqの特徴 ? 停止する保証のあるプログラムしか書け ない ? (再帰の記述に関する制限) ? →プログラムの正当性証明に用いられる
- 11. コード例 ? プログラムの正当性証明 ? (anarchy proof 30: Certified Compiler)
- 12. Coqの特徴 ? 停止する保証のあるプログラムしか書け ない ? (再帰の記述に関する制限) ? →プログラムの正当性証明に用いられる ? →数学の定理の証明に用いられる
- 14. コード例 ? √2は無理数であることの証明 ? (anarchy proof 6: Sqrt 2)
- 15. Coqの根底にある理論 ? Coqにおける「証明」とは？ ? → Curry-Howard 対応 証明 ： 命 題 プログラム ： 型
- 16. Coqの根底にある理論 ? Curry-Howard対応の例 ? 含意(AならばB): 関数 A -> B (Haskell) ? 連言(AかつB): ペア pair<A, B> (C++) ? 選言(AまたはB): Either A B (Haskell) ? 矛盾(⊥): 到達不能型 Nothing (Scala) ? 否定(Aでない): A -> ⊥
- 17. Coqの根底にある理論 ? では、こういうコードは？ ? Definition A : False := A. ? Aが定義できたら、矛盾が導けてしまう。 ? ↑ 無限ループの禁止
- 18. Coqの根底にある理論 ? Coqは停止するプログラムしか書けない ? これをどう保証するか？ ? _人人 人人人人人人_ > 型システムの出番 < ￣Y^Y^Y^Y^Y^Y^Y^Y￣
- 19. Coqの根底にある理論 ? 停止性を保証する型システム ? Simply Typed Lambda Calculus ? ↓ +polymorphism (型に依存した値) ? ↓ +type operators (型に依存した型) ? ↓ +dependent types (値に依存した型) ? Calculus of Constructions
- 20. Coqの根底にある理論 ? Calculus of Constructions (CoC) ? ↓ + 再帰等 ? Calculus of Inductive Constructions (CIC) ? このCICをCoqでは用いている ? CICと集合論のZFCは互換 ( CIC(i)→ZFC(i-2), ZFC(i)→CIC(i+1) )
- 21. Coqで何ができるの？ ? 数学サイド ? 有名なのは – ゲーデルの不完全性定理の証明 (公理系が多層化するので、形式的な言語で書 いたほうが議論しやすいと思われる) – 四色問題の証明 (四色問題は数学的証明部とコンピューターに よる探索部に別れる。Coqではこれを有機的 に結合できるため、証明の信頼性が高まる)
- 22. Coqで何ができるの？ ? プログラミングサイド ? プログラムを証明するという試みもいく つか行われている – Coq自体でプログラムを書く→他の言語へ出力 – C言語プログラムの証明：Frama-Cプラグイン – Javaプログラムの証明: Krakatoa – 独自の言語Why3MLで書いたプログラムの証 明 ? Zとかに比べるとまだ発展途上かも
- 26. Coqをはじめる ?
- 27. Coqをはじめる ? 日本語資料が少ない ? コミュニティーが大きくない ? 最後に、いくつかの参考資料を紹介して 終わります
- 28. Coqの資料 ? http://coq.inria.fr/ – Coq公式サイト ? プログラミング Coq – 女子大生によるCoqプログラミング入門 ? anarchy proof – 証明ジャッジ 練習用に使える ? あとは面倒くさいのでここを見て
- 29. コミュニティー ? 名古屋にいろいろあるらしい – Coq Party, Proof Summit …
- 30. 本 ? 本(英語) – Coq’art ? Coqの本らしい – TAPL ? 型理論の本
- 31. おわり ?