Swiftプログラミングと論理 〜そして帰ってきた圏論〜 / Swift and Logic, and Category Theory

Swiftプログラミングと論理 〜そして帰ってきた圏論〜 iOSDC Japan 2019 (Sep 6, 2019)
https://fortee.jp/iosdc-japan-2019/proposal/9529444c-a849-47cd-94a7-bf2b694320aa

Transcript

1. Swiftͱ࿦ཧ
   ʙͦͯ͠ؼ͖ͬͯͨݍ࿦ʙ 2019/09/06 iOSDC 2019 Yasuhiro Inami / @inamiy
2. ࿦ཧֶ
   ࢥߟͷಓےΛʮਅཧ
   5SVUI ʯ
   ͱ͍͏֓೦Λ༻͍ͯઆ໌͢Δֶ໰
3. J04%$
   ͸
   J04ΧϯϑΝϨϯε
   J04ΧϯϑΝϨϯε
   ͸
   ͨͷ͠ʔ
   ΑͬͯɺJ04%$
   ͸
   ͨͷ͠ʔ
4. ΋͠
   "
   ͳΒ͹
   #
   ΋͠
   #
   ͳΒ͹
   $
   Αͬͯɺ΋͠
   "
   ͳΒ͹
   $
5. 2
   ͜Ε͸ৗʹਖ਼͍͠ʁ
6. ൴ࢯ
   ͸
   ΰϦϥ
   ΰϦϥ
   ͸
   Πέϝϯ
   Αͬͯɺ൴ࢯ
   ͸
   Πέϝϯ
8. ʮਖ਼͍͠ʯͱ͸ͳΜͧ΍ʁ
   ԿΛਖ਼͍͠ͱߟ͑ɺࢥߟΛల։͍͚ͯ͠Δ͔ʁ
9. ࿦ཧͷʮਖ਼͠͞ʯΛ෼͚ͯߟ͑Δ 
   ࿦ཧͷʮܗʯ͕ਖ਼͍͠
   
   ࿦ཧͷʮ಺༰ʯ͕ਖ਼͍͠
10. ߏจ࿦
    (Syntax) ه߸తͳ࿦ཧࣜͱਪ࿦نଇΛ࢖ͬͯɺ
    ʢػցతʹʣ৽͍͠࿦ཧࣜΛܭࢉʢূ໌ʣ͢Δ
11. ࿦ཧͷύλʔϯ "
    ͳΒ͹
    #
    "
    ͱ
    #
    "
    ·ͨ͸
    #
    "
    Ͱͳ͍ A → B A ∧ B A ∨ B ¬A
12. ໋୊ͱ࿦ཧࣜ ࿦ཧه߸ ໋୊ม߲ ໋୊ఆ߲ ∧ , ∨ , ¬, → A, B, C, ⋯ ⊤ , ⊥
13. ࿦ཧࣜͷྫ A ∧ (B → C) (A ∨ B) ∧ (C → D) (¬A → ⊥ ) ∨ (¬B ∧ ⊤ )
14. ਪ࿦نଇͷྫɿϞʔμεϙωϯε A → B A B جຊతͳਪ࿦نଇΛ
    ެཧܥͱͯ͠ఆΊΔ લఏ̍ɿ
    "ͳΒ͹#
    લఏ̎ɿ
    "Ͱ͋Δ
    ݁࿦ɹɿ
    #Ͱ͋Δ
15. ূ໌ਤͷྫʢਪ࿦نଇͷద༻աఔͷ໦ߏ଄ʣ
16. ҙຯ࿦
    (Semantics) ࿦ཧࣜʹʮਅʯ·ͨ͸ʮِʯͷ ਅཧ஋Λ෇༩ͯ͠ղऍ͢Δ
17. ࿦ཧࣜʢه߸ʣˠ
    ਅཧ஋ͷׂΓ౰ͯ A B ¬A A∧B A∨B A→B 1 1 0 1 1 1 1 0 0 0 1 0 0 1 1 0 1 1 0 0 1 0 0 1 ෇஋ 
    
    ਅ
    
    
    ِ A → B A ∧ B A ∨ B ¬A ֤ม߲ͷਅِΛܾΊΔ
    ʹ
    ߦΛબͿ
18. ਅཧ஋දͷྫ A B ¬A ¬A∨B A→B (¬A∨B) → (A→B) (A→B) → (¬A∨B) 1 1 0 1 1 1 1 1 0 0 0 0 1 1 0 1 1 1 1 1 1 0 0 1 1 1 1 1 ৗʹʹͳΔ
    ࿦ཧ͕ࣜଘࡏ
19. (A → B) ↔ (¬A ∨ B) ͸ɺ໋୊
    "ɺ#
    ʹΑΒͣɺৗʹਅ
    ߃ਅ
    τʔτϩδʔ P ↔ Q := (P → Q) ∧ (Q → P)
20. ߃ਅʢτʔτϩδʔʣͷྫ ྗͱ͸ύϫʔ
    ຖ೔͕ΤϒϦσΠ A → A ಉҰ཯
21. ߃ਅʢτʔτϩδʔʣͷྫ ੈͷதʹ͸छྨͷஉ͔͠ډͳ͍
    Զ͔ɺԶҎ֎͔ A ∨ ¬A ഉத཯
22. ߃ਅʢτʔτϩδʔʣͷྫ (A → B) → ((B → C) → (A → C)) ((((A → B) → (¬C → ¬D)) → C) → E) → ((E → A) → (D → A)) ¬(A ∧ ¬A) (A ∧ ¬A) → B ((A → B) → A) → A ¬¬A → A (A → B) ↔ (¬B → ¬A) ¬(A ∧ B) ↔ (¬A ∨ ¬B) ¬(A ∨ B) ↔ (¬A ∧ ¬B)
23. (A → B) → ((B → C) → (A → C)) ((((A → B) → (¬C → ¬D)) → C) → E) → ((E → A) → (D → A)) ¬(A ∧ ¬A) (A ∧ ¬A) → B ((A → B) → A) → A ¬¬A → A (A → B) ↔ (¬B → ¬A) ¬(A ∧ B) ↔ (¬A ∨ ¬B) ¬(A ∨ B) ↔ (¬A ∧ ¬B) ߃ਅʢτʔτϩδʔʣͷྫ ໃ६཯ രൃ཯ ೋॏ൱ఆআڈ ύʔεͷ๏ଇ ରۮ཯ υɾϞϧΨϯͷ๏ଇ ਪҠ཯ ϝϨσΟεͷެཧ
24. ߃ਅʢτʔτϩδʔʣͷྫ ߃ਅͳ࿦ཧࣜ͸ແݶʹଘࡏ͢Δ
    
 ˠ
    ༗ݶͷنଇ͔Βಋ͖ग़ͤͳ͍͔ʁ A → ¬¬A A → ¬¬¬¬A A → ¬¬¬¬¬¬A ⋯
25. ߃ਅͳ࿦ཧ͔ࣜΒ
    ܗࣜతମܥΛߟ͑Δ
26. ܗࣜతମܥʢه߸ʴจ๏ʴެཧʴਪ࿦نଇʣ ެཧ
    ʹ
    લఏͱͯ͠ಋೖ͞ΕΔجຊతͳԾఆ
    ʢҰ෦ͷ߃ਅͳ࿦ཧࣜʣ
    ਪ࿦نଇ
    ʹ
    ࿦ཧ͔ࣜΒଞͷ࿦ཧࣜΛಋ͘͜ͱ
    ެཧͱਪ࿦نଇʢܗࣜతମܥʣΛ࢖ͬͯ
    ͢΂ͯͷ߃ਅͳ࿦ཧࣜʢఆཧʣΛಋ͘
27. ܗࣜతମܥͷछྨ w ήϯπΣϯྲྀ
    w ࣗવԋ៷
    ʜ
    ೔ৗͷਪ࿦ʹ͍ۙɺެཧͳ͠ɺਪ࿦نଇ͕ଟ͍
    w γʔΫΤϯτܭࢉ
    ʜ
    ެཧ͕̍ͭʢಉҰੑʣɺਪ࿦نଇ͕ଟ͍
    w ώϧϕϧτྲྀ
    w ެཧ͕ଟ͍ɺਪ࿦نଇ͕̍ͭʢϞʔμεϙωϯεʣ
    w ܗࣜతମܥ͔Βಋग़͞ΕΔ࿦ཧࣜʢఆཧʣ͸ɺ߃ਅʢ݈શੑʣ
28. ήϯπΣϯྲྀɾࣗવԋ៷ A B A ∧ B A ∧ B A A ∧ B B A A ∨ B B A ∨ B A ∨ B C C C A → B A B B A → B ⊥ ¬A A ¬A ⊥ ⊥ A ⋮ [A] ¬¬A A ⋮ [A] ⋮ [B] ⋮ [A] <">
    ʜ
    "ͷԾఆΛด͡Δ
29. ήϯπΣϯྲྀɾࣗવԋ៷ʢγʔΫΤϯτܭࢉ෩ʣ Γ ⊢ A Γ ⊢ B Γ ⊢ A ∧ B Γ ⊢ A ∧ B Γ ⊢ A Γ ⊢ A ∧ B Γ ⊢ B Γ ⊢ A Γ ⊢ A ∨ B Γ ⊢ B Γ ⊢ A ∨ B Γ ⊢ A ∨ B Γ, A ⊢ C Γ, B ⊢ C Γ ⊢ C Γ ⊢ A → B Γ ⊢ A Γ ⊢ B Γ, A ⊢ B Γ ⊢ A → B Γ, A ⊢ ⊥ Γ ⊢ ¬A Γ ⊢ A Γ ⊢ ¬A Γ ⊢ ⊥ Γ ⊢ ⊥ Γ ⊢ A Γ ⊢ ¬¬A Γ ⊢ A A ∈ Γ Γ ⊢ A ϵ⊢"
    ʜ
    ࿦ཧࣜͷ༗ݶྻϵ͔Βɺ࿦ཧࣜ"͕ূ໌Ͱ͖Δ
30. ώϧϕϧτྲྀ A → B A B B → (A → B) (A → (B → C)) → ((A → B) → (A → C)) ¬¬A → A A → A ∨ B ⊥ → A B → A ∨ B (A → C) → ((B → C) → ((A ∨ B) → C)) A ∧ B → A A ∧ B → B A → (B → (A ∧ B)) ਪ࿦نଇ͸
    ϞʔμεϙωϯεͷΈ (A → ¬A) → ¬A ¬A → (A → B)
31. ͦΕͱͳ͘
 ʮ4XJGUϓϩάϥϛϯάʯ
    ͬΆ͍
32. ࿦ཧ
    ˱
    4XJGUϓϩάϥϛϯά A → B A ∧ B A ∨ B ¬A := A → ⊥ ରԠ 㱻 ؔ਺ܕ ௚ੵܕ ௚࿨ܕ ⊥ Either<A, B> Never typealias Not<A> = (A) -> Never (A, B) (A) -> B ϘτϜܕ 㲄Λ࢖ͬͯ
    ൱ఆΛఆٛͰ͖Δ
33. ʲ࠶ܝʳήϯπΣϯྲྀɾࣗવԋ៷ A B A ∧ B A ∧ B A A ∧ B B A A ∨ B B A ∨ B A ∨ B C C C A → B A B B A → B ⊥ ¬A A ¬A ⊥ ⊥ A ⋮ [A] ¬¬A A ⋮ [A] ⋮ [B] ⋮ [A]
34. /// `B ===> A → B` /// - Note: More formally, A ⊢ B ===> ⊢ A → B. func implyIntro<A, B>(_ b: B) -> ((A) -> B) { { _ in b } } /// `A → B, A ===> B` (Modus ponens) func implyElim<A, B>(_ f: (A) -> B, _ a: A) -> B { f(a) } A → B A B B A → B ⋮ [A]
35. /// `A, B ===> A ∧ B` func andIntro<A, B>(_ a: A, _ b: B) -> (A, B) { (a, b) } /// `A ∧ B ===> A` func andElim1<A, B>(_ ab: (A, B)) -> A { ab.0 } /// `A ∧ B ===> B` func andElim2<A, B>(_ ab: (A, B)) -> B { ab.1 } A B A ∧ B A ∧ B A A ∧ B B
36. /// `A ===> A ∨ B` func orIntro1<A, B>(_ a: A) -> Either<A, B> { .left(a) } /// `B ===> A ∨ B` func orIntro2<A, B>(_ b: B) -> Either<A, B> { .right(b) } /// `A ∨ B, A → C, B → C ===> C` func orElim<A, B, C>( _ e: Either<A, B>, _ ac: (A) -> C, _ bc: (B) -> C ) -> C { switch e { case let .left(a): return ac(a) case let .right(b): return bc(b) } } A A ∨ B B A ∨ B A ∨ B C C C ⋮ [A] ⋮ [B]
37. struct Not<A> { let f: (A) -> Never } /// `A ⊢ ⊥ ===> ⊢ ¬A` func notIntro<A>(_ x: Never) -> Not<A> { Not { _ in x } } /// `A, ¬A ===> ⊥` (NOTE: not using `fatalError`) func notElim<A>(_ a: A, _ notA: Not<A>) -> Never { notA.f(a) } ⊥ ¬A A ¬A ⊥ ⋮ [A]
38. /// `⊥ ===> A` func absurd<A>(_ x: Never) -> A { // Do nothing, but it compiles. } ⊥ A
39. ʲ࠶ܝʳώϧϕϧτྲྀ B → (A → B) (A → (B → C)) → ((A → B) → (A → C)) A → A ∨ B B → A ∨ B (A → C) → ((B → C) → ((A ∨ B) → C)) A ∧ B → A A ∧ B → B A → (B → (A ∧ B)) A → B A B ਪ࿦نଇ͸
    ϞʔμεϙωϯεͷΈ ¬¬A → A ⊥ → A (A → ¬A) → ¬A ¬A → (A → B)
40. ʲ࠶ܝʳώϧϕϧτྲྀ (A → C) → ((B → C) → ((A ∨ B) → C)) A → B A B A → A ∨ B B → A ∨ B A ∧ B → A A ∧ B → B A → (B → (A ∧ B)) ਪ࿦نଇ͸
    ϞʔμεϙωϯεͷΈ ¬¬A → A ⊥ → A (A → ¬A) → ¬A ¬A → (A → B) (A → (B → C)) → ((A → B) → (A → C)) A ∨ B := ¬A → B := ¬B → A A ∧ B := ¬(A → ¬B) := ¬(B → ¬A) ¬A := A → ⊥ /05&
    ˮ
    ˭
    ™
    ͸ɺˠ
    ͱ
    ˵
    ͷΈΛ࢖ͬͯهड़Ͱ͖Δ B → (A → B)
41. ίϯϏωʔλ࿦ཧ Kxy = x Sxyz = xz(yz) I = SKK K : X → Y → X S : (Z → Y → X) → (Z → Y) → Z → X I : X → X ஋ͷؔ਺Խ
    ҰൠԽ 
 3FBEFSϞφυͷQVSF Ϟʔμεϙωϯε
    ͷҰൠԽ
 3FBEFSϞφυͷBQ
42. /// `K = A → (B → A)` func k<A, B>(_ a: A) -> (B) -> A { { _ in a } } /// `S = (A → (B → C)) → ((A → B) → (A → C))` func s<A, B, C>(_ a: @escaping (C) -> (A) -> B) -> (_ b: @escaping (C) -> A) -> (C) -> B { { b in { c in a(c)(b(c)) } } }
43. /// `I = SKK: A → A` func i<A>(_ a: A) -> A { let k_: (A) -> (A) -> A = k let skk: (A) -> A = s(k)(k_) return skk(a) } i("hello") // "hello" i(123) // 123
44. ࿦ཧ
    
    ⇕
    
    4XJGUϓϩάϥϛϯά
47. ((A → B) → A) → A A ∨ ¬A ¬¬A → A ¬(A ∧ B) → (¬A ∨ ¬B) (A → B) → (¬A ∨ B) (¬B → ¬A) → (A → B) ഉத཯ ೋॏ൱ఆআڈ ରۮ཯
    ൱ఆআڈWFS υɾϞϧΨϯͷ๏ଇ
    ™㱸 ؚ࣮࣭ҙ ύʔεͷ๏ଇ /05&
    ʮٯʯ͸߃ਅ 4XJGUͰ࣮૷Ͱ͖ͳ͍߃ਅͳ࿦ཧࣜ
48. /// `A ∨ ¬A` (Law of excluded middle) func excludedMiddle<A>() -> Either<A, Not<A>> { fatalError("Can't impl in Swift”) }
49. /// `A ∨ ¬A` (Law of excluded middle) func excludedMiddle<A>() -> Either<A, Not<A>> { fatalError("Can't impl in Swift”) } ANY LANGUAGES!
50. /// `((A → B) → A) → A` func peirceLaw<A, B>() -> (((A) -> B) -> A) -> A { { (aba: ((A) -> B) -> A) in let ab: (A) -> B = { fatalError("Can't impl ") }() let a = aba(ab) return a } }
51. /// `((A → B) → A) → A` func peirceLaw<A, B>() -> (((A) -> B) -> A) -> A { { (aba: ((A) -> B) -> A) in // WARNING: This compiles, but using invalid `excludedMiddle()`. let either: Either<A, Not<A>> = excludedMiddle() switch either { case let .left(a): return a case let .right(notA): return aba { a in absurd(notA.f(a)) } } } } ݟ্͔͚͸࣮૷Ͱ͖͍ͯΔ͕ɺ
    ഉத཯Λ࢖͍ͬͯΔͷͰɺ
52. ͜Ε·Ͱͷ࿦ཧ͸ɾɾɾ ݹయ࿦ཧ
    ϒʔϧ࿦ཧ
    ࿦ཧࣜʹʮਅʯ·ͨ͸ʮِʯͷ
 ਅཧ஋Λ෇༩ͯ͠ղऍ͢Δ
53. ݹయ࿦ཧʹ͓͚Δʮˠʯ A → B Bool true false USVF
    PS
    GBMTF
    ௨Γ͔͠ͳ͍
54. 4XJGUϓϩάϥϛϯάʹ͓͚Δʮˠʯ Types Int Bool (A) -> B (Int)->Bool ৽͍͠ܕ͕
    ߏ੒͞ΕΔ
55. ݹయ࿦ཧ
    ϒʔϧ࿦ཧ
    ˣ
 ߏ੒త࿦ཧ
 ௚؍ओٛ࿦ཧ ഉத཯΍ೋॏ൱ఆআڈ͕
    ੒Γཱͨͳ͘ͳΔ
56. ௚؍ओٛ࿦ཧ
    ⇕
    
    4XJGUϓϩάϥϛϯά
57. ௚؍ओ໋ٛ୊࿦ཧʹ͓͚Δ
    ࣗવԋ៷
    
    ⇕
    
    ୯७ܕ෇͖ϥϜμܭࢉ
 ؔ਺ܕϓϩάϥϛϯάͷཧ࿦తج൫
58. ܕͳ͠ϥϜμܭࢉʢུ֓ʣ t ::= x | λx . t | t t ʢม਺ʣ ʢλந৅ɺؔ਺ఆٛʣ ʢؔ਺ద༻ʣ λx . x λx . (λy . x) (λx . xx)(λx . xx) λ߲ͷྫ ϥϜμ߲
59. ܕ෇͖ϥϜμܭࢉʢུ֓ʣ T ::= X | T → T ʢܕม਺ʣ ʢؔ਺ܕʣ t ::= x | λ(x : T) . t | t t ʢม਺ʣ ʢλந৅ʣ ʢؔ਺ద༻ʣ : T ϥϜμ߲ ܕɹ
60. ܕ෇͖ϥϜμܭࢉʢུ֓ʣ A ∈ Γ Γ ⊢ A Γ, A ⊢ B Γ ⊢ A → B Γ ⊢ A → B Γ ⊢ A Γ ⊢ B (x : A) ∈ Γ Γ ⊢ x : A Γ, x : A ⊢ t : B Γ ⊢ λ(x : A) . t : A → B Γ ⊢ t12 : A → B Γ ⊢ t1 : A Γ ⊢ t12 t1 : B ܕ෇͚نଇͷʮܕͷΈʯʹ஫໨͢Δͱʜ ࣗવԋ៷ͱ
    ಉ౳ λ߲ͷܕ෇͚نଇ ม਺ Еந৅ ؔ਺ద༻
61. ௚؍ओ໋ٛ୊࿦ཧʹ͓͚Δ
    ࣗવԋ៷
    
    ⇕
    
    ୯७ܕ෇͖ϥϜμܭࢉ
 ؔ਺ܕϓϩάϥϛϯάͷཧ࿦తج൫ ΧϦʔɾϋϫʔυ
    ಉܕରԠ
62. ΧϦʔɾϋϫʔυಉܕରԠ ௚؍ओ໋ٛ୊࿦ཧʹ͓͚Δ

    ࣗવԋ៷ ୯७ ܕ෇͖ϥϜμܭࢉ
    
 ؔ਺ܕϓϩάϥϛϯά ໋୊ɾఆཧ ܕ ূ໌ਤ ϥϜμ߲ʢϓϩάϥϜʣ ؚҙಋೖ ϥϜμந৅ʢؔ਺ఆٛʣ Ϟʔμεϙωϯε ؔ਺ద༻ ެཧ άϩʔόϧม਺ Ծఆ ࣗ༝ม਺ ԾఆΛด͡Δ ଋറม਺ ଞͷ࿦ཧԋࢉ
    㱸
    㱹ͳͲ ͷ
    ֦ுͱಉܕରԠ΋Մೳ
63. ௚؍ओٛ࿦ཧ
 ࿦ཧࣜʹʮՄೳੈքʯΛߟྀͨ͠
    ʮਅʯʮِʯͷਅཧ஋Λ෇༩ͯ͠ղऍ͢Δ
64. ௚؍ओٛ࿦ཧͱʮՄೳੈքʯʢ஌ࣝঢ়ଶʣ A 0 B 0 A 1 B 0 A 1 B 1
65. ֤ੈքͱਅཧ஋ͷҨ఻ؔ܎ A 0 B 0 A 1 B 0 A 1 B 0 
    ͸ະདྷ΁Ҩ఻͢Δ
    
    ʹ໭Βͳ͍ ৽͍͠஌ݟ
66. ֤ੈքͱਅཧ஋ͷҨ఻ؔ܎ A 0 ¬A 0 A 0 ¬A 1 A 0 ¬A 1 ™"
    
    
    ͷ৔߹ɺ
    ݱࡏ͔Βະདྷʹ͔͚ͯ
    "
    
    
    
    ʢ"
    
    
    ʹͳΔ͜ͱ͸ͳ͍ʣ Ҩ఻
67. A 0 ¬A 0 A 0 ¬A 1 A 0 ¬A 1 ™"
    
    
    ͷ৔߹ɺ
    ݱࡏ͔Βະདྷʹ͔͚ͯ
    "
    
    
    
    ʢ"
    
    
    ʹͳΔ͜ͱ͸ͳ͍ʣ Ҩ఻ ֤ੈքͱਅཧ஋දͷҨ఻ؔ܎ A ∨ ¬A ഉத཯͸߃ਅͰ͸ͳ͍
68. ֤ੈքͱਅཧ஋ͷҨ఻ؔ܎ A → B 1 A 0 B 0 A → B 1 A 1 B 1 A → B 1 A 1 B 1 Ҩ఻ "
    
    
    ͕ಘΒΕΔͱɺ
 #
    
    ΋ࣗಈతʹಘΒΕΔ "
    
    
    #
    
    
    ʹ
    ͳΔ͜ͱ͸ͳ͍
69. ֤ੈքͱਅཧ஋ͷҨ఻ؔ܎ "
    
    
    ͕ಘΒΕΔͱɺ
 #
    
    ΋ࣗಈతʹಘΒΕΔ A 0 B 0 A 1 B 0 A 1 B 1 A 0 B 1
70. ΫϦϓΩɾϞσϧʢࡶͳղઆʣ wΫϦϓΩɾϑϨʔϜ
    ʜ
    
    ˠ
    
    ˠ
    
    ͳͲͷੈքͷॱংू߹
    wΫϦϓΩɾϞσϧ
    ʜ
    ϑϨʔϜͷ֤ੈքͷ্ʹ
    Ҩ఻͢Δ
    
 ɹɹɹɹɹɹɹɹɹ
    
    ਅཧ஋ͷׂΓ౰ͯΛߦͬͨ΋ͷ
    w௚؍ओٛ࿦ཧʹ͓͚Δ߃ਅ
 ʜ
    ೚ҙͷϑϨʔϜʴ೚ҙͷਅཧ஋ͷׂΓ౰ͯ
 ɹ
    ʹ
    ೚ҙͷϞσϧʹ͓͍ͯਅʹͳΔ࿦ཧࣜͷ͜ͱ "
    
    
    ͕ಘΒΕΔͱɺ
 #
    
    ΋ࣗಈతʹಘΒΕΔ
71. ݹయ࿦ཧ
    ˩
    ௚؍ओٛ࿦ཧ ࠷খ࿦ཧ ௚؍ओٛ࿦ཧ ݹయ࿦ཧ A ∨ ¬A ⊥ → A → , ∧ , ∨ , ¬, ⊥ Λ࢖ͬͨ࿦ཧࣜ A → A ∨ B A ∧ B → A ໃ६཯ ഉத཯ ⋮ ʲ஫ҙʳ௚؍ओٛ࿦ཧ͕ഉத཯Λ௚઀ؚΉΘ͚Ͱ͸ͳ͍ʢ࣍ϖʔδࢀরʣ
72. άϦϕϯίͷఆཧɿݹయ࿦ཧ
    ˠ
    ௚؍ओٛ࿦ཧ΁ͷຒΊࠐΈ ௚؍ओٛ࿦ཧ ݹయ࿦ཧ A ∨ ¬A ¬¬(A ∨ ¬A) ¬¬ ೋॏ൱ఆಋೖ ഉத཯ ೋॏ൱ఆഉத཯
73. ((A → B) → A) → A A ∨ ¬A ¬¬A → A ¬(A ∧ B) → (¬A ∨ ¬B) (A → B) → (¬A ∨ B) (¬B → ¬A) → (A → B) ഉத཯ ೋॏ൱ఆআڈ ରۮ཯
    ൱ఆআڈWFS υɾϞϧΨϯͷ๏ଇ
    ™㱸 ؚ࣮࣭ҙ ύʔεͷ๏ଇ ʲ࠶ܝʳ௚؍ओٛ࿦ཧͰ੒Γཱͨͳ͍࿦ཧࣜ /05&
    ʮٯʯ͸߃ਅ
74. ¬¬(((A → B) → A) → A) ¬¬(A ∨ ¬A) ¬¬(¬¬A → A) ¬¬(¬(A ∧ B) → (¬A ∨ ¬B)) ¬¬((A → B) → (¬A ∨ B)) ¬¬((¬B → ¬A) → (A → B)) ௚؍ओٛ࿦ཧͰ߃ਅͳ࿦ཧࣜ ͢΂ͯ
    ௚؍ओٛ࿦ཧ Ͱ੒Γཱͭ
75. ¬¬((A → B) → A) → ¬¬A ¬¬(A ∨ ¬A) ¬¬¬¬A → ¬¬A ¬¬¬(A ∧ B) → ¬¬(¬A ∨ ¬B) ¬¬(A → B) → ¬¬(¬A ∨ B) ¬¬(¬B → ¬A) → ¬¬(A → B) Tautologies in Intuitionistic Logic Using helper rule ¬¬(A → B) ¬¬A → ¬¬B
76. /// `¬¬(A ∨ ¬A)` (Law of excluded middle in Intuitionistic Logic) func excludedMiddle_IL<A>() -> Not<Not<Either<A, Not<A>>>> { Not<Not<Either<A, Not<A>>>> { notEither in let notA: Not<A> = Not { a in notEither.f(.left(a)) } let either: Either<A, Not<A>> = .right(notA) return notEither.f(either) } }
77. /// `¬¬¬¬A ===> ¬¬A` (Double negation elimination in IL) func doubleNegationElim_IL<A>( _ notNotNotNotA: Not<Not<Not<Not<A>>>> ) -> Not<Not<A>> { Not<Not<A>> { notA in notNotNotNotA.f( Not<Not<Not<A>>> { notNotA in notNotA.f(notA) } ) } }
78. /// `¬¬¬(A ∧ B) ===> ¬¬(¬A ∨ ¬B)` (De-Morgan's Law in IL) func deMorgan4_IL<A, B>(_ notNotNotAB: Not<Not<Not<(A, B)>>>) -> Not<Not<Either<Not<A>, Not<B>>>> { Not<Not<Either<Not<A>, Not<B>>>> { (notEither: Not<Either<Not<A>, Not<B>>>) in let notNotAB = Not<Not<(A, B)>> { notAB in let notB = Not<B> { b in let notA = Not<A> { a in notAB.f((a, b)) } let either: Either<Not<A>, Not<B>> = .left(notA) return notEither.f(either) } let either: Either<Not<A>, Not<B>> = .right(notB) return notEither.f(either) } return notNotNotAB.f(notNotAB) } }
79. /// `¬¬((A → B) → A) → ¬¬A` (Peirce's Law in IL) func peirceLaw_IL<A, B>() -> (Not<Not<((A) -> B) -> A>>) -> Not<Not<A>> { { notNotF in Not<Not<A>> { notA in let notABA = Not<((A) -> B) -> A> { aba in let ab: (A) -> B = { a in absurd(notElim(a, notA)) } let a = aba(ab) return notA.f(a) } return notNotF.f(notABA) } } }
80. ύʔεͷ๏ଇ
    ˠ
    DBMMDD ¬¬(A → B) ¬¬A → ¬¬B ((A → ¬¬B) → ¬¬A) → ¬¬A ͜͜Ͱ Λ࢖͏ͱ ¬¬(A → B) A → ¬¬B ¬¬(((A → B) → A) → A) ύʔεͷ๏ଇ
81. /// Continuation. typealias Cont<R, A> = (@escaping (A) -> R) -> R /// /// Call with Current Continuation. /// - Peirce: `((A → B) → A) → A` /// - CallCC: `((A → M<B>) → M<A>) → M<A>` /// /// - Note: `callCC` is like control operators e.g. `goto`, `return`, `throw`. /// func callCC<A, B, R>( _ f: @escaping (_ exit: @escaping (A) -> Cont<R, B>) -> Cont<R, A> ) -> Cont<R, A> { { outer in f { a in { _ in outer(a) } }(outer) } }
82. func doubleNegationElim_callCC<R, A>( _ doubleNegation: @escaping ( _ neg: @escaping (A) -> Cont<R, Never> ) -> Cont<R, Never> ) -> Cont<R, A> { callCC { exit -> Cont<R, A> in flatMap(doubleNegation(exit), absurd) } }
83. ֊໋୊࿦ཧ
 ͢΂ͯʮ˲ʯ
    ͱ
    ଘࡏʮ˳ʯ
84. ֊໋୊࿦ཧ A1 ∧ A2 ∧ ⋯ ≅ ∀X . X A1 ∨ A2 ∨ ⋯ ≅ ∃X . X (A1 → C) ∧ (A2 → C) ∧ ⋯ ≅ ∀X . (X → C) ʮ໋୊ʯͷશশྔԽ
    㱼ɺଘࡏྔԽ
    㱽
 ֊ड़ޠ࿦ཧͷʮ߲ʯͷྔԽͱҟͳΔͷͰ஫ҙ 㱸
    ͱ
    㱼 㱹
    ͱ
    㱽
85. ֊໋୊࿦ཧͷਪ࿦نଇ ∀X . A(X) A(T) A(Y) ∀X . A(X) ∃X . A(X) ∀X . (A(X) → C) C A(T) ∃X . A(X)
    
    
    
    
    ͸ɹɹɹ
    ʹࢸΔԋ៷ͷԾఆ͢΂ͯͱɹɹɹ
    ͷதͰ
    ࣗ༝ม਺ͱͯ͠࢖ΘΕ͍ͯͳ͍ܕม਺ Y A(Y) A(X)
    
    
    
    ͸ɹɹʹ
    ୅ೖՄೳͳܕ T A
86. (A1 → C) ∧ (A2 → C) ∧ ⋯ ≅ ∀X . (X → C) let intToBool: (Int) -> Bool = { ... } let floatToBool: (Float) -> Bool = { ... } let strToBool: (String) -> Bool = { ... } // ... ͢΂ͯͷܕʹ͍ͭͯಉ͡Α͏ͳ࣮૷Λߦ͍͍ͨ // Swift ͷδΣωϦΫεʢଟ૬ؔ਺ʣΛ࢖͏ͱɺ // ্هͷॏෳίʔυΛ1ͭʹ·ͱΊͯந৅ԽͰ͖Δɻ func xToBool<X>(_ x: X) -> Bool { ... }
87. ˲ͱ˳ͷؔ܎ (A1 ∨ A2 ) → C ≅ (A1 → C) ∧ (A2 → C) (∃X . X) → C ≅ ∀X . (X → C) (A1 ∨ A2 ∨ ⋯) → C ≅ (A1 → C) ∧ (A2 → C) ∧ ⋯ (A → C) → ((B → C) → ((A ∨ B) → C)) ࢀߟɿ
88. ∀X . (X → C) ≅ (∃X . X) → C func forallXToBool<X>(_ x: X) -> Bool { anyToBool(x) } /// - Note: `∃X.X` is isomorphic to `Any`. func anyToBool(_ any: Any) -> Bool { forallXToBool(any) }
89. ∀(X <: P) . (X → C) ≅ (∃(X <: P) . X) → C protocol P { var value: String { get } } struct AnyP: P { let value: String } func forallXProtocolToBool<X: P>(_ x: X) -> Bool { // Generic func protocolToBool(x) } func protocolToBool(_ p: P) -> Bool { // Protocol func (dynamic) forallXProtocolToBool(AnyP(value: p.value)) }
90. ∀(X <: P) . (X → C) ≅ (∃(X <: P) . X) → C // Reverse Opaque Result Type (static) func someProtocolToBool(_ p: some P) -> Bool { forallXProtocolToBool(p) } // ERROR: Isn’t supported yet in Swift 5.1
91. ֊໋୊࿦ཧ
    ⇕
    
    δΣωϦΫε
    ଟ૬ੑ
    Ұ෦ɺϓϩτίϧϕʔεʹஔ͖׵͑΋Մೳ
92. ϥϜμΩϡʔϒ
93. ϥϜμΩϡʔϒ ֊ ଟ૬ ϥϜμ
    ֊௚؍ओ໋ٛ୊࿦ཧ
    ܕʹґଘͨ͠஋
    ଟ૬ؔ਺ ͕࡞ΕΔ ୯७ܕ෇͖ϥϜμ
    ֊௚؍ओ໋ٛ୊࿦ཧ
    ஋ʹґଘͨ͠஋
    ߴ֊ؔ਺ ͕࡞ΕΔ ґଘܕ
    
    ֊௚؍ओٛड़ޠ࿦ཧ
    ஋ʹґଘͨ͠ܕ͕࡞ΕΔ ߴ֊ଟ૬ϥϜμ
    ߴ֊ΧΠϯυʴଟ૬ؔ਺ ߴ֊ΧΠϯυܕ
    ܕʹґଘͨ͠ܕ
    ߴ֊ͷܕؔ਺ ͕࡞ΕΔ
94. ϥϜμΩϡʔϒ 4XJGU͸
    ΠϚίί ࠓճ
    ֶΜͩ͜ͱ
95. ϥϜμΩϡʔϒ ֊ ଟ૬ ϥϜμ
    ֊௚؍ओ໋ٛ୊࿦ཧ
    ܕʹґଘͨ͠஋
    ଟ૬ؔ਺ ͕࡞ΕΔ ୯७ܕ෇͖ϥϜμ
    ௚؍ओ໋ٛ୊࿦ཧ
    ஋ʹґଘͨ͠஋
    ௨ৗͷߴ֊ؔ਺ ͕࡞ΕΔ ґଘܕ
    
    ֊௚؍ओٛड़ޠ࿦ཧ
    ஋ʹґଘͨ͠ܕ͕࡞ΕΔ ߴ֊ଟ૬ϥϜμ
    ଟ૬ͳߴ֊ܕߏஙࢠ͕࡞ΕΔ ߴ֊ΧΠϯυܕ
    ܕʹґଘͨ͠ܕ
    ߴ֊ͷܕߏஙࢠ ͕࡞ΕΔ Calculus of Constructions
96. ·ͱΊ w࿦ཧΛʮܗࣜʯͱʮҙຯʯͷͭͷଆ໘͔Βߟ͑Δ
    wܗࣜతମܥ
    ʜ
    ެཧʢҰ෦ͷ߃ਅͳ࿦ཧࣜʣͱਪ࿦نଇ
    wݹయ࿦ཧ͔Β௚؍ओٛ࿦ཧ΁ʢഉத཯ͷഇࢭͱΫϦϓΩҙຯ࿦ʣ
    w֊໋୊࿦ཧʢδΣωϦΫεͱϓϩτίϧʣ
    w௚؍ओٛ࿦ཧ
    ˱
    4XJGUϓϩάϥϛϯάʢΧϦʔɾϋϫʔυରԠʣ
    w࿦ཧΛֶͿͱɺܕͷҙຯͱՁ஋͕෼͔Δ
97. Sample Code
 http://gist.github.com/inamiy/SwiftAndLogic
98. One more thing…
99. ʙؼ͖ͬͯͨݍ࿦ʙ
100. ࡢ೥ͷ
     J04%$
     
     ͷൃද
 IUUQTTQFBLFSEFDLDPNJOBNJZJPTEDKBQBO
 IUUQTRJJUBDPNJOBNJZJUFNTFDEFBGCDE
101. A B C ݍ
102. A B C ݍ idA idB idC
103. A B C ݍ f g ∘ f g
104. ߃౳ࣹͱ߹੒ A → B B → C A → C A → A
105. ࿦ཧԋࢉ
     ˭
     ͔ͭ A ∧ B A A ∧ B B A B A ∧ B
106. A ∧ B A B A ∧ B A A ∧ B B
107. (C → A) ∧ (C → B) C → (A ∧ B) A B C A ∧ B A B A ∧ B HomC (C, A) × HomC (C, B) ≅ HomC (C, A × B)
108. ࿦ཧԋࢉ
     ˮ
     ·ͨ͸ A A ∨ B B A ∨ B A ∨ B A → C B → C C
109. A ∨ B A B A A ∨ B B A ∨ B
110. A B C A ∨ B (A → C) ∧ (B → C) (A ∨ B) → C A ∨ B A → C B → C C HomC (A, C) × HomC (B, C) ≅ HomC (A + B, C)
111. ถాͷิ୊ Hom[C,Set] (HomC (A, − ), F) ≅ F(A) ∀B . (A → B) → F(B) ≅ F(A) A ⟺ ∀B . (A → B) → B A ⟹ (A → ⊥ ) → ⊥ '
     
     ߃౳ؔखͷͱ͖ #
     
     ˵
     ʹಛघԽ
 ˲আڈ ೋॏ൱ఆ ¬¬A
112. άϦϕϯίͷఆཧɿݹయ࿦ཧ
     ˠ
     ௚؍ओٛ࿦ཧ΁ͷຒΊࠐΈ ௚؍ओٛ࿦ཧ ݹయ࿦ཧ A ∨ ¬A ¬¬(A ∨ ¬A) ¬¬ ೋॏ൱ఆಋೖ ഉத཯ ೋॏ൱ఆഉத཯ $14ม׵ A ⟹ (A → ⊥ ) → ⊥
113. F(C) D ݍ F C ݍ U(D) ࣹͷू߹ U ≅ rightAdjunct leftAdjunct
114. F(C) D ݍ F U C U(D) ݍ F(U(D)) U(F(C)) f f F(f) U(f) unitC counitD
115. A × X B ݍ − × X ( − )X A BX ݍ BX × X f f f × id eval ႈ
     ࢦ਺ର৅ ධՁࣹ
116. B BX × X eval A × X − × X ( − )X A BX f f f × id ႈ
     ࢦ਺ର৅ ݍ ݍ ධՁࣹ X → B B B
117. σΧϧτ ΧϧςγΞϯ ดݍ  ऴର৅
     
     ⊤
      ௚ੵ
     "ʷ#
     "˭#
      ႈ ࢦ਺ର৅
     #"
     "ˠ#
     Λ࣋ͭݍͷ͜ͱ ௚؍ओٛ ࿦ཧͷܗࣜతମܥ͸σΧϧτดݍʹΑͬͯ
 ݍ࿦తʹҙຯ෇͚͢Δ͜ͱ͕Ͱ͖Δ σΧϧτดݍ ࿦ཧࣜͷূ໌ ܕ෇͖ϥϜμܭࢉ ର৅ ࿦ཧࣜ ܕ ࣹ ূ໌ ϥϜμ߲
     ࣗ༝ม਺Λ࣋ͨͳ͍ ႈର৅ ˠ
     Λ࢖ͬͨ࿦ཧࣜ ؔ਺ܕ ධՁࣹ Ϟʔμεϙωϯε ؔ਺ద༻ ΧϦʔɾϋϫʔυɾϥϯϕοΫରԠ
120. "MHFCSBJD
     %BUB
     5ZQF
     JO
     4XJGU
 IUUQTTQFBLFSEFDLDPNJOBNJZBMHFCSBJDEBUBUZQFJOTXJGU
121. τϙε
     ʹ
     σΧϧτดݍʴ෦෼ର৅෼ྨࢠ {a ∈ A|p(a)} A τϙε Ω true 1 unit m p p.b.
122. τϙε
     ʹ
     σΧϧτดݍʴ෦෼ର৅෼ྨࢠ {a ∈ A|p(a)} A τϙε Ω true 1 unit m ෦෼ର৅
     4VCPCKFDU
     Ϟϊࣹ ෦෼ର৅෼ྨࢠ
     4VCPCKFDU
     $MBTTJpFS
     ྫɿτϙε͕ू߹ͷݍͷͱ͖

     Њ
     
     \
     USVF
     GBMTF
     ^ p p.b. Ҿ͖໭͠
     
 1VMMCBDL
     QC ಛੑࣹ
     "্ͷड़ޠ
123. ࢀߟจݙʢ࿦ཧֶɺϥϜμܭࢉɺܕγεςϜʣ w ʰܭࢉ࿦ཧֶʱߨٛࢿྉ
     
     ُࢁ޾ٛ
     w ΧϦʔʹϋϫʔυಉܕରԠ
     
     8JLJQFEJB
     w ΧϦʔɾϋϫʔυରԠͱ௚؍ओٛ࿦ཧͷ ҙຯ࿦ೖ໳
     
     ໼ా෦ढ़հ
     w ௚؍ओٛ࿦ཧ΁ͷট଴
     
     রҪҰ੒
     w ਺ֶಉ޷ձ
     
     ފా
     w $MBTTJDBM
     -PHJD
     JO
     )BTLFMM w
     "
     5ZQF
     4ZTUFN
     'SPN
     4DSBUDI
     r
     3PCFSU
     8JENBOO
     w "
     4IPSU
     *OUSPEVDUJPO
     UP
     4ZTUFNT
     '
     BOE
     'Т
     
     1BCMP
     /PHVFJSB
     w
     ࿦ཧͱܭࢉͷ͘͠Έ
     
     Ԯ୩ণݾɺ੢࡚ਅ໵
     w
     ৘ใՊֶʹ͓͚Δ࿦ཧ
     
     খ໺׮᏷
     w
     ϓϩάϥϜҙຯ࿦
     
     ԣ಺׮จ
     w
     ܕγεςϜೖ໳
     5B1-
     
     1JFSDF
124. ࢀߟจݙʢݍ࿦ɺτϙεʣ w ೥
     ݍ࿦ษڧձ
     ࢿྉ
     
     தଜߊҰ
     w ᐻࢁਖ਼޾ͷΩϚΠϥࣂҭه
     w ఩ֶऀͷͨΊͷݍ࿦ೖ໳
     
     ৿ాਅੜ
     w ݍ࿦ʹΑΔϓϩάϥϛϯάͱ࿦ཧ
     
     !TIJBUTVNBU
     
     !@@JOU
     w τϙε
     
     BMHE
     w 5IF
     %BSL
     4JEF
     PG
     'PSDJOH
     w 0MJWJB
     $BSBNFMMPT
     XFCTJUF
     w "O
     *OUSPEVDUJPO
     UP
     5PQPT
     5IFPSZ
     w ,SJQLFr+PZBM
     ҙຯ࿦
     
     ;JQIJM
     "MFTIMBT
     
     w (SPUIFOEJFDL
     5PQPT
     ΁ͷೖ໳
     
     !LSJQLFKPZBM
     w ϓϩάϥϛϯάݴޠͷҙຯ࿦ͱݍ࿦
     
     ௕୩઒ ਅਓ
     w τϙεͱߴ֊࿦ཧ
     
     5BJDIJ
     6FNVSB
     w
     ݍ࿦
     
     "XPEFZ
     w
     ݍ࿦ʹΑΔ࿦ཧֶʕߴ֊࿦ཧͱτϙε
     
     ਗ਼ ਫ
     ٛ෉
     w
     ݍ࿦ͷา͖ํ
     
     ೔ຊධ࿦ࣾ
125. Thanks! Yasuhiro Inami @inamiy