圏論とコンピュータサイエンス / Category Theory and Theoretical Computer Science

Transcript

1. ݍ࿦ͱίϯϐϡʔλαΠΤϯε ࢁా༔೭հ yunosuke(at)ueda.info.waseda.ac.jp ૣҴాେֶେֶӃ جװཧ޻ֶݚڀՊ ৘ใཧ޻ɾ৘ใ௨৴ઐ߈ ্ాݚڀࣨ 2020/3/9
2. ֓ཁ ಋೖ ݍ࿦ͷಛ௃ CS ΁ͷԠ༻ ࣗݾ঺հ ݚڀ • ݴޠ (HydLa) ͷҙຯ࿦ ʢݩʣझຯ • ਺ֶ • ڝϓϩ 2 / 23
3. ֓ཁ ಋೖ ݍ࿦ͷಛ௃ CS ΁ͷԠ༻ ֓ཁ ͜ͷൃදͰ࿩͢͜ͱ • ݍͷఆٛͱ؆୯ͳྫ • ݍ࿦ͷߟ͑ํ͕৽͍͠ࢹ఺Λ༩͑ͯ͘ΕΔ͜ͱ • ݍ࿦͕ CS ෼໺ʹͲ͏Ԡ༻͞Ε͍ͯΔ͔ ஫ҙ ͨͿΜ෼͔Βͳ͍ྫ͕ग़ͯ͘Δͱࢥ͍·͢ ஌Βͳ͍෼໺ͷ۩ମྫ͸దٓεϧʔ͍ͯͩ͘͠͞ ͨͩ͠ҎԼͷ஌͍ͬͯΔ΋ͷͱͯ͠ਐΊ·͢ • ू߹ɼࣸ૾ͷجૅ஌ࣝʢશࣹɼ୯ࣹɼ௚ੵɼ௚࿨ʣ 3 / 23
4. ֓ཁ ಋೖ ݍ࿦ͷಛ௃ CS ΁ͷԠ༻ ݍ࿦ͱ͸ ݍ࿦ͱ͸ԿͰ͋Δ͔ • 20 ੈلத൫ʹͰ͖ͨ৽͍͠਺ֶ • ௒ந৅తͰ͓΋͠Ζ͍ • ਺ֶʹݶΒͳ͍ཧ࿦෼໺ͷڞ௨ݴޠ ݍ࿦ͱ͸ԿͰ͸ͳ͍ͷ͔ • ϓϩάϥϜΛॻ্͘Ͱ໾ʹཱͭ΋ͷ 4 / 23
5. ֓ཁ ಋೖ ݍ࿦ͷಛ௃ CS ΁ͷԠ༻ ਺ֶͷ෮श 1 ◦ ू߹ͱࣸ૾ ू߹ͱࣸ૾ʹରͯ͠ҎԼ͕੒Γཱͭ • ೚ҙͷू߹ X ʹରͯ͠߃౳ࣸ૾ idX ͕ଘࡏ • ೚ҙͷࣸ૾ f : X → Y, g : Y → Z ʹରͯ͠ ߹੒ࣸ૾ g ◦ f : X → Z ͕ଘࡏ άϥϑͱ४ಉܕ άϥϑͱͦͷ४ಉܕʹରͯ͠ҎԼ͕੒Γཱͭ • ೚ҙͷάϥϑ G ʹରͯ͠߃౳ࣸ૾ idG ͸४ಉܕ • ೚ҙͷ४ಉܕ f : G1 → G2 , g : G2 → G3 ʹରͯ͠ ߹੒ࣸ૾ g ◦ f : G1 → G3 ͸४ಉܕ 5 / 23
6. ֓ཁ ಋೖ ݍ࿦ͷಛ௃ CS ΁ͷԠ༻ ਺ֶͷ෮श 2 ◦ ܈ͱ४ಉܕ ܈ͱͦͷ४ಉܕʹରͯ͠ҎԼ͕੒Γཱͭ • ೚ҙͷ܈ G ʹରͯ͠߃౳ࣸ૾ idG ͸४ಉܕ • ೚ҙͷ४ಉܕ f : G1 → G2 , g : G2 → G3 ʹରͯ͠ ߹੒ࣸ૾ g ◦ f : G1 → G3 ͸४ಉܕ ൒ॱংू߹ͱ୯ௐࣸ૾ ൒ॱংू߹ͱ୯ௐʢ૿Ճʣࣸ૾ʹରͯ͠ҎԼ͕੒Γཱͭ • ೚ҙͷ൒ॱংू߹ X ʹରͯ͠߃౳ࣸ૾ idX ͸୯ௐ • ೚ҙͷ୯ௐࣸ૾ f : X → Y, g : Y → Z ʹରͯ͠ ߹੒ࣸ૾ g ◦ f : X → Z ͸୯ௐ 6 / 23
7. ֓ཁ ಋೖ ݍ࿦ͷಛ௃ CS ΁ͷԠ༻ ݍͷؾ࣋ͪ Ҏ্ͷྫͰ͸Ϟϊͱ໼ҹʹରͯ࣍͠ͷ 2 ͕ͭ੒Γཱ͍ͬͯͨ • ೚ҙͷϞϊʹରͯ͠߃౳తͳ໼ҹ͕ଘࡏ • ߦ͖ઌͱग़ൃ఺͕ಉ͡໼ҹʹରͯ͠߹੒ͨ͠໼ҹ͕ଘࡏ ݍ͸͜ͷ͋Γ;Εͨಛ௃Ͱఆٛ͞ΕΔ 7 / 23
8. ֓ཁ ಋೖ ݍ࿦ͷಛ௃ CS ΁ͷԠ༻ ݍͷఆٛ ఆٛ [1] ݍ͸࣍ͷཁૉ͔Β੒Γཱͭ • ର৅ɿA, B, C, ... • ࣹɿf, g, h, ... • ೚ҙͷࣹ f ʹରͯ͠ର৅ dom(f), cod(f) ͕͋Δ A = dom(f), B = cod(f) Ͱ͋Δ f Λ f : A → B ͱॻ͘ • ࣹ f : A → B, g : B → C s.t. cod(f) = dom(g) ʹରͯ͠ ࣹ g ◦ f : A → C ͕͋Γɼ ೚ҙͷࣹ f : A → B, g : B → C, h : C → D ʹରͯ͠ h ◦ (g ◦ f) = (h ◦ g) ◦ f ͕੒Γཱͭ • ೚ҙͷର৅ A ʹରࣹ͠ idA : A → A ͕͋Γɼ ೚ҙͷࣹ f : A → B ʹର͠ f ◦ idA = f = idB ◦ f ͕੒Γཱͭ 8 / 23
9. ֓ཁ ಋೖ ݍ࿦ͷಛ௃ CS ΁ͷԠ༻ ஫ҙ ର৅ͱͯ͠ू߹ɺࣹͱͯࣸ͠૾ΛऔͬͨݍΛ Sets ͱݺͿ ݍͷྫ͸ʢߏ଄෇͖ʣू߹ͱʢߏ଄Λอͭʣࣸ૾͚ͩͰ͸ͳ͍ ൒ॱংͦͷ΋ͷ ൒ॱংू߹ P Λߟ͑Δ ର৅ͱͯ͠ཁૉΛͱΓɼॱংؔ܎͕͋Δͱ͖ʹࣹ͕͋Δͱ͢Δ • ೚ҙͷཁૉ x ʹର͠ x ≤ x • x ≤ y, y ≤ z ͳΒ x ≤ z ݍͰͳ͍ྫ • ൒ॱংू߹ͱ୯ௐݮগࣸ૾ ∵ ୯ௐݮগࣸ૾ͷ߹੒͸୯ௐ૿Ճࣸ૾ • ϚάϚ M ͷཁૉͱͦͷԋࢉ ∵ ϚάϚͷԋࢉ͸୯Ґݩ͕ͳ݁͘߹తͰ΋ͳ͍ 9 / 23
10. ֓ཁ ಋೖ ݍ࿦ͷಛ௃ CS ΁ͷԠ༻ CS ͬΆ͍ྫ ໋୊ͱূ໌ • ೚ҙͷ໋୊ φ ʹରͯ͠ φ ⊢ φ • φ ⊢ ψ, ψ ⊢ ρ ͳΒ φ ⊢ ρ ϓϩάϥϜʹ͓͚Δܕͱؔ਺ ϓϩάϥϛϯάݴޠ L Λߟ͑Δ • L ͷ೚ҙͷܕ T ʹର͠Ҿ਺Λͦͷ··ฦؔ͢਺͕ॻ͚Δ • ؔ਺ f : T1 → T2 , g : T2 → T3 ʹର͠ g(f(t)) Λฦؔ͢਺ 10 / 23
11. ֓ཁ ಋೖ ݍ࿦ͷಛ௃ CS ΁ͷԠ༻ ԋश ͜ΕΒ͕ݍʹͳ͍ͬͯΔ͜ͱΛ֬ೝͯ͠Έ͍ͯͩ͘͞ ର৅ ࣹ ϕΫτϧۭؒ ઢܗࣸ૾ ࣮਺ R ͷΈ ࿈ଓؔ਺ ू߹ 2 ߲ؔ܎ ϞϊΠυ ϞϊΠυ४ಉܕ ू߹ X ͷཁૉ = ܈ G ͷཁૉ ܈ԋࢉ 11 / 23
12. ֓ཁ ಋೖ ݍ࿦ͷಛ௃ CS ΁ͷԠ༻ ݍ࿦ͷಛ௃ ݍ࿦Ͱ͸ର৅΍ࣹͷಛ௃෇͚ΛࣹͷΈΛ༻͍ͯߦ͏ ू߹࿦ͱҟͳΓର৅ͷத਎͸ݟͳ͍ ʢཁૉΛݟͳͯ͘΋ಉ౳ͷදݱྗ͕͋Δʣ ཁૉΛݟͳ͍͜ͱʹΑͬͯ • ఆ͕ٛ؆ܿʹͳΔ • ΑΓந৅తʹͳΔ • ࠓ·Ͱ෼͔Βͳ͔ͬͨ͜ͱ͕෼͔Δ 12 / 23
13. ֓ཁ ಋೖ ݍ࿦ͷಛ௃ CS ΁ͷԠ༻ Ϟϊࣹ ࣹͷಛ௃෇͚ͷྫͱͯ͠୯ࣹੑͱશࣹੑΛऔΓ্͛Δ ఆٛ ࣹ f : A → B ͕ϞϊࣹͰ͋Δͱ͸ ೚ҙͷࣹ g, h : C → A ʹରͯ͠ fg = fh ͳΒ g = h Ͱ͋Δ͜ͱ C g // h // A f // B Sets ʹ͓͍ͯϞϊࣹͰ͋Δ͜ͱ͸୯ࣹͰ͋Δ͜ͱͱಉ஋ʢԋशʣ g, h ͕ A ͷ೚ҙͷݩΛද͍ͯ͠Δͱࢥ͑͹ࣗવ Ͱ͸શࣹ͸ʁ 13 / 23
14. ֓ཁ ಋೖ ݍ࿦ͷಛ௃ CS ΁ͷԠ༻ Τϐࣹ ఆٛ ࣹ f : A → B ͕ΤϐࣹͰ͋Δͱ͸ ೚ҙͷࣹ i, j : B → C ʹରͯ͠ if = jf ͳΒ i = j Ͱ͋Δ͜ͱ A f // B i // j // C Sets ʹ͓͍ͯΤϐࣹͰ͋Δ͜ͱ͸શࣹͰ͋Δ͜ͱͱಉ஋ʢԋशʣ if = jf ͔Β i = j ͕ݴ͑ΔͨΊʹ͸ f Λ߹੒ͨ͜͠ͱͰ৘ใ͕ࣦΘΕͯ͸͍͚ͳ͍ͱߟ͑Δͱࣗવ ͞ΒʹϞϊࣹͱΤϐࣹ͸૒ରʹͳ͍ͬͯΔ 14 / 23
15. ֓ཁ ಋೖ ݍ࿦ͷಛ௃ CS ΁ͷԠ༻ ૒ର ݍ࿦ʹ͓͍ͯ 2 ͭͷ֓೦͕૒ରͰ͋Δͱ͸ɺ ยํͷࣹͷ޲͖Λશͯٯ޲͖ʹ͢Δͱ΋͏ยํʹͳΔ͜ͱ ࢼ͠ʹΤϐࣹͷਤΛͻͬ͘Γฦͯ͠ΈΔͱ Ϟϊࣹͷਤ C g // h // A f // B ͻͬ͘Γฦͨ͠Τϐࣹͷਤ C i // j // B f // A ͭ·Γ୯ࣹੑͱશࣹੑ͸ͪΐ͏Ͳ൓ରͷ֓೦Ͱ͋Δ͜ͱ͕෼͔ͬͨ 15 / 23
16. ֓ཁ ಋೖ ݍ࿦ͷಛ௃ CS ΁ͷԠ༻ ੵ ର৅ͷಛ௃෇͚ͷྫͱͯ͠ੵͱ༨ੵΛऔΓ্͛Δ ෳ਺ͷࣹΛߟ͑Δ࣌ɼਤࣜͱ͍͏ɽ ੵ ਤࣜ A p1 ←− P p2 −→ B ͕ A, B ͷੵͰ͋Δͱ͸ ೚ҙͷର৅ Z ͱਤࣜ A z1 ←− Z z2 −→ B ʹରͯ͠ pi ◦ u = zi Λຬͨ͢Ұҙͳ u : Z → P ͕ଘࡏ͢Δ͜ͱ Z z1  u  z2  A P p1 oo p2 // B Sets ʹ͓͍ͯ P ͕ੵͰ͋Δ͜ͱ͸௚ੵͰ͋Δ͜ͱͱಉ஋ʢԋशʣ (P = A × Bɼpi ͕ࣹӨɼu = ⟨z1 , z1 ⟩) 16 / 23
17. ֓ཁ ಋೖ ݍ࿦ͷಛ௃ CS ΁ͷԠ༻ ༨ੵ ݍ࿦ʹ͓͍ͯ͸૒ରͷ֓೦ΛΑ͘༨ʙͱݺͿ ༨ੵ ਤࣜ A q1 −→ Q q2 ←− B ͕ A, B ͷ༨ੵͰ͋Δͱ͸ ೚ҙͷର৅ Z ͱਤࣜ A z1 −→ Z z2 ←− B ʹରͯ͠ u ◦ qi = zi Λຬͨ͢Ұҙͳ u : Q → Z ͕ଘࡏ͢Δ͜ͱ Z A z1 ?? q1 // Q u OO B z2 __ q2 oo Sets ʹ͓͍ͯ Q ͕༨ੵͰ͋Δ͜ͱ͸௚࿨Ͱ͋Δ͜ͱͱಉ஋ʢԋशʣ ௚ੵͱ௚࿨͸ͪΐ͏Ͳ൓ରͷ֓೦Ͱ͋Δ͜ͱ͕෼͔ͬͨ ͦΕͧΕ͸Α͘ ∏ ͱ ⨿ Ͱॻ͕͘૒ରͳͷͰࣗવ 17 / 23
18. ֓ཁ ಋೖ ݍ࿦ͷಛ௃ CS ΁ͷԠ༻ ܕແ͠ϥϜμܭࢉ ܕແ͠ϥϜμܭࢉͰ࣍ͷΑ͏ͳϥϜμࣜΛߟ͑Δ λx.xx ܕແ͠ϥϜμܭࢉͷϞσϧΛ୳ͯ͠ΈΔ 1 x ͸ؔ਺ͷ͸ͣ 2 A → B ͱ͍͏ؔ਺ͩͱࢥͬͯΈΔ 3 x ͸ͦͷҾ਺ͱͯ͠༩͑ΒΕΔͷͰू߹ A ͷཁૉͰ͋Δ 4 BA = A ͸ໃ६͢ΔͷͰ BA ∼ = A ͱͯ͠ΈΔ 5 ͦΕͰ΋ೱ౓Λߟ͑Δͱ |A| = |B| = 1 ͱ͍͏ࣗ໌ͳղͷΈ 6 ܕແ͠ϥϜμܭࢉͷϞσϧ͸ͳ͍ʁ ʢ༨༟͕͋ͬͨΒͲ͕͓͔͍͔͜͠ߟ͔͑ͯΒ࣍ʹߦ͍ͬͯͩ͘͞ʣ 18 / 23
19. ֓ཁ ಋೖ ݍ࿦ͷಛ௃ CS ΁ͷԠ༻ ΋͔ͯ͠͠ Sets Ͱ ߟ͍͑ͯ·ͤΜ͔ʁ 19 / 23
20. ֓ཁ ಋೖ ݍ࿦ͷಛ௃ CS ΁ͷԠ༻ ී௨͸ |A| ͕େ͖͘ͳΕ͹ |A| < |BA| ͳͷͰղʹ͸ͳΒͳ͍ ∵ Sets Ͱߟ͍͑ͯΔ͔Βʂ ܕແ͠ϥϜμܭࢉͷඇࣗ໌ͳϞσϧͷߏ੒๏ 1 cpoʢ׬උ൒ॱংू߹ʣͷݍͰߟ͑Δ 2 উखͳ cpo D ʹରͯ͠ɺD0 = D, Dn+1 = DDn n ͱ͢Δ 3 Dn ͸ Dn+1 ʹຒΊࠐΊɺ·ͨ D∞ ͸ cpo Ͱ͋Δ͜ͱ͕ࣔͤΔ 4 ͦͯ͠ D∞ ∼ = DD∞ ∞ ΋ࣔͤΔ 5 D ͸ D∞ ʹຒΊࠐΊͯ D Λେ͖͘औΕ͹ D∞ ΋޷͖ͳ͚ͩେ͖͘Ͱ͖Δ ͜ͷߏ੒๏͸͋Δ৚݅Λຬͨ͢ݍʹҰൠԽͰ͖ΔͨΊ ܕແ͠ϥϜμܭࢉͷඇࣗ໌ͳϞσϧ͕ແ਺ʹ͋Δ͜ͱ͕෼͔Δ [2] 20 / 23
21. ֓ཁ ಋೖ ݍ࿦ͷಛ௃ CS ΁ͷԠ༻ ܕ෇͖ϥϜμܭࢉ ܕ෇͖ϥϜμܭࢉͷ΄͏͸ͦΕ΄Ͳ೉͘͠ͳ͍ Sets ͸΋ͪΖΜϞσϧʹͳ͍ͬͯΔ Ұൠʹ͋Δݍ͕ϥϜμܭࢉͷϞσϧʹͳΔʹ͸ ݍ࿦తͳҙຯͰͷႈ͕͋Ε͹Α͍ ·ͨ௚ੵܕ͕͋ΔͳΒશͯͷ༗ݶੵ͕͋Ε͹ྑ͍͠ ௚࿨ܕ͕͋ΔͳΒશͯͷ༗ݶ༨ੵ͕͋Ε͹ྑ͍ ܕ෇͖ϥϜμܭࢉʹ͓͍ͯ΋Ϟσϧʹඞཁͳ৚͕݅෼͔ͬͨ 21 / 23
22. ֓ཁ ಋೖ ݍ࿦ͷಛ௃ CS ΁ͷԠ༻ ͦͷଞ ϥϜμܭࢉҎ֎ͷԠ༻ͱͯ͠͸ Ϟφυ Haskell, Scala Ͱ࢖ΘΕͯΔ ݍ࿦͸ؔ਺ܕϓϩάϥϛϯάͷ໾ʹ͸ཱ͔ͭ΋ τϙε ߴ֊௚؍ओٛ࿦ཧͷϞσϧʹͳ͍ͬͯΔΒ͍͠ [3] ༨୅਺ ঢ়ଶભҠܥ΍ແݶσʔλߏ଄Λ௒؆୯ʹॻ͚Δ [4] ͳͲ͕͋Δ 22 / 23
23. ֓ཁ ಋೖ ݍ࿦ͷಛ௃ CS ΁ͷԠ༻ ࢀߟจݙ [1] Steve Awodey. ݍ࿦ ݪஶୈ 2 ൛. ڞཱग़൛, 2015. [2] ԣ಺׮จ. ϓϩάϥϜҙຯ࿦. ڞཱग़൛, 1994. [3] ਗ਼ਫٛ෉. ݍ࿦ʹΑΔ࿦ཧֶ ߴ֊࿦ཧͱτϙε. ౦ژେֶग़൛ձ, 2007. [4] J. Rutten. Universal coalgebra: a theory of systems. 1996. 23 / 23