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
5分でわかる Curry–Howard 同型対応
Search
Susisu
May 28, 2017
Programming
0
1k
5分でわかる Curry–Howard 同型対応
5分で伝えることが無茶だとわかりました
https://connpass.com/event/54292/
Susisu
May 28, 2017
Tweet
Share
More Decks by Susisu
See All by Susisu
君だけのオリジナル async / await を作ろう / TSKaigi 2025
susisu
18
14k
null or undefined
susisu
25
7.5k
Mackerel のフロントエンドフレームワーク移行 序章 / Hatena Engineer Seminar #13
susisu
0
2.1k
スクリーンショット撮影のために Puppeteer を操る / Kyoto.js 16
susisu
0
890
BuckleScript 使ってみた
susisu
0
340
Atom パッケージ開発のすゝめ
susisu
1
2.2k
ジェネレータを有効活用し隊 / Kyoto.js 11 LT
susisu
2
2.2k
遅延評価と健康
susisu
0
620
楽しく学ぶ難解プログラミング言語
susisu
0
840
Other Decks in Programming
See All in Programming
kiroでゲームを作ってみた
iriikeita
0
130
DatadogのArchived LogsをSnowflakeで高速に検索する方法(Archive Searchでオワコンにならないことを祈って) / How to search Datadog Archived Logs quickly with Snowflake (hoping Datadog Archive Search doesn’t make this obsolete)
civitaspo
0
110
#QiitaBash TDDで(自分の)開発がどう変わったか
ryosukedtomita
1
350
DynamoDBは怖くない!〜テーブル設計の勘所とテスト戦略〜
hyamazaki
0
170
知って得する@cloudflare_vite-pluginのあれこれ
chimame
1
140
AIのメモリー
watany
12
1.2k
Strands Agents で実現する名刺解析アーキテクチャ
omiya0555
1
110
ZeroETLで始めるDynamoDBとS3の連携
afooooil
0
140
なぜあなたのオブザーバビリティ導入は頓挫するのか
ryota_hnk
5
550
GitHub Copilotの全体像と活用のヒント AI駆動開発の最初の一歩
74th
2
740
Terraform やるなら公式スタイルガイドを読もう 〜重要項目 10選〜
hiyanger
11
2.8k
オホーツクでコミュニティを立ち上げた理由―地方出身プログラマの挑戦 / TechRAMEN 2025 Conference
lemonade_37
1
430
Featured
See All Featured
Templates, Plugins, & Blocks: Oh My! Creating the theme that thinks of everything
marktimemedia
31
2.5k
10 Git Anti Patterns You Should be Aware of
lemiorhan
PRO
656
60k
For a Future-Friendly Web
brad_frost
179
9.9k
Java REST API Framework Comparison - PWX 2021
mraible
32
8.8k
How STYLIGHT went responsive
nonsquared
100
5.7k
Fashionably flexible responsive web design (full day workshop)
malarkey
407
66k
Git: the NoSQL Database
bkeepers
PRO
431
65k
Helping Users Find Their Own Way: Creating Modern Search Experiences
danielanewman
29
2.8k
Making the Leap to Tech Lead
cromwellryan
134
9.5k
4 Signs Your Business is Dying
shpigford
184
22k
Chrome DevTools: State of the Union 2024 - Debugging React & Beyond
addyosmani
7
790
Code Reviewing Like a Champion
maltzj
524
40k
Transcript
Ͱ Θ ͔ Δ C u r
r y – H o w a rd ಉ ܕ ର Ԡ 2 0 1 7 - 0 5 - 2 8 ୈ 6 ճ O U CC LT ձ
͓ લ ୭ ͩ susisu / @susisu2413 • JavaScript
• Haskell • きんいろモザ イク
͢͜ͱ ୯७ܕ͖ϥϜμܭࢉ ࣗવԋ៷ʢ໋ཧʣ Curry–HowardಉܕରԠ System
F ͤͳ͍͜ͱʢ࣌ؒతʹʣ w ϥϜμܭࢉͷৄࡉ w ड़ޠཧ w ݹయཧͱ؍ओٛཧ
୯ ७ ܕ ͖ ϥϜ μ ܭ ࢉ
୯ ७ ܕ ͖ ϥϜ μ ܭ ࢉ w
ϥϜμܭࢉʜ୯७ͳϓϩάϥϛϯάݴޠΈ͍ͨͳͷ w ม w ؔ w ؔద༻ͷͭͷΈ w ؔܕϓϩάϥϛϯάͷཧతͳج൫ w ୯७ܕ͖ϥϜμܭࢉͦΕʹܕΛ͚ͭͨͷͷɺ ࠷؆୯ͳͷ
୯ ७ ܕ ͖ ϥϜ μ ܭ ࢉ t
::= -- ߲ x -- ม λx: T. t -- λநʢؔʣ t t -- ؔద༻ T ::= -- ܕ X -- ܕม T → T -- ؔͷܕ
୯ ७ ܕ ͖ ϥϜ μ ܭ ࢉ w
ܕ͚نଇ࣍ͷΑ͏ͳܗͰॻ͘ ʮલఏ͕ͯ͢Γཱͭͱ͖ɺ݁Γཱͭʯ w લఏ݁࣍ͷΑ͏ͳܗࣜ ʮจ຺ΓͷԼͰɺ߲ tTͱ͍͏ܕΛͭʯ ৈଥ (0 ڎΤࣣ) ٗ ` t : T
୯ ७ ܕ ͖ ϥϜ μ ܭ ࢉ x
: A 2 ` x : A , x : A ` t : B ` x : A. t : A ! B ` t1 : A ! B ` t2 : A ` t1 t2 : B
ࣗ વ ԋ ៷
ࣗ વ ԋ ៷ w ཧֶͷܗࣜମܥͷͻͱͭ w ཧతʹਖ਼໋͍͠ʢఆཧʣ จ຺ʹΑΒͣ߃ʹਅͳ໋ w
ܗࣜମܥͦͷΑ͏ͳఆཧΛಋͨ͘Ίͷͷ w ͳΜ͔ࣗવͬΆ͍ʢਓ͕ؒߦ͏ਪʹࣅ͍ͯΔʣ w ͜ͷεϥΠυͰ໋ཧͷൣғΈߟ͑·͢
ࣗ વ ԋ ៷ P ::= -- ໋ X --
໋ม P → P -- ཧแؚʮͳΒʯ P ∧ P -- ཧੵʮ͔ͭʯ P ∨ P -- ཧʮ·ͨʯ ¬P -- ൱ఆ
ࣗ વ ԋ ៷ w ಋग़نଇ࣍ͷΑ͏ͳܗͰॻ͘ ʮલఏ͕ͯ͢Γཱͭͱ͖ɺ݁Γཱͭʯ w લఏ݁࣍ͷΑ͏ͳܗࣜ ʮจ຺ΓͷԼͰɺP߃ʹਅʯ
ৈଥ (0 ڎΤࣣ) ٗ ` P
ࣗ વ ԋ ៷ A 2 ` A , A
` B ` A ! B ` A ! B ` A ` B
ࣗ વ ԋ ៷ A 2 ` A , A
` B ` A ! B ` A ! B ` A ` B x : A 2 ` x : A , x : A ` t : B ` x : A. t : A ! B ` t1 : A ! B ` t2 : A ` t1 t2 : B ୯ ७ ܕ ͖ ϥϜ μ ܭ ࢉ
ࣗ વ ԋ ៷ A 2 ` A , A
` B ` A ! B ` A ! B ` A ` B x : A 2 ` x : A , x : A ` t : B ` x : A. t : A ! B ` t1 : A ! B ` t2 : A ` t1 t2 : B ୯ ७ ܕ ͖ ϥϜ μ ܭ ࢉ ໋㱻ܕ
ࣗ વ ԋ ៷ A 2 ` A , A
` B ` A ! B ` A ! B ` A ` B x : A 2 ` x : A , x : A ` t : B ` x : A. t : A ! B ` t1 : A ! B ` t2 : A ` t1 t2 : B ୯ ७ ܕ ͖ ϥϜ μ ܭ ࢉ Curry–Howard ಉܕରԠ
ࣗ વ ԋ ៷ A 2 ` A , A
` B ` A ! B ` A ! B ` A ` B x : A 2 ` x : A , x : A ` t : B ` x : A. t : A ! B ` t1 : A ! B ` t2 : A ` t1 t2 : B ୯ ७ ܕ ͖ ϥϜ μ ܭ ࢉ ͱΜ͔ͭDJ
C u r r y – H o w a
rd ಉ ܕ ର Ԡ ଞͷཧԋࢉࢠʹؔͯ͠ରԠΛߟ͑Δ͜ͱͰ͖Δ ࣗ વ ԋ ៷ ୯ ७ ܕ ͖ ϥϜ μ ܭ ࢉ ໋ ܕ ఆ ཧ ߲ ͕ ଘ ࡏ ͢ Δ ܕ ཧ แ ؚ → ؔ ͷ ܕ →
C u r r y – H o w a
rd ಉ ܕ ର Ԡ ϥϜμܭࢉͰɺ͋Δܕͷ߲͕ଘࡏ͢Δ͜ͱΛࣔ͢ ରԠ͢Δ໋ʢఆཧʣͷূ໌ → ূ໌ࢧԉγεςϜʢ$PRͳͲʣ ϥϜμܭࢉͷ߲ʢϓϩάϥϜʣΛॻ͘ ίϯϐϡʔλʔ͕ܕΛ֬ೝ ఆཧ͕ূ໌Ͱ͖ͨ
Sy s t e m F
Sy s t e m F w ֊ͷܕ͖ϥϜμܭࢉ ୯७ܕ͖ϥϜμܭࢉ ܕʹؔ͢Δந
w ໋ཧͷൣғΛશͯΧόʔͰ͖Δ ܕʹؔ͢ΔநͰཧԋࢉࢠΛΤϯίʔυՄೳ
Sy s t e m F t ::= -- ߲
x -- ม λx: T. t -- λநʢؔʣ t t -- ؔద༻ ΛX. t -- ܕʹؔ͢Δநʢؔʣ t [T] -- ܕͷద༻ T ::= -- ܕ X -- ܕม T → T -- ௨ৗͷؔͷܕ ∀X. T -- શশྔԽ͞Εͨܕ
Sy s t e m F , X ` t
: A ` ⇤X. t : 8X. A ` t : 8X. A ` t [B] : [X 7! B]A
Sy s t e m F ֤छཧԋࢉࢠͷΤϯίʔυҎԼͷͱ͓Γ A ^ B
⌘ 8X. ((A ! B ! X) ! X) ! X A _ B ⌘ 8X. ((A ! X) ! (B ! X) ! X) ! X ? ⌘ 8X. X ¬A ⌘ A ! ? 9X. A ⌘ 8Y. (8X. A ! Y ) ! Y
Sy s t e m F w ূ໌ࢧԉγεςϜͬΆ͍ͷΛ࣮ͯ͠Έͨ IUUQTHJUIVCDPNTVTJTVTZTUFNGKTJNQM w
σϞʢ͕࣌ؒ͋ΕʣʢͨͿΜ࣌ؒͳ͍ʣ
· ͱ Ί
· ͱ Ί w Curry–HowardಉܕରԠཧֶͱϓϩάϥϜͷؒͷ ରԠؔ w System FΛ࣮͢Δͷָ͔ͬͨ͠ʢंྠͷ࠶ൃ໌ʣ ࣗ
વ ԋ ៷ ܕ ͖ ϥϜ μ ܭ ࢉ ໋ ܕ ఆ ཧ ߲ ͕ ଘ ࡏ ͢ Δ ܕ
λ→ λ2 λω λ ω λP λPω λP2 λC
λ→ λ2 λω λ ω λP λPω λP2 λC ୯७ܕ͖ϥϜμܭࢉ
System F System Fω (Haskell) CoC (Coq)
λ→ λ2 λω λ ω λP λPω λP2 λC ୯७ܕ͖ϥϜμܭࢉ
System F System Fω (Haskell) CoC (Coq) :zenzenyowai:
ࢀ ߟ จ ݙ • ஜେֶͷܭࢉཧֶͷߨٛࢿྉ http://www.cs.tsukuba.ac.jp/~kam/complogic/ • ޒेཛྷ ३,
ϓϩάϥϛϯάݴޠͷجૅ֓೦, αΠΤϯε ࣾ, 2011 • B. C. Pierce, Types and Programming Languages, The MIT press, 2002 ʢຊޠ༁͋Δʣ