プログラムを書いて証明しよう！ -- Coqを用いた形式証明の解説 --

2022年 Zli 秋の大LT スライド

Transcript

1. プログラムを書いて証明しよう！ Coqを用いた形式証明の解説 Zli 大LT 2022/10/15 sou7 / soukouki 1
2. sou7といいます 学部2年 Zli 次期副代表 GDSC(Google Developer Student Community) Aizu Lead プログラミング言語触ったりしてます Twitter : @sou7___ Github : @soukouki .　　　　　　　　　　　　　　　　　やぁ > 2
3. 今回話すこと なんでプログラムを書いたら証明できるの？ カリー・ハワード同型対応を通して、型と命題、コードと証明が関係している ことを、Haskellのコードを通して確認します。 Coqの証明って実際どんな感じなの？ Coqでどうやって証明をしていくのか、簡単な例を通して解説します。 今取り組んでいる証明 Coqってどこで使われてるの？ このCoqが、実際にどんな分野で活用されているのか紹介します。 3
4. 証明とプログラム、命題と型 Coqの根底となる理論として、カリー・ハワード同型対応があります。 論理の世界 プログラミングの世界 命題 型 証明 コード 4
6. 実際に見てみよう この命題を関数に落とすと (p -> q) -> p -> q という型を持つ関数(変数)を定義す ることになります。 modusPonens :: (p -> q) -> p -> q modusPonens hpq hp = hpq hp (P → Q) → P → Q 6
7. もうちょっと違う例で見てみましょう。 に対応する型は、 ((A -> B), (B -> C)) -> (A -> C) です。 syllogism :: ((a -> b), (b -> c)) -> (a -> c) syllogism (hab, hbc) ha = hbc (hab ha) (A → B) ∧ (B → C) → (A → C) 7
8. ド・モルガンの法則の一部は、こんなふうに書けます。 import Data.Void and_l :: (p, q) -> p and_l (hp, _) = hp and_r :: (p, q) -> q and_r (_, hq) = hq deMorgan :: (Either (p -> Void) (q -> Void)) -> ((p, q) -> Void) deMorgan (Left hnp) = hnp . and_l deMorgan (Right hnq) = hnq . and_r ¬P ∨ ¬Q → ¬(P ∧ Q) 8
9. じゃぁCoqだとどんなふうに証明するの？ これまではHaskellでの証明を見てきましたが、証明の割にとてもややこしいコードに なってしまいます。 そこでCoqは、タクティックと呼ばれる構文を使うことで、証明を簡単に書けるよう にしました。 Theorem ModusPonens (P Q: Prop): (P -> Q) -> P -> Q. Proof. move=> Hpq Hp. (* Proof.からQed.までの3行がタクティック *) apply Hpq. apply Hp. Qed. (このコードはSSReflectのタクティックを使っているため、実際にはSSReflectをイン ポートする必要があります。) 9
10. 集合論をCoqを使って学ぶ 最近はCoqを使って集合論を学んでいます。 1. 概念や定理をじっくり学べる Coqを使って形式化することで、「その定理が表していることは何か」を考えら れます。 2. 証明の是非を判断できる 数学の証明は合っているのか、間違っているのかを判別するのが難しいです。 しかし、Coqを使えば、間違った証明を書けばエラーが出るので、正しい証明を 書けます。 10
11. (* (2.3)' *) Theorem subsets_cap: forall A B C, C \subset A -> C \subset B -> C \subset A \cap B. Proof. move=> A B C HC_subset_A HC_subset_B x. split. - by apply HC_subset_A. - by apply HC_subset_B. Qed. (* (2.4)' *) Theorem cap_diag: forall A, A \cap A = A. Proof. move=> A. apply eq_subset' => x; rewrite -cap_and. - by case. - by split => //. Qed. 11
12. Coqがどんな分野で活躍しているか これまでCoqについて色々話してきましたが、実際にCoqが活躍している場所を紹介し ます。 1. 定理の証明の検証 2. 安全なソフトウェアの開発 12
13. 1. 定理の証明の検証 数学の証明の中には、いくつか「証明の正しさを保証できない」ものが存在します。 ABC予想 なんか他にもあるやろ そのような証明に対して、形式的な言語を使い機械的に検証することで、証明が本当 に正しいことを検証します。定理証明支援系で行われた形式証明として、以下のもの があります。 四色定理 奇数位数定理 この定理の証明のために作られたライブラリ(MathComp)が今も広く使われてい ます。 ケプラー予想 Coqと同じ定理証明支援系である、Isabelle/HOLを使って証明されています。 13
14. 2. 安全なソフトウェアの開発 プログラムがバグなく動くことを保証したいときに、どんな手段があるでしょうか。 1. ソースコードとにらめっこする 2. 型をつける => 例えばクイックソートなんかでは、型は合っていてもバグがあるかも・・・ (その条件式、本当に合ってる？) 3. テストを書く => 全パターンはチェックできない！ 4. 形式的に証明をする => ソースコードが仕様を満たしていることを保証できます！！ 14
15. まとめ おすすめの本・サイト 「Coq/SSReflect/MathCompによる定理証明」 https://www.morikita.co.jp/books/mid/006241 「ソフトウェアの基礎」 日本語版 https://www.chiguri.info/sfja/lf/toc.html 上の本を読み進めながらサイトの演習問題を解く流れが安定すると思います！ 参考文献 「計算と論理」配布資料 「カリー・ハワード同型対応」 https://www.fos.kuis.kyoto-u.ac.jp/~igarashi/class/cal21w/ch.pdf 15
16. 今回の内容 1. カリー・ハワード同型対応によって、定理と型、証明とプログラムが対応する 2. Coqを使った証明の雰囲気 3. Coqは数学の証明の正しさを保証したり、 プログラムの正しさを保証するのに使える(テストより強力!) 終わりに Coqとか形式証明とか触れるインターンがもしあれば教えてほしいです！ 16