「プログラミング」と「数学」の関係 〜カリー・ハワード同系対応と定理証明支援系Coq〜

2024-02-16 Mariconf Zli 合同LT
2024-02-27 TOGATTA Server LT
で行ったLTスライドです

Transcript

1. 「プログラミング」と「数学」の関係 〜カリー・ハワード同系対応と定理証明支援系Coq〜 2024-02-16 Mariconf Zli 合同LT 2024-02-27 TOGATTA Server LT
2. 自己紹介 ActivityPub/Misskey: @sou7@misskey.io twitter: @sou7___ アンダーバー3つ 好きな言語: Coq Ruby 学部3年 進級確定 2
3. 最近やっていること Coqで集合論の証明(後述) C言語コンパイラーづくり Rui Ueyamaさんの「低レイヤを知りたい人のためのCコンパイラ作 成入門」を読んでいます。 現在ステップ21まで進んでいて、そろそろ真面目に型の宣言を解析 しないといけないところです。 3
4. C言語クイズ 次の変数の型はどんな型になるでしょうか？ int func() { // ① int *a[3]; // ② int (*b)[3]; // ③ int (**c)(); } 4
5. 正解 int func() { // ① int *a[3]; // Array<Pointer<Int>> // ② int (*b)[3]; // Pointer<Array<Int>> // ③ int (**c)(); // Pointer<Function<Int>> } 5
6. 「関数」と「ならば」の関係 Floatを受け取ってIntを返す関数 toInt : Float -> Int Intを受け取ってStringを返す関数 toString : Int -> String これらを使って、Floatを受け取ってStringを返す関数を作るとしま す。 6
7. toString(toInt(float_value)) というふうに、関数を合成すること で実現できます。 7
8. 大雨と道路の例 大雨が降れば、道路が浸水する 大雨 -> 浸水 道路が浸水すれば、道路が渋滞する 浸水 -> 渋滞 これらを使って、大雨が降れば、道路が渋滞するということを証明で きます。 8
9. 「関数」 Aを受け取ってBを返す関数 f : A -> B Bを受け取ってCを返す関数 g : B -> C 組み合わせることで、Aを受け取ってCを返す関数 g(f(x)) を作れる 「ならば」 AならばB H1 : A -> B BならばC H2 : B -> C 組み合わせることで、AならばC を証明できる 「関数」と「ならば」どこか似ているような気がしませんか？ 9
10. 実際にこれらは深い対応関係があり、カリー・ハワード同系対応と呼 ばれています。 ハスケル・カリーさんとウィリアム・アルヴィン・ハワードさんが、 1930-60年代にかけて発見しました。 今回はこの対応関係について話していきます。 10
11. 「構造体」と「かつ」の関係 構造体は、複数のデータをまとめたものです。例えば、以下の例では x座標とy座標をまとめて、Pointという構造体を定義しています。 struct Point { int x; int y; }; 11
12. AかつBと言ったとき、AとB が同時に成り立つことを意味 します。 例えば かつ な らば、 は第一象限にあ ります。 12
13. 「構造体」 x座標とy座標を同時に持つ構造体 struct Point { int x; int y; } 「かつ」 条件Aと条件Bが同時に成り立つ x > 0 かつ y > 0 「同時に持つ」と「同時に成り立つ」も対応しているように見えませ んか？ 13
14. 「構造体」と「かつ」の関係 実際にこれらも対応しています。 「同時に持つ」ような型は、取れる値の集合が各要素の集合の直積に なるので、直積型と呼ばれます。 14
15. 構造体の拡張「代数的データ構造」 「かつ」が「タプル型」に対応するのなら、「または」は何に対応す るのかも気になります。 15
16. 実は、構造体の拡張である、代数的データ構造と対応しています。 enum Result<T, E> { Ok(T), Err(E), } RustのResult型は、成功した場合の値 Ok(T) と、失敗した場合の値 Err(E) のどちらか一方を持ちます。 「どちらか一方を持つ」と「どちらか一方が成り立つ」のように、こ れらも対応しています。 取れる値の集合が各要素の集合の直和になるので、直和型と呼ばれま す。 16
17. 「再帰」と「帰納法」の関係 以下は再帰を使った階乗の計算の例です。 frac(n) は、nが0のとき1 を返し、それ以外のときは n * frac(n-1) を返します。 int fact(int n) { if (n == 0) { return 1; } else { return n * fact(n - 1); } } 17
18. 数学的帰納法 数学的帰納法は、以下のような形をしています。 1. が成り立つ 2. が成り立つならば、 も成り立つ これら2つが成り立つとき、全ての自然数 について が成り立つ と言えます。 18
19. 数学的帰納法のステップ2、「 が成り立つならば、 も 成り立つ」では、 の証明の中で、 が成り立つことを 呼び出しています。 証明の中で、自分自身を呼び出す・・・そう！これは再帰のテクニッ クと同じです！ 帰納法は再帰そのものなのです！ 19
20. 「プログラミング」と「数学」を紐付け る定理証明支援系 ここまで、「プログラミング」と「数学」には深い関係があることを 見てきました。 「プログラミング」には、コンパイラやIDEなど、多くの支援ツール があります。カリー・ハワード同系対応を使うことで、これらのツー ルを「数学」にも応用することができます。 20
21. プログラム風に書いた証明 AならばB H1 : A -> B BならばC H2 : B -> C H1とH2を使ったAならばC A -> C の証明 fun x => H2(H1(x)) これなら型検査などの「プログラミング」の道具を応用できそうで す！ 21
22. 定理証明支援系Coq プログラム風に証明を書くことで、証明を検証し、正しい証明かどう かを確かめることができます。 A_implies_C = fun (A B C : Type) (H1 : A -> B) (H2 : B -> C) => fun (x : A) => H2 (H1 x). AばらばBは H1 : A -> B BならばCは H2 : B -> C それらを使い、 fun (x : A) => H2 (H1 x) とすることで、AならばC を証明しています。 22
23. タクティックを使った証明 プログラム風に証明を書くのは難しいので、Coqでは普通、タクティ ックと呼ばれるコマンドをつかって証明を書きます。 From mathcomp Require Import ssreflect. Theorem a_implies_c A B C: (A -> B) -> (B -> C) -> (A -> C). Proof. move=> H1 H2 HA. apply H2. apply H1. exact HA. Qed. 23
24. Coqによる「かつ」「または」の証明 Theorem and_comm A B: A /\ B -> B /\ A. Proof. case. (* 仮定の A/\B を分解して、AとBを得る *) move=> HA HB. split. (* ゴールの B/\A を分解して、AとBを証明する *) - exact HB. - exact HA. Qed. 24
25. Theorem or_comm A B: A \/ B -> B \/ A. Proof. (* 仮定の A\/B を分解して、A->B\/A と B->B\/A を証明する *) case. - move=> HA. right. (* ゴールのB\/Aから右辺を選ぶ *) exact HA. - move=> HB. left. (* ゴールのB\/Aから左辺を選ぶ *) exact HB. Qed. 25
26. まとめ 「プログラミング」と「数学」には深い対応関係があります。 「プログラミング」と「数学」 「関数」と「ならば」 「直積型」と「かつ」 「直和型」と「または」 「再帰」と「帰納法」 Coqはこの対応関係を用いた、証明用のプログラミング言語 26
27. 最近やっていること 松坂先生の「集合・位相入 門」という本を、定理証明支 援系Coqによって形式化して います。 27