型について

slide.md

型と証明とプログラム

今回の話

• プログラムの「型」
• 論理学の話
• C言語がわかれば良い
  • Haskell が別れば尚良い
• お手柔らかに

型とは

• int とか char とか
• プログラムの値に意味を与えるタグ
  • ビット列「01000101」
    • 整数型 → 69
    • 文字列型 → E

型付け

• 値に型を付ける作業のこと
• 動的型付け、静的型付け
  • コンパイル時に型付けするのが静的
• 型に関する言語処理系の機構 → 型システム
• 型検査機 → 不正な型付けを防止する
  • int a = "hogehoge"; // エラー
  • printf(2912312); // エラー

いろいろな型と表記

• A: 型 A
• A→B: Aを受け取りBを返す関数の型
  • (A→B)→C, ((A→B)→C)→D ...
• A×B: AとBの直積(product)
  • AとBのペア・タプルともいう
  • Aの値とBの値両方を保持
• A+B: AとBの直和(union)
  • Aの値かBの値を保持

数理論理学

• 推論を記号的・形式的に処理する学問
  • 「ソクラテスは人間である」 仮定1: P
  • 「人間ならば死ぬ」 仮定2: P → Q
  • 「ソクラテスは死ぬ」 結論: Q
  • P, P → Q |- Q
• 推論を連ねたもの：証明・導出
  • 推論のルールの体系：推論規則

数理論理学の表記

• A 命題 A
• A → B 「AならばB」という命題
• A ∧ B 「AかつB」という命題
• A ∨ B 「AまたはB」という命題
• ¬ A 「Aの否定」という命題

Curry-Howard 対応

• 「型」と「命題」 「証明」と「プログラム」(型付きλ計算の項)がそれぞれ対応
• 証明したい定理の命題を型に翻訳
• 型に合わせてプログラムを書けば、それが「証明」となる
• 何が嬉しいか？
  • 証明の正当性を型検査機がチェックしてくれる

CH対応関係

論理	型
A	A
A → B	A→B
A ∧ B	A×B
A ∨ B	A+B
¬ A	A→Void

証明のための言語

• Coq, Agda, ATS ...
• 関数型プログラミングをベース
• 定理証明系や証明支援系と言われる
• 算術の証明(整数や実数)も出来る
  • ある程度の自動定理証明もしてくれる
• 四色定理がCoqで(再)証明された(2004)

ソフトウェアテスト

• ある関数・機能を実装した
• それが正しく動くか確認したい：デバッグ
  • 幾つかの入力に関してチェック
  • コーナーケース(際どい入力に関してチェック)
  • すべての入力を網羅できない場合が多い
• ソフトウェアテストでは、欠陥が存在することを示すことはできるが、欠陥が存在しないことは証明できない。

ソフトウェア証明

1. 実装したい関数・機能が満たすべき条件を考える
2. 関数・機能を実装する
3. 実装したものが先の条件を満たしているか証明する

• 論理的に欠陥のないプログラムであることが示せる
• 「絶対にバグのないプログラムが作れる」
  • …条件の設定が妥当であれば
  • (そもそも型検査機がバグってるとダメ…)

実用例

• CompCert
  • Coqにより証明が付けられたC言語のコンパイラ
• 脆弱性の発見
  • OpenSSLの脆弱性(CVE-2014-0224)
  • CoqでSSLを実装している際、安全性に関する条件をOpenSSLが検査していないことがわかった

話せなかったこと

• 依存型について
  • 値に依存する型
• 直観論理について
• Code Extractionについて
• Curry-Howard-Lambek対応: 型-論理-圏の関係
• 厳密な話

まとめ

• 型と命題、プログラムと証明が対応
• プログラムを書くことで証明ができ、処理系がその正当性を検査してくれる
• プログラムに証明を付けることによって欠陥のないプログラムであることが示せる
• 論理学的に考え抜くことで健全なプログラムを書き健全な人生を送ろう