5分でわかる Curry–Howard 同型対応

5分で伝えることが無茶だとわかりました

https://connpass.com/event/54292/

Transcript

1.  ෼ Ͱ Θ ͔ Δ
   C u r r y – H o w a rd ಉ ܕ ର Ԡ 2 0 1 7 - 0 5 - 2 8
   ୈ 6 ճ
   O U CC LT ձ
2. ͓ લ ͸ ୭ ͩ susisu / @susisu2413 • JavaScript • Haskell • きんいろモザ イク
3. ࿩͢͜ͱ
    ୯७ܕ෇͖ϥϜμܭࢉ
    ࣗવԋ៷ʢ໋୊࿦ཧʣ
    Curry–HowardಉܕରԠ
   
   System F
   ࿩ͤͳ͍͜ͱʢ࣌ؒతʹʣ
   w ϥϜμܭࢉͷৄࡉ
   w ड़ޠ࿦ཧ
   w ݹయ࿦ཧͱ௚؍ओٛ࿦ཧ
4. ୯ ७ ܕ ෇ ͖ ϥϜ μ ܭ ࢉ
5. ୯ ७ ܕ ෇ ͖ ϥϜ μ ܭ ࢉ w ϥϜμܭࢉ
   ʜ
   ୯७ͳϓϩάϥϛϯάݴޠΈ͍ͨͳͷ
   w ม਺
   w ؔ਺
   w ؔ਺ద༻
   ͷͭͷΈ
   w ؔ਺ܕϓϩάϥϛϯάͷཧ࿦తͳج൫
   w ୯७ܕ෇͖ϥϜμܭࢉ͸ͦΕʹܕΛ͚ͭͨ΋ͷͷ಺ɺ ࠷΋؆୯ͳ΋ͷ
6. ୯ ७ ܕ ෇ ͖ ϥϜ μ ܭ ࢉ t ::= -- ߲ x -- ม਺ λx: T. t -- λந৅ʢؔ਺ʣ t t -- ؔ਺ద༻ T ::= -- ܕ X -- ܕม਺ T → T -- ؔ਺ͷܕ
7. ୯ ७ ܕ ෇ ͖ ϥϜ μ ܭ ࢉ w ܕ෇͚نଇ͸࣍ͷΑ͏ͳܗͰॻ͘
   ʮલఏ͕͢΂ͯ੒Γཱͭͱ͖ɺ݁࿦΋੒Γཱͭʯ
   w લఏ΍݁࿦͸࣍ͷΑ͏ͳܗࣜ
   ʮจ຺
   Γ
   ͷԼͰɺ߲ t
   ͸
   T
   ͱ͍͏ܕΛ΋ͭʯ ৈଥ (0 ڎΤࣣ) ٗ໼ ` t : T
8. ୯ ७ ܕ ෇ ͖ ϥϜ μ ܭ ࢉ x : A 2 ` x : A , x : A ` t : B ` x : A. t : A ! B ` t1 : A ! B ` t2 : A ` t1 t2 : B
9. ࣗ વ ԋ ៷
10. ࣗ વ ԋ ៷ w ࿦ཧֶͷܗࣜମܥͷͻͱͭ
    w ࿦ཧతʹਖ਼໋͍͠୊ʢఆཧʣ
    
    จ຺ʹΑΒͣ߃ʹਅͳ໋୊
    w ܗࣜମܥ͸ͦͷΑ͏ͳఆཧΛಋͨ͘Ίͷ΋ͷ
    w ͳΜ͔ࣗવͬΆ͍ʢਓ͕ؒߦ͏ਪ࿦ʹࣅ͍ͯΔʣ
    w ͜ͷεϥΠυͰ͸໋୊࿦ཧͷൣғΈߟ͑·͢
11. ࣗ વ ԋ ៷ P ::= -- ໋୊ X -- ໋୊ม਺ P → P -- ࿦ཧแؚʮͳΒ͹ʯ P ∧ P -- ࿦ཧੵʮ͔ͭʯ P ∨ P -- ࿦ཧ࿨ʮ·ͨ͸ʯ ¬P -- ൱ఆ
12. ࣗ વ ԋ ៷ w ಋग़نଇ͸࣍ͷΑ͏ͳܗͰॻ͘
    ʮલఏ͕͢΂ͯ੒Γཱͭͱ͖ɺ݁࿦΋੒Γཱͭʯ
    w લఏ΍݁࿦͸࣍ͷΑ͏ͳܗࣜ
    ʮจ຺
    Γ
    ͷԼͰɺP
    ͸߃ʹਅʯ ৈଥ (0 ڎΤࣣ) ٗ໼ ` P
13. ࣗ વ ԋ ៷ A 2 ` A , A ` B ` A ! B ` A ! B ` A ` B
14. ࣗ વ ԋ ៷ 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 ୯ ७ ܕ ෇ ͖ ϥϜ μ ܭ ࢉ
15. ࣗ વ ԋ ៷ 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 ୯ ७ ܕ ෇ ͖ ϥϜ μ ܭ ࢉ ໋୊
    㱻
    ܕ
16. ࣗ વ ԋ ៷ 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 ಉܕରԠ
17. ࣗ વ ԋ ៷ 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
18. C u r r y – H o w a rd ಉ ܕ ର Ԡ ଞͷ࿦ཧԋࢉࢠʹؔͯ͠ରԠΛߟ͑Δ͜ͱ΋Ͱ͖Δ ࣗ વ ԋ ៷ ୯ ७ ܕ ෇ ͖ ϥϜ μ ܭ ࢉ ໋ ୊ ܕ ఆ ཧ ߲ ͕ ଘ ࡏ ͢ Δ ܕ ࿦ ཧ แ ؚ → ؔ ਺ ͷ ܕ →
19. C u r r y – H o w a rd ಉ ܕ ର Ԡ ϥϜμܭࢉͰɺ͋Δܕͷ߲͕ଘࡏ͢Δ͜ͱΛࣔ͢
    
    ରԠ͢Δ໋୊ʢఆཧʣͷূ໌
    → ূ໌ࢧԉγεςϜʢ$PR
    ͳͲʣ
     ϥϜμܭࢉͷ߲ʢϓϩάϥϜʣΛॻ͘
     ίϯϐϡʔλʔ͕ܕΛ֬ೝ
     ఆཧ͕ূ໌Ͱ͖ͨ
20. Sy s t e m F
21. Sy s t e m F w ֊ͷܕ෇͖ϥϜμܭࢉ
    ୯७ܕ෇͖ϥϜμܭࢉ
    
    ܕʹؔ͢Δந৅
    w ໋୊࿦ཧͷൣғΛશͯΧόʔͰ͖Δ
    ܕʹؔ͢Δந৅Ͱ࿦ཧԋࢉࢠΛΤϯίʔυՄೳ
22. Sy s t e m F t ::= -- ߲ x -- ม਺ λx: T. t -- λந৅ʢؔ਺ʣ t t -- ؔ਺ద༻ ΛX. t -- ܕʹؔ͢Δந৅ʢؔ਺ʣ t [T] -- ܕ΁ͷద༻ T ::= -- ܕ X -- ܕม਺ T → T -- ௨ৗͷؔ਺ͷܕ ∀X. T -- શশྔԽ͞Εͨܕ
23. Sy s t e m F , X ` t : A ` ⇤X. t : 8X. A ` t : 8X. A ` t [B] : [X 7! B]A
24. 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
25. Sy s t e m F w ূ໌ࢧԉγεςϜͬΆ͍ͷΛ࣮૷ͯ͠Έͨ
    IUUQTHJUIVCDPNTVTJTVTZTUFNGKTJNQM
    w σϞʢ͕࣌ؒ͋Ε͹ʣʢͨͿΜ࣌ؒͳ͍ʣ
26. · ͱ Ί
27. · ͱ Ί w Curry–HowardಉܕରԠ͸࿦ཧֶͱϓϩάϥϜͷؒͷ ରԠؔ܎
    w System FΛ࣮૷͢Δͷָ͔ͬͨ͠ʢंྠͷ࠶ൃ໌ʣ ࣗ વ ԋ ៷ ܕ ෇ ͖ ϥϜ μ ܭ ࢉ ໋ ୊ ܕ ఆ ཧ ߲ ͕ ଘ ࡏ ͢ Δ ܕ
28. λ→ λ2 λω λ ω λP λPω λP2 λC
29. λ→ λ2 λω λ ω λP λPω λP2 λC ୯७ܕ෇͖ϥϜμܭࢉ System F System Fω (Haskell) CoC (Coq)
30. λ→ λ2 λω λ ω λP λPω λP2 λC ୯७ܕ෇͖ϥϜμܭࢉ System F System Fω (Haskell) CoC (Coq) :zenzenyowai:
31. ࢀ ߟ จ ݙ • ஜ೾େֶͷܭࢉ࿦ཧֶͷߨٛࢿྉ http://www.cs.tsukuba.ac.jp/~kam/complogic/ • ޒेཛྷ ३, ϓϩάϥϛϯάݴޠͷجૅ֓೦, αΠΤϯε ࣾ, 2011 • B. C. Pierce, Types and Programming Languages, The MIT press, 2002 ʢ೔ຊޠ༁΋͋Δʣ