Upgrade to Pro
— share decks privately, control downloads, hide ads and more …
Speaker Deck
Features
Speaker Deck
PRO
Sign in
Sign up for free
Search
Search
「プログラミング」と「数学」の関係 〜カリー・ハワード同系対応と定理証明支援系Coq〜
Search
soukouki
March 13, 2024
1
86
「プログラミング」と「数学」の関係 〜カリー・ハワード同系対応と定理証明支援系Coq〜
2024-02-16 Mariconf Zli 合同LT
2024-02-27 TOGATTA Server LT
で行ったLTスライドです
soukouki
March 13, 2024
Tweet
Share
More Decks by soukouki
See All by soukouki
自作Cコンパイラ 8時間の奮闘
soukouki
0
950
定理証明支援系Coq(セキュリティキャンプLT会)
soukouki
1
130
Coqで選択公理を形式化してみた
soukouki
0
180
型クラスと依存型のカルパッチョ、代数的構造を添えて
soukouki
2
470
Coqのコントリビューターになった話
soukouki
0
150
次に流行る※プログラミング言語「Lean」
soukouki
2
1.4k
証明しながらプログラミング! - タクティックによるCoqプログラミング
soukouki
0
220
帰納型とパターンマッチングの紹介
soukouki
0
120
ステータスバーに歌詞を表示させてみた!
soukouki
0
110
Featured
See All Featured
Building Your Own Lightsaber
phodgson
102
6.1k
Writing Fast Ruby
sferik
626
61k
[RailsConf 2023 Opening Keynote] The Magic of Rails
eileencodes
28
9.1k
Build The Right Thing And Hit Your Dates
maggiecrowley
32
2.4k
What’s in a name? Adding method to the madness
productmarketing
PRO
22
3.1k
Agile that works and the tools we love
rasmusluckow
327
21k
Speed Design
sergeychernyshev
24
580
No one is an island. Learnings from fostering a developers community.
thoeni
19
3k
Fight the Zombie Pattern Library - RWD Summit 2016
marcelosomers
231
17k
RailsConf 2023
tenderlove
29
880
Creating an realtime collaboration tool: Agile Flush - .NET Oxford
marcduiker
25
1.8k
A better future with KSS
kneath
238
17k
Transcript
「プログラミング」と「数学」の関係 〜カリー・ハワード同系対応と定理証明支援系Coq〜 2024-02-16 Mariconf Zli 合同LT 2024-02-27 TOGATTA Server LT
自己紹介 ActivityPub/Misskey: @
[email protected]
twitter: @sou7___ アンダーバー3つ 好きな言語: Coq Ruby 学部3年
進級確定 2
最近やっていること Coqで集合論の証明(後述) C言語コンパイラーづくり Rui Ueyamaさんの「低レイヤを知りたい人のためのCコンパイラ作 成入門」を読んでいます。 現在ステップ21まで進んでいて、そろそろ真面目に型の宣言を解析 しないといけないところです。 3
C言語クイズ 次の変数の型はどんな型になるでしょうか? int func() { // ① int *a[3]; //
② int (*b)[3]; // ③ int (**c)(); } 4
正解 int func() { // ① int *a[3]; // Array<Pointer<Int>>
// ② int (*b)[3]; // Pointer<Array<Int>> // ③ int (**c)(); // Pointer<Function<Int>> } 5
「関数」と「ならば」の関係 Floatを受け取ってIntを返す関数 toInt : Float -> Int Intを受け取ってStringを返す関数 toString :
Int -> String これらを使って、Floatを受け取ってStringを返す関数を作るとしま す。 6
toString(toInt(float_value)) というふうに、関数を合成すること で実現できます。 7
大雨と道路の例 大雨が降れば、道路が浸水する 大雨 -> 浸水 道路が浸水すれば、道路が渋滞する 浸水 -> 渋滞 これらを使って、大雨が降れば、道路が渋滞するということを証明で
きます。 8
「関数」 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
実際にこれらは深い対応関係があり、カリー・ハワード同系対応と呼 ばれています。 ハスケル・カリーさんとウィリアム・アルヴィン・ハワードさんが、 1930-60年代にかけて発見しました。 今回はこの対応関係について話していきます。 10
「構造体」と「かつ」の関係 構造体は、複数のデータをまとめたものです。例えば、以下の例では x座標とy座標をまとめて、Pointという構造体を定義しています。 struct Point { int x; int y;
}; 11
AかつBと言ったとき、AとB が同時に成り立つことを意味 します。 例えば かつ な らば、 は第一象限にあ ります。 12
「構造体」 x座標とy座標を同時に持つ構造体 struct Point { int x; int y; }
「かつ」 条件Aと条件Bが同時に成り立つ x > 0 かつ y > 0 「同時に持つ」と「同時に成り立つ」も対応しているように見えませ んか? 13
「構造体」と「かつ」の関係 実際にこれらも対応しています。 「同時に持つ」ような型は、取れる値の集合が各要素の集合の直積に なるので、直積型と呼ばれます。 14
構造体の拡張「代数的データ構造」 「かつ」が「タプル型」に対応するのなら、「または」は何に対応す るのかも気になります。 15
実は、構造体の拡張である、代数的データ構造と対応しています。 enum Result<T, E> { Ok(T), Err(E), } RustのResult型は、成功した場合の値 Ok(T)
と、失敗した場合の値 Err(E) のどちらか一方を持ちます。 「どちらか一方を持つ」と「どちらか一方が成り立つ」のように、こ れらも対応しています。 取れる値の集合が各要素の集合の直和になるので、直和型と呼ばれま す。 16
「再帰」と「帰納法」の関係 以下は再帰を使った階乗の計算の例です。 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
数学的帰納法 数学的帰納法は、以下のような形をしています。 1. が成り立つ 2. が成り立つならば、 も成り立つ これら2つが成り立つとき、全ての自然数 について が成り立つ
と言えます。 18
数学的帰納法のステップ2、「 が成り立つならば、 も 成り立つ」では、 の証明の中で、 が成り立つことを 呼び出しています。 証明の中で、自分自身を呼び出す・・・そう!これは再帰のテクニッ クと同じです! 帰納法は再帰そのものなのです!
19
「プログラミング」と「数学」を紐付け る定理証明支援系 ここまで、「プログラミング」と「数学」には深い関係があることを 見てきました。 「プログラミング」には、コンパイラやIDEなど、多くの支援ツール があります。カリー・ハワード同系対応を使うことで、これらのツー ルを「数学」にも応用することができます。 20
プログラム風に書いた証明 AならばB H1 : A -> B BならばC H2 :
B -> C H1とH2を使ったAならばC A -> C の証明 fun x => H2(H1(x)) これなら型検査などの「プログラミング」の道具を応用できそうで す! 21
定理証明支援系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
タクティックを使った証明 プログラム風に証明を書くのは難しいので、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
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
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
まとめ 「プログラミング」と「数学」には深い対応関係があります。 「プログラミング」と「数学」 「関数」と「ならば」 「直積型」と「かつ」 「直和型」と「または」 「再帰」と「帰納法」 Coqはこの対応関係を用いた、証明用のプログラミング言語 26
最近やっていること 松坂先生の「集合・位相入 門」という本を、定理証明支 援系Coqによって形式化して います。 27