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
1.1k
5分でわかる Curry–Howard 同型対応
5分で伝えることが無茶だとわかりました
https://connpass.com/event/54292/
Susisu
May 28, 2017
Tweet
Share
More Decks by Susisu
See All by Susisu
Go で言うところのアレは TypeScript で言うとコレ / Kyoto.なんか #7
susisu
7
2.4k
君だけのオリジナル async / await を作ろう / TSKaigi 2025
susisu
18
15k
null or undefined
susisu
25
7.6k
Mackerel のフロントエンドフレームワーク移行 序章 / Hatena Engineer Seminar #13
susisu
0
2.2k
スクリーンショット撮影のために Puppeteer を操る / Kyoto.js 16
susisu
0
900
BuckleScript 使ってみた
susisu
0
350
Atom パッケージ開発のすゝめ
susisu
1
2.2k
ジェネレータを有効活用し隊 / Kyoto.js 11 LT
susisu
2
2.2k
遅延評価と健康
susisu
0
630
Other Decks in Programming
See All in Programming
いま中途半端なSwift 6対応をするより、Default ActorやApproachable Concurrencyを有効にしてからでいいんじゃない?
yimajo
2
340
monorepo の Go テストをはやくした〜い!~最小の依存解決への道のり~ / faster-testing-of-monorepos
convto
2
380
非同期jobをtransaction内で 呼ぶなよ!絶対に呼ぶなよ!
alstrocrack
0
520
Catch Up: Go Style Guide Update
andpad
0
170
私達はmodernize packageに夢を見るか feat. go/analysis, go/ast / Go Conference 2025
kaorumuta
2
490
PostgreSQLで手軽にDuckDBを使う!DuckDB&pg_duckdb入門/osk2025-duckdb
takahashiikki
1
240
メモリ不足との戦い〜大量データを扱うアプリでの実践例〜
kwzr
1
850
Breaking Up with Big ViewModels — Without Breaking Your Architecture (droidcon Berlin 2025)
steliosf
PRO
1
330
10年もののAPIサーバーにおけるCI/CDの改善の奮闘
mbook
0
770
開発者への寄付をアプリ内課金として実装する時の気の使いどころ
ski
0
350
ポスターセッション: 「まっすぐ行って、右!」って言ってラズパイカーを動かしたい 〜生成AI × Raspberry Pi Pico × Gradioの試作メモ〜
komofr
0
940
高度なUI/UXこそHotwireで作ろう Kaigi on Rails 2025
naofumi
4
3.4k
Featured
See All Featured
Done Done
chrislema
185
16k
The Success of Rails: Ensuring Growth for the Next 100 Years
eileencodes
46
7.6k
Dealing with People You Can't Stand - Big Design 2015
cassininazir
367
27k
It's Worth the Effort
3n
187
28k
The Straight Up "How To Draw Better" Workshop
denniskardys
237
140k
RailsConf & Balkan Ruby 2019: The Past, Present, and Future of Rails at GitHub
eileencodes
140
34k
Making the Leap to Tech Lead
cromwellryan
135
9.5k
Fireside Chat
paigeccino
40
3.7k
What's in a price? How to price your products and services
michaelherold
246
12k
Visualizing Your Data: Incorporating Mongo into Loggly Infrastructure
mongodb
48
9.7k
For a Future-Friendly Web
brad_frost
180
9.9k
ピンチをチャンスに:未来をつくるプロダクトロードマップ #pmconf2020
aki_iinuma
127
53k
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 ʢຊޠ༁͋Δʣ