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
300
水戸黄門で学ぶカリー=ハワード同型対応
Shuma
June 22, 2024
Tweet
Share
More Decks by Shuma
See All by Shuma
阿部寛のホームページをSRE観点で改善出来るか考えてみた。
shubox
0
62
一日の終わりに、晩酌しながら眺めたいシステムログの世界
shubox
0
70
プロダクトがクローズした話
shubox
0
25
今も熱いもの!魂を揺さぶる戦士の儀式:マオリ族のハカ
shubox
0
230
信頼性工学とは? ~カツオを題材に~
shubox
0
87
バージョン管理と人生設計の類似点ver2 -リポジトリから学ぶ生きるヒント-
shubox
0
270
バージョン管理と人生設計の類似点
shubox
0
110
今年を振り返り、来年の抱負
shubox
0
250
インフラエンジニアが活きる組織、活きない組織って?
shubox
0
170
Other Decks in Programming
See All in Programming
Navigating Dependency Injection with Metro
zacsweers
3
260
Putting The Genie in the Bottle - A Crash Course on running LLMs on Android
iurysza
0
140
機能追加とリーダー業務の類似性
rinchoku
2
1.3k
MCPとデザインシステムに立脚したデザインと実装の融合
yukukotani
4
1.4k
Kiroで始めるAI-DLC
kaonash
2
590
Introducing ReActionView: A new ActionView-compatible ERB Engine @ Rails World 2025, Amsterdam
marcoroth
0
690
テストコードはもう書かない:JetBrains AI Assistantに委ねる非同期処理のテスト自動設計・生成
makun
0
300
概念モデル→論理モデルで気をつけていること
sunnyone
2
170
[FEConf 2025] 모노레포 절망편, 14개 레포로 부활하기까지 걸린 1년
mmmaxkim
0
1.6k
Amazon RDS 向けに提供されている MCP Server と仕組みを調べてみた/jawsug-okayama-2025-aurora-mcp
takahashiikki
1
110
Deep Dive into Kotlin Flow
jmatsu
1
340
JSONataを使ってみよう Step Functionsが楽しくなる実践テクニック #devio2025
dafujii
1
530
Featured
See All Featured
Performance Is Good for Brains [We Love Speed 2024]
tammyeverts
12
1.1k
Reflections from 52 weeks, 52 projects
jeffersonlam
352
21k
Optimizing for Happiness
mojombo
379
70k
JavaScript: Past, Present, and Future - NDC Porto 2020
reverentgeek
51
5.6k
Statistics for Hackers
jakevdp
799
220k
Building Better People: How to give real-time feedback that sticks.
wjessup
368
19k
Large-scale JavaScript Application Architecture
addyosmani
512
110k
The Invisible Side of Design
smashingmag
301
51k
Testing 201, or: Great Expectations
jmmastey
45
7.7k
Speed Design
sergeychernyshev
32
1.1k
Save Time (by Creating Custom Rails Generators)
garrettdimon
PRO
32
1.6k
CoffeeScript is Beautiful & I Never Want to Write Plain JavaScript Again
sstephenson
162
15k
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. 印籠を見せる(結果出力) この流れは、プログラムの実行過程と直接的に対応します。
水戸黄門の旅とカリーハワード同型対応で考えると② プログラミング言語での簡単な例 この例は、水戸黄門の行動をプログラムと して表現しています。 型注釈は命題に、関数の実装は証明に 対応します。
カリーハワード同型対応の現代的応用 プログラムの正当性の証明 • 命題:「このプログラムは仕様を満たす」 • 証明:プログラム自体が証明となる • 応用例: 銀行システム ◦
命題:「全ての取引は整合性を保つ」 ◦ 証明/プログラム:取引を処理する関数 ◦ 利点:数学的に正しさが保証されたシステムの構築が可能
カリーハワード同型対応の現代的応用② 補足説明: • 応用例で、「命題」は型システムにおける型に対応し、「証明」はその型を持つプログラムに対応します。 • プログラムの正当性の証明では、プログラム自体が証明となるため、正しいプログラムを書くことが即ち証明を構築する ことになります。 • プログラムの自動生成は、与えられた型(仕様)に対して、その型を持つプログラム(証明)を自動的に構築するプロセ スと見なせます。
• 型駆動開発は、型(命題)を先に定義し、それを満たすプログラム(証明)を段階的に構築していく手法です。これはカ リーハワード同型対応の考え方を開発プロセスに応用したものと言えます。
なぜ、重要なのか プログラミングの論理的思考促進: • プログラムを数学的命題として捉えることで、より厳密な設計と実装が可能になります。 複雑な問題解決への新アプローチ: • 数学的証明とプログラムの対応を利用して、難しい問題を新しい視点で解決できます。 数学とプログラミングの統合: • 両分野の知識を相互に活用し、より深い理解と革新的なアイデアの創出が可能になります。
まとめ ・カリー=ハワード同型対応の中で命題と証明を、水戸黄門の冒険 = プログラムの実行過程に当て はめて説明して見ました。 ・この考え方で、プログラミングや数学の見方が変わる。 ・興味が出たら、学んで見てください。 →プロがいますので神戸までお越しください。
終わり