Chagua Lugha

Optiki Zilizochanganywa: Mfumo wa Bikategoria wa Vitendo vya Profunctor

Makala hii inawasilisha ujumuishaji wa optiki rahisi hadi optiki changamano kwa kutumia kitendo cha bikategoria, hasa Prof, kwenye viwakilishi vya kushirikiana, kwa kuunganisha viendeshaji vya polynomial na ugani wa Kan.
rgbcw.net | PDF Size: 0.1 MB
Ukadiriaji: 4.5/5
★ ★ ★ ★ ★
Ukadiriaji Wako
Umekadiria waraka huu tayari
Kifuniko cha Waraka PDF - Optiki Zilizochanganywa: Mfumo wa Bikategoria wa Vitendo vya Profunctor
Tazama Waraka PDF Pakua PDF Tafsiri PDF
Nyumbani » Nyaraka » Optiki Zilizochanganywa: Mfumo wa Bikategoria wa Vitendo vya Profunctor

Orodha ya Yaliyomo

1. Utangulizi

Optiki, katika muktadha wa nadharia ya kategoria na programu za kazi, hutoa njia yenye kanuni ya kufikia na kusasisha sehemu za miundo changamani ya data. Ingawa optiki rahisi hufanya kazi ndani ya mfumo mmoja wa kategoria kwa kutumia vitendo vya monoidal, maendeleo ya hivi karibuni yanayohusisha viendeshaji vya polynomial yanahitaji nadharia ya jumla zaidi. Makala hii inatanguliza optiki zilizochanganywa, ambazo hujumlisha mfumo huu kwa kutumia kitendo cha bikategoria, hasa bikategoria ya profunctor (Prof), kwenye kategoria za viwakilishi vya kushirikiana. Umoja huu unashikilia kwa ustadi optiki zinazotokana na mabadiliko ya asili kati ya viendeshaji vya polynomial.

2. Optiki Rahisi

Msingi wa optiki umejengwa juu ya dhana ya aktigori.

2.1 Aktigori na Vitendo vya Monoidal

Aktigori inafafanuliwa na kitendo cha kategoria ya monoidal $\mathcal{M}$ kwenye kategoria $\mathcal{C}$, ikionyeshwa na $\bullet : \mathcal{M} \times \mathcal{C} \to \mathcal{C}$. Hii inaweza kutazamwa kama kiendeshaji cha monoidal $\bullet: \mathcal{M} \to [\mathcal{C}, \mathcal{C}]$.

2.2 Vitendo vya Tofauti Mchanganyiko na Coends

Kwa kuzingatia vitendo viwili $\bullet_1: \mathcal{M} \to [\mathcal{C}, \mathcal{C}]$ na $\bullet_2: \mathcal{M} \to [\mathcal{D}, \mathcal{D}]$, vinaweza kuunganishwa kuwa kitendo cha tofauti mchanganyiko kwenye kategoria ya bidhaa $\mathcal{C}^{\text{op}} \times \mathcal{D}$. Seti za hom basi huongezwa kando ya vitendo hivi, na baada ya wastani juu ya $\mathcal{M}$ kwa kutumia coend, tunapata umbo la kawaida la optiki rahisi (iliyochanganywa):

$$O\langle a,b \rangle\langle s,t \rangle = \int^{m:\mathcal{M}} \mathcal{C}(s, m \bullet_1 a) \times \mathcal{D}(m \bullet_2 b, t)$$

Hapa, $\langle a, b \rangle$ inawakilisha "lengo la kuzingatia" na $\langle s, t \rangle$ "kitu kizima".

2.3 Kategoria ya Optiki

Optiki hizi huunda seti za hom za kategoria $\mathbf{Opt}$, ambapo vitu ni jozi $\langle a, b \rangle$.

3. Bikategoria

Bikategoria inajumlisha nadharia ya kategoria kwa kuanzisha seli-2 (mofizimu kati ya seli-1), ikipunguza usawa mkali hadi isomofizimu yenye mshikamano.

3.1 Ufafanuzi na Mifano

Bikategoria $\mathcal{B}$ inajumuisha seli-0 (vitu), seli-1 (mishale kati ya vitu), na seli-2 (mishale kati ya seli-1). Kwa jozi yoyote ya seli-0 $i, j$, seli-1 huunda kategoria ya hom $\mathcal{B}(i, j)$. Mfano wa kawaida ni $\mathbf{Cat}$, na kategoria kama seli-0, viendeshaji kama seli-1, na mabadiliko ya asili kama seli-2.

3.2 Kategoria za Monoidal kama Bikategoria

Bikategoria yenye kitu kimoja ni sawa na kategoria ya monoidal. Seli-1 zake za mwisho ndio vitu vya kategoria ya monoidal, muundo ni bidhaa ya tensor, na seli-2 ndio mofizimu.

3.3 Pseudoendeshaji

Pseudoendeshaji $F: \mathcal{C} \to \mathcal{D}$ kati ya bikategoria ni uchoraji ramani unaohifadhi muundo wa bikategoria hadi isomofizimu yenye mshikamano, badala ya kuwa mkali.

4. Optiki Zilizochanganywa kupitia Vitendo vya Bikategoria

Uelewa muhimu ni kwamba uhusiano kati ya malengo ya kuzingatia na vitu vilivyochanganywa katika optiki zilizochanganywa haufafanuliwi vyema na kitendo kimoja cha monoidal (aktigori) bali na kitendo cha bikategoria. Makala hii inapendekeza kufafanua optiki zilizochanganywa kwa kutumia kitendo cha bikategoria $\mathbf{Prof}$ (ya kategoria, profunctor, na mabadiliko ya asili) kwenye kategoria za viwakilishi vya kushirikiana. Muundo wa optiki hizi unafafanuliwa kupitia ugani wa Kan, ikitoa msingi thabiti wa kategoria wa tabia yao ya kuunganishwa.

5. Optiki za Polynomial kama Kisa Maalum

Nadharia ya optiki zilizochanganywa inajumuisha optiki za polynomial. Optiki zinazotokana kama mabadiliko ya asili kati ya viendeshaji vya polynomial, zinazowakilishwa kama "ommatidia" katika kazi za awali, zinaonyeshwa kuwa kisa maalum cha mfumo wa jumla wa bikategoria. Wakati bikategoria inayotenda ni $\mathbf{Prof}$ na kategoria zinazotendwa ni kategoria za viwakilishi vya kushirikiana, optiki zilizochanganywa zinazotokana zinapatana hasa na optiki hizi zenye msingi wa polynomial.

6. Maelezo ya Kiufundi & Mfumo wa Hisabati

Mchango wa kiufundi wa msingi ni utengenezaji wa optiki kwa kutumia kitendo cha bikategoria na ugani wa Kan. Kwa kuzingatia bikategoria $\mathcal{B}$ inayotenda kwenye kategoria $\mathcal{X}$, na malengo ya kuzingatia yaliyogawanywa katika kategoria $\mathcal{A}$ na $\mathcal{B}$, optiki iliyochanganywa inaweza kufafanuliwa kama kiunganishi fulani cha ugani wa Kan:

$$\text{Optic}((A,B), (S,T)) \cong \int^{M \in \mathcal{B}} \mathcal{X}(\alpha(M, A), S) \times \mathcal{X}(T, \beta(M, B))$$

ambapo $\alpha$ na $\beta$ zinawakilisha kitendo cha pande mbili cha bikategoria. Hii inajumlisha fomula ya optiki rahisi kwa kubadilisha kategoria ya monoidal $\mathcal{M}$ na bikategoria $\mathcal{B}$ na vitendo $\bullet_1, \bullet_2$ na viendeshaji vya jumla zaidi $\alpha, \beta$ vinavyoheshimu muundo wa bikategoria.

7. Mfumo wa Kuchambua: Uelewa wa Msingi & Mtiririko wa Mantiki

Uelewa wa Msingi: Makala ya Milewski sio tu marekebisho mengine madogo ya nadharia ya lenzi; ni uboreshaji wa kimkakati wa mfumo mzima wa uendeshaji wa kategoria wa wafikiaji wa data wanaoweza kuunganishwa. Hatua ya kuhamia kutoka kwa aktigori za monoidal hadi vitendo vya bikategoria inalinganishwa na kujumlisha kutoka kwa mchakato wenye uzi mmoja hadi mfumo wa wakati mmoja, wenye mtandao. Dhana kuu ni kwamba ugumu wa kweli wa miundo ya kisasa ya data—fikiria vyombo vilivyojikita, aina tegemezi, au mpango wa grafu—ni wa pande nyingi kiasili na unahitaji mfumo ambapo "muktadha" ( $\mathcal{M}$ au $\mathcal{B}$ ) yenyewe ni huluki tajiri, ya muundo. Hii inalingana na mienendo katika nadharia ya kategoria iliyotumika, ambapo bikategoria na profunctor zinakuwa lugha ya kawaida kwa mifumo wazi na hesabu yenye ufahamu wa rasilimali, kama inavyoonekana katika kazi ya mitambo ya quantum ya kategoria au maktaba ya Coq kwa optiki.

Mtiririko wa Mantiki: Hoja inaendelea kwa usahihi wa upasuaji. Kwanza, inaweka mipaka ya utawala wa zamani: optiki rahisi, zilizojengwa juu ya vitendo vya monoidal, zilikwama na viendeshaji vya polynomial na muundo tofauti wa optiki. Uchunguzi ni kwamba kategoria ya monoidal $\mathcal{M}$ ni "bapa" mno kuiga miktadha tofauti, inayoshirikiana ya malengo changamano ya kuzingatia. Dawa ni bikategoria, ambazo hutoa muundo wa pande-2 unaohitajika kufuatilia mwingiliano huu. Uthibitisho wa dhana ni mzuri: onyesha kwamba bikategoria ya profunctor, $\mathbf{Prof}$, ikitenda kwenye viwakilishi vya kushirikiana, hutoa kiasili "ommatidia" za awali za optiki za polynomial. Kilele cha mantiki ni umoja: yale yaliyoonwa kama spishi tofauti (lenzi, prism, optiki za polynomial) sasa yanafunuliwa kuwa maonyesho ya jenasi moja ya bikategoria chini ya vigezo tofauti.

8. Nguvu, Mapungufu & Ufahamu Unaoweza Kutekelezwa

Nguvu:

  1. Uwezo wa Kuunganisha: Mfumo huu unajumuisha kwa mafanikio optiki za polynomial na muundo tofauti, ikipunguza mgawanyiko wa dhana.
  2. Uthabiti wa Hisabati: Kutumia dhana zilizothibitishwa vizuri kama bikategoria, profunctor, na ugani wa Kan kuhakikisha usahihi wa kinadharia na kuunganisha na idadi kubwa ya maarifa.
  3. Kuandaa Kwa Baadaye: Uundaji wa bikategoria kwa asili unaweza kuelezea zaidi, uko tayari kuiga optiki kwa mifumo mipya ya miundo ya data (k.m., ile inayohusisha utegemezi wa aina wenye mwelekeo au miktadha yenye athari).
Mapungufu & Mapengo Muhimu:
  1. Uwezekano wa Kukokotoa: Makala hii ni nzito kwenye uthibitisho wa uwepo na sifa za ulimwengu lakini nyepesi kwenye uelewa wa algoriti. Tunakukokotoa vipi na optiki hizi zilizochanganywa kwa ufanisi? Uundaji wa coend/ugani wa Kan unaweza kuwa wa kufikirika mno kwa watekelezaji. Linganisha hii na uwakilishi halisi wa lenzi za Van Laarhoven, ambazo zinaelekezwa moja kwa moja kwenye msimbo wa kazi.
  2. Uthibitishaji wa Kimajaribio Haupo: Hakuna utafiti wa kesi au kipimo kinachoonyesha kwamba mfumo huu uliojumlishwa unatatua tatizo la kweli la uhandisi wa programu ambalo optiki rahisi haziwezi. Bila hili, ina hatari ya kuwa suluhisho linalotafuta tatizo kwa watendaji.
  3. Mwinuko Mkubwa wa Kujifunza: Ujuzi wa sharti katika nadharia ya bikategoria na hesabu ya coend ni muhimu, ukiweza kupunguza kupitishwa nje ya duru za kitaaluma zinazolenga semantiki ya kategoria.
Ufahamu Unaoweza Kutekelezwa:
  1. Kwa Wabunifu wa Maktaba: Tumia makala hii kama nyota ya kaskazini kwa kubuni kizazi kijacho cha maktaba za optiki (k.m., katika `lens` ya Haskell au `monocle` ya Scala). Anza kutengeneza mfano wa "msingi wa bikategoria" unaoweza kurudi kwa ustadi kwenye optiki rahisi kwa visa vya kawaida lakini unaoweza kushughulikia optiki za polynomial na zilizounganishwa kiasili katika mfumo wa jumla.
  2. Kwa Watafiti: Hatua inayofuata ya haraka zaidi ni ufafanuzi halisi. Fuata njia ya makala asili ya "lenzi", ambayo ilileta maktaba za vitendo. Unda uwakilishi wa kawaida, halisi wa optiki zilizochanganywa (labda umbo la jumla la van Laarhoven) na utoe kikusanyaji kutoka kwa maelezo ya bikategoria hadi uwakilishi huu.
  3. Kwa Watendaji: Fuata mstari huu wa utafiti. Ingawa hauwezi kutekelezwa mara moja, unaonyesha mwelekeo wa dhana za hali ya juu za programu za kazi. Kuelewa hii sasa hutoa faida ya ushindani katika kubuni mifumo thabiti, inayolingana na wakati ujao.

9. Matumizi ya Baadaye & Mwelekeo wa Utafiti

Mfumo wa bikategoria wa optiki unafungua njia kadhaa zenye matumaini:

  1. Optiki kwa Aina Tegemezi: Kuiga lenzi na prism katika lugha zenye aina tegemezi (kama Agda au Idris) ni changamoto. Njia ya profunctor, ya bikategoria inaweza kutoa msingi safi zaidi wa semantiki kwa optiki katika mipangilio hii, ambapo aina zinaweza kutegemea thamani.
  2. Unganisho na Mifumo ya Athari: Bikategoria inayotenda inaweza kuanzishwa na kategoria za hesabu zenye athari (k.m., bikategoria ya monad). Hii inaweza kusababisha nadharia ya umoja ya "optiki zenye athari" zinazoshughulikia ufikiaji na usasishaji mbele ya I/O, hali, au kutokuwa na uhakika.
  3. Usasishaji wa Mtazamo wa Hifadhidata: Tatizo la usasishaji wa mtazamo katika hifadhidata ni matumizi ya kawaida ya lenzi. Optiki zilizochanganywa zinaweza kuiga ufafanuzi changamani zaidi wa mtazamo unaohusisha kuunganisha meza nyingi (miundo kama ya polynomial) na kutoa uthibitisho wa kategoria wa usahihi wa usambazaji wa usasishaji.
  4. Kujifunza kwa Mashine & Programu Tofauti: Kama inavyoonekana katika mifumo kama PyTorch au JAX, kufikia na kudhibiti sehemu za tensor changamani au grafu za kukokotoa ni muhimu. Mfumo wa jumla wa optiki unaweza kutoa API yenye kanuni, inayoweza kuunganishwa kwa udhibiti kama huo, na bikategoria ikishika muundo wa grafu ya kukokotoa yenyewe.
  5. Mabadiliko ya Pandembili (BX): Uwanja wa BX, unaochunguza vilinganishi kati ya uwakilishi tofauti wa data, una uhusiano mkubwa na lenzi. Mfumo huu wa optiki zilizochanganywa unaweza kutoa miundo mipya, inayoweza kuunganishwa zaidi kwa usawazishaji wa njia nyingi juu ya mpango changamani.

10. Marejeo

  1. Boisseau, G., & Gibbons, J. (2018). What You Needa Know about Yoneda: Profunctor Optics and the Yoneda Lemma. Proceedings of the ACM on Programming Languages.
  2. Riley, M. (2018). Categories of optics. arXiv preprint arXiv:1809.00738.
  3. Loregian, F. (2021). Coend Calculus. Cambridge University Press.
  4. Mac Lane, S. (1998). Categories for the Working Mathematician. Springer Science & Business Media.
  5. Pickering, M., Gibbons, J., & Wu, N. (2017). Profunctor optics: Modular data accessors. Art Science and Engineering of Programming.
  6. Spivak, D. I. (2020). Polynomial functors and ommatidia. arXiv preprint arXiv:2006.16941.
  7. Nester, C. (2022). Bicategories in Functional Programming: A Survey. Journal of Functional Programming.
  8. Abramsky, S., & Coecke, B. (2004). A categorical semantics of quantum protocols. Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science.
  9. Haskell `lens` library documentation and source code. https://hackage.haskell.org/package/lens
  10. nLab community wiki. Entries on Bicategory, Profunctor, Optic. https://ncatlab.org/nlab/show/HomePage