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
水戸黄門で学ぶカリー=ハワード同型対応
Search
Shuma
June 22, 2024
Programming
1
320
水戸黄門で学ぶカリー=ハワード同型対応
Shuma
June 22, 2024
Tweet
Share
More Decks by Shuma
See All by Shuma
阿部寛のホームページをSRE観点で改善出来るか考えてみた。
shubox
0
70
一日の終わりに、晩酌しながら眺めたいシステムログの世界
shubox
0
72
プロダクトがクローズした話
shubox
0
25
今も熱いもの!魂を揺さぶる戦士の儀式:マオリ族のハカ
shubox
0
230
信頼性工学とは? ~カツオを題材に~
shubox
0
89
バージョン管理と人生設計の類似点ver2 -リポジトリから学ぶ生きるヒント-
shubox
0
270
バージョン管理と人生設計の類似点
shubox
0
120
今年を振り返り、来年の抱負
shubox
0
260
インフラエンジニアが活きる組織、活きない組織って?
shubox
0
180
Other Decks in Programming
See All in Programming
デミカツ切り抜きで面倒くさいことはPythonにやらせよう
aokswork3
0
240
オープンソースソフトウェアへの解像度🔬
utam0k
15
2.9k
「ちょっと古いから」って避けてた技術書、今だからこそ読もう
mottyzzz
11
6.7k
非同期jobをtransaction内で 呼ぶなよ!絶対に呼ぶなよ!
alstrocrack
0
930
Devoxx BE - Local Development in the AI Era
kdubois
0
130
CSC509 Lecture 05
javiergs
PRO
0
300
チームの境界をブチ抜いていけ
tokai235
0
180
コードとあなたと私の距離 / The Distance Between Code, You, and I
hiro_y
0
170
Range on Rails ―「多重範囲型」という新たな選択肢が、複雑ロジックを劇的にシンプルにしたワケ
rizap_tech
0
150
品質ワークショップをやってみた
nealle
0
260
ソフトウェア設計の実践的な考え方
masuda220
PRO
4
580
Writing Better Go: Lessons from 10 Code Reviews
konradreiche
0
1.2k
Featured
See All Featured
Unsuck your backbone
ammeep
671
58k
How to Create Impact in a Changing Tech Landscape [PerfNow 2023]
tammyeverts
55
3k
The Pragmatic Product Professional
lauravandoore
36
6.9k
Fight the Zombie Pattern Library - RWD Summit 2016
marcelosomers
234
17k
jQuery: Nuts, Bolts and Bling
dougneiner
65
7.9k
Performance Is Good for Brains [We Love Speed 2024]
tammyeverts
12
1.2k
Into the Great Unknown - MozCon
thekraken
40
2.1k
Stop Working from a Prison Cell
hatefulcrawdad
271
21k
Building Applications with DynamoDB
mza
96
6.7k
Visualization
eitanlees
149
16k
Large-scale JavaScript Application Architecture
addyosmani
514
110k
Imperfection Machines: The Place of Print at Facebook
scottboms
269
13k
Transcript
水戸黄門で学ぶカリー=ハワード 同型対応 Shuma
自己紹介 名前:Shuma 現職:ベンチャー企業でインフラエンジニア 経歴:飲食店店長→バイト→インフラエンジニア 一言:昨日までAWSSummitに参加していて楽しかった。
LT始める前に ・文系なので、数学苦手です。(数学に関する質問されると泣きます。。) ・それでもなぜ、この LTをやろうと思ったのか、 →私の住んでいる神戸に HackBarというエンジニアバーがありまして、 そこで店員をやられている ”ことさん(関数型プログラミングの愛好家) ”からカリー=ハワード同型対応を通して数学とプログラミ ングの証明の関係性に関して教えていただきました。
感銘を受けたので、今回発表してみることにして見ました。 ただ、私もうまく理解できていないので間違っていたらご教示いただけると幸いです。
話すことと話さないこと① 話すこと: 1. カリーハワード同型対応の基本概念 ◦ 論理学の命題と型理論の対応 ◦ 数学的証明とプログラムの対応 2. 水戸黄門の物語を用いた直感的な説明
◦ 物語の展開とプログラムの実行過程の類似性 3. 実世界での応用例 ◦ プログラムの正当性証明
話すことと話さないこと② 話さないこと: 1. カリーハワード同型対応の数学的厳密性 ◦ 圏論や型理論の深い数学的詳細 2. 特定のプログラミング言語での実装詳細 ◦ 関数型言語での具体的なコード例
3. 歴史的な発展過程の詳細 ◦ 発見以降の理論の進化 4. 高度な応用分野 ◦ 証明支援システムの内部機構 ◦ 量子計算との関連性
カリー=ハワード同型対応とは? アメリカの数学者ハスケル・カリー(Haskell Curry)と論理学者ウィリアム・ハワード(William Howard)により最初に発見された形式論理の体系とある種の計算の体系との 構文論的なアナロジーを一般化した概念である。 つまり、論理学とプログラミング言語理論を結びつける重要な概念 引用:カリー=ハワード同型対応 - Wikiwand
どっちがカリー=ハワード同型対応を提唱者? A、
どっちがカリー=ハワード同型対応を提唱者? B,
正解は、、 Bです。 • 1934年,1958年に,ハスケルカリーが今とは少し違う形で 言及. • 1968年,ウィリアムハワードが現在の形で定式化. 出所: 2010_tetsugakukisobunkaseminar-2_05.pdf (kyoto-u.ac.jp) カリーハワード同型対応入門
水戸黄門の世界 「江戸時代のスーパーヒーロー」 • 水戸黄門:正義のために旅をする隠れた大名。 • 毎回のストーリー展開が、実はカリーハワード同型対応の完璧な例示ではないかと • 時代劇(約一時間の中でストーリー展開がはっきりとしている) と勝手に思いました。。 実際に水戸黄門を題材にカリー=ハワード同型対応に当てはめて考えていきます。
論理命題と型理論の関係: • 命題 = プログラムの仕様 • 型 = その仕様を表現する方法 •
プログラム = 仕様を満たす具体的な実装 簡単に言えば: • 命題は「何をすべきか」 • 型は「どんな形でやるか」 • プログラムは「実際にどうやるか」
論理命題と型理論 まずは、水戸黄門のストーリーを命題と型理論にあてはめて行きます。 命題(P):「不正を正す」(型に相当) 証明(Q):水戸黄門の具体的な行動の計画(プログラムに相当) 型(T):「不正を正す」という目的を達成するための方法の集合 プログラム(t):水戸黄門の実際の行動(型 Tに属する具体的な実装)
水戸黄門の旅をカリーハワード同型対応で考えると① • 命題(型):「悪を倒す」 • 証明(プログラム):水戸黄門の具体的な行動 1. 町に到着する(関数の開始) 2. 情報を集める(データ入力) 3.
悪人を特定する(条件分岐) 4. 証拠を集める(データ処理) 5. 印籠を見せる(結果出力) この流れは、プログラムの実行過程と直接的に対応します。
水戸黄門の旅とカリーハワード同型対応で考えると② プログラミング言語での簡単な例 この例は、水戸黄門の行動をプログラムと して表現しています。 型注釈は命題に、関数の実装は証明に 対応します。
カリーハワード同型対応の現代的応用 プログラムの正当性の証明 • 命題:「このプログラムは仕様を満たす」 • 証明:プログラム自体が証明となる • 応用例: 銀行システム ◦
命題:「全ての取引は整合性を保つ」 ◦ 証明/プログラム:取引を処理する関数 ◦ 利点:数学的に正しさが保証されたシステムの構築が可能
カリーハワード同型対応の現代的応用② 補足説明: • 応用例で、「命題」は型システムにおける型に対応し、「証明」はその型を持つプログラムに対応します。 • プログラムの正当性の証明では、プログラム自体が証明となるため、正しいプログラムを書くことが即ち証明を構築する ことになります。 • プログラムの自動生成は、与えられた型(仕様)に対して、その型を持つプログラム(証明)を自動的に構築するプロセ スと見なせます。
• 型駆動開発は、型(命題)を先に定義し、それを満たすプログラム(証明)を段階的に構築していく手法です。これはカ リーハワード同型対応の考え方を開発プロセスに応用したものと言えます。
なぜ、重要なのか プログラミングの論理的思考促進: • プログラムを数学的命題として捉えることで、より厳密な設計と実装が可能になります。 複雑な問題解決への新アプローチ: • 数学的証明とプログラムの対応を利用して、難しい問題を新しい視点で解決できます。 数学とプログラミングの統合: • 両分野の知識を相互に活用し、より深い理解と革新的なアイデアの創出が可能になります。
まとめ ・カリー=ハワード同型対応の中で命題と証明を、水戸黄門の冒険 = プログラムの実行過程に当て はめて説明して見ました。 ・この考え方で、プログラミングや数学の見方が変わる。 ・興味が出たら、学んで見てください。 →プロがいますので神戸までお越しください。
終わり