Solidne zastosowania teorii kategorii w TCS?

Nauczyłem się kilku fragmentów teorii kategorii. Z pewnością jest to inny sposób patrzenia na rzeczy. (Bardzo ogólne podsumowanie dla tych, którzy go nie widzieli: teoria kategorii daje sposoby wyrażania wszelkiego rodzaju zachowań matematycznych wyłącznie w kategoriach funkcjonalnych związków między obiektami. Na przykład rzeczy takie jak iloczyn kartezjański dwóch zbiorów są zdefiniowane całkowicie w kategoriach jak zachowują się inne funkcje, a nie pod względem tego, jakie elementy są elementami zestawu.)

Mam niejasne zrozumienie, że teoria kategorii jest przydatna po stronie języków programowania / logiki („Teoria B”) i zastanawiam się, ile algorytmów i złożoności („Teoria A”) może skorzystać. Może jednak pomóc mi oderwać się od ziemi, jeśli znam pewne solidne zastosowania teorii kategorii w Teorii B. (Już domyślnie zakładam, że do tej pory nie znaleziono żadnych zastosowań w Teorii A, ale jeśli je macie, to nawet lepiej dla mnie!)

Przez „solidne zastosowanie” mam na myśli:

(1) Aplikacja zależy tak mocno od teorii kategorii, że bardzo trudno ją osiągnąć bez użycia maszyny.

(2) Aplikacja przywołuje co najmniej jedno nietrywialne twierdzenie teorii kategorii (np. Lemat Yonedy).

Możliwe, że (1) oznacza (2), ale chcę się upewnić, że są to „prawdziwe” aplikacje.

Chociaż mam pewne doświadczenie z „Teorią B”, minęło trochę czasu, więc doceniam każdą de-żargonizację.

(W zależności od tego, jakie odpowiedzi otrzymam, mogę później przekształcić to pytanie w wiki społeczności. Ale naprawdę chcę dobrych aplikacji z dobrymi objaśnieniami, więc wstydem jest nie nagradzanie czegoś odpowiadającego).

Mogę wymyślić jeden przypadek, w którym teoria kategorii została bezpośrednio „zastosowana” w celu rozwiązania otwartego problemu w językach programowania: Thorsten Altenkirch, Peter Dybjer, Martin Hofmann i Phil Scott, „Normalizacja przez ocenę dla typowego rachunku lambda z koproduktami” . Z ich streszczenia: „Rozwiązujemy problem decyzyjny dla po prostu wpisanego rachunku lambda z silnymi sumami binarnymi, równoważnie problem słowny dla wolnych kartezjańskich zamkniętych kategorii z binarnymi koproduktami. Nasza metoda opiera się na technice semantycznej znanej jako„ normalizacja przez ocenę ”i obejmuje odwracając interpretację składni na odpowiedni model snopa i z tego wydobywając odpowiednie unikalne formy normalne. ”

Ogólnie jednak myślę, że teoria kategorii nie jest zwykle stosowana do udowodnienia głębokich twierdzeń w językach programowania (których nie ma tak wielu), ale oferuje raczej koncepcyjne ramy, które są często przydatne (na przykład w powyższym idea semantyki (przed) snopa).

Ważnym przykładem historycznym jest sugestia Eugenio Moggiego, że pojęcie monady (która jest podstawowa i wszechobecna w teorii kategorii) może być użyte jako część semantycznego wyjaśnienia skutków ubocznych w językach programowania (np. Stan, niedeterminizm). To zainspirowało również do refleksji na temat składni języków programowania, na przykład prowadzącej bezpośrednio do „Monec typeclass” w Haskell (używanej do enkapsulacji efektów).

Niedawno (ostatnia dekada) to wyjaśnienie skutków w odniesieniu do monad zostało ponownie przeanalizowane z punktu widzenia starego związku (ustanowionego przez teoretyków kategorii, w latach 60.) między monadami a teoriami algebraicznymi: patrz Martin Hyland i John Power , „Kategoria teoretycznego zrozumienia algebry uniwersalnej: teorie i monady Lawvere” . Chodzi o to, że monadyczny widok efektów jest zgodny z (pod pewnymi względami bardziej atrakcyjnym) algebraicznym widokiem efektów, w którym efekty (np. Sklep) można wyjaśnić w kategoriach operacji (np. „Wyszukiwanie” i „aktualizacja”) i powiązane równania (np. idempotency aktualizacji). Niedawny artykuł na ten temat autorstwa Paula-André Mellièsa: „Segal warunek spełnia efekty obliczeniowe”, który również w dużej mierze opiera się na ideach pochodzących z „teorii wyższej kategorii” (na przykład pojęcie „struktury Yonedy” jako sposobu organizacji semantyki presheaf).

Kolejna pokrewna klasa przykładów pochodzi z logiki liniowej . Wkrótce po wprowadzeniu przez Jean-Yvesa Girarda w latach 80. (w celu lepszego zrozumienia logiki konstruktywnej), ustanowiono trwałe powiązania z teorią kategorii. Aby uzyskać wyjaśnienie tego połączenia, zobacz John Baez i Mike Stay, „Fizyka, topologia, logika i obliczenia: kamień z Rosetty” .

Wreszcie odpowiedź ta byłaby niepełna bez odniesienia do oświecającego bloga sigfpe „A Neighborhood of infinity” . W szczególności możesz sprawdzić „Częściowe uporządkowanie niektórych teorii kategorii zastosowanych do Haskell” .

Obliczenia kwantowe

Bardzo interesującym obszarem jest zastosowanie różnych kategorii monoidalnych do obliczeń kwantowych. Niektórzy mogą twierdzić, że jest to również fizyka, ale pracę wykonują ludzie z działów informatyki. Wczesny artykuł na ten temat to Kategoryczna semantyka protokołów kwantowych autorstwa Samsona Abramsky'ego i Boba Coecke; wiele ostatnich prac Abramsky'ego i Coecke'a oraz innych kontynuuje prace w tym kierunku.

W tej części pracy protokoły kwantowe są aksjatyzowane jako (niektóre rodzaje) zwartych zamkniętych kategorii. Takie kategorie mają piękny język graficzny pod względem schematów ciągów (i wstążek). Równania w kategorii odpowiadają niektórym ruchom struny, takim jak prostowanie splątanego, ale nie wiązanego struny, co z kolei odpowiada coś znaczącego w mechanice kwantowej, takiego jak teleportacja kwantowa.

Podejście kategoryczne oferuje logiczny widok na wysokim poziomie, co zwykle wymaga obliczeń na bardzo niskim poziomie.

Teoria systemów

$F$$F$

Transformacje grafów

$G_1,G_2$$P$$e_1:P\to G_1$$e_2:P\to G_2$$G_1$$G_2$$G_1$$G_2$$P$

$(L, K, R)$$L$$R$$K$$l:K\to L$$r:K\to R$$L\setminus K$$R\setminus K$$d$$K$$D$$d$$l$$G$$d$$k$

Języki programowania (przez MathOverflow)

Istnieje wiele zastosowań teorii kategorii w projektowaniu języków programowania i teorii języków programowania. Obszerne odpowiedzi można znaleźć w MathOverflow. https://mathoverflow.net/questions/3721/programming-languages-based-on-category-theory ) https://mathoverflow.net/questions/4235/relating-category-theory-to-programming-language-theory .

Bigraphs - Process Calculi

Wreszcie są bigraphy Milnera , ogólne ramy do opisywania i wnioskowania na temat systemów agentów wchodzących w interakcje. Można to postrzegać jako ogólne ramy rozumowania na temat algeb procesów i ich strukturalnych i behawioralnych teorii. Podejście opiera się również na wypychaniach.

Już domyślnie zakładam, że do tej pory nie znaleziono żadnych aplikacji w teorii A, ale jeśli masz niektóre z nich, jest to dla mnie jeszcze lepsze!

• Rozumiem, że teoria gatunków Joyal'ego jest stosunkowo szeroko stosowana w kombinatorykach wyliczeniowych, jako uogólnienie funkcji generujących, które dodatkowo podpowiadają, jak permutować rzeczy oprócz ich liczby.

• Pippenger zastosował dualność kamienną, aby odnieść się do regularnych języków i odmian półgrup. Jeandel wprowadził automaty topologiczne, które stosują te pomysły, aby ujednolicić rachunki (i dowody!) Dla automatów kwantowych, probabilistycznych i zwykłych.

• Roland Backhouse przedstawił abstrakcyjne charakterystyki chciwych algorytmów za pomocą powiązań Galois z tropikalnym semirowaniem.

W znacznie bardziej spekulatywnym tonie Noam wspomniał o modelach snopków. Te abstrakcyjnie charakteryzują technikę syntaktyczną relacji logicznych, która jest prawdopodobnie jedną z najpotężniejszych technik semantyki. Najczęściej używamy ich do udowodnienia wyników niewyrażalności i spójności, ale powinno to być interesujące dla teoretyków złożoności, ponieważ jest to dobry przykład praktycznej nienaturalnej (w sensie Razborova / Rudicha) techniki dowodu. (Jednak relacje logiczne są zwykle bardzo starannie zaprojektowane, aby zagwarantować ich relatywizację - jako projektanci języków chcemy być w stanie zapewnić programistom, że wywołania funkcji są czarnymi skrzynkami!)

EDYCJA: Będę kontynuował spekulacje, na prośbę Ryana. Jak rozumiem, naturalnym dowodem jest z grubsza próba zdefiniowania indukcyjnego niezmiennika struktury obwodu, podlegającego różnym rozsądnym warunkom. Podobne pomysły są (co nie dziwi) dość powszechne również w językach programowania, gdy próbujesz zdefiniować niezmiennik utrzymywany indukcyjnie za pomocą rachunku lambda (na przykład, aby udowodnić bezpieczeństwo typu). 1

$A \to B$$A \to B$$A$

$A \to B$$A$$B$. Zauważ, że nie ma pojedynczego niezmiennika indukcyjnego - definiujemy całą rodzinę niezmienników poprzez rekurencję w strukturze danych wejściowych i używamy innych środków, aby pokazać, że wszystkie warunki leżą w obrębie tych niezmienników. Dowód teoretyczny jest znacznie silniejszą techniką i pozwala udowodnić spójność wyników.

Związek z rolkami wynika z faktu, że często musimy rozumować o terminach otwartych (tj. Terminach z wolnymi zmiennymi), a zatem musimy rozróżnić między utknięciem z powodu błędów a utknięciem z powodu konieczności zmniejszenia zmiennej. Krążki wynikają z rozważania redukcji rachunku lambda jako definiowania morfizmów kategorii, której terminami są obiekty (tj. Częściowy porządek indukowany przez redukcję), a następnie z rozważania funktorów z tej kategorii na zbiory (tj. Predykaty). Jean Gallier napisał na ten temat kilka fajnych artykułów na początku 2000 roku, ale wątpię, aby były one czytelne, chyba że zasymilowałeś już dość dużą liczbę rachunków lambda.

Istnieje wiele przykładów, z których pierwszy przychodzi na myśl zastosowanie teorii kategorii przez Alexa Simpsona do udowodnienia właściwości języków programowania, patrz np. „ Adekwatność obliczeniowa dla typów rekurencyjnych w modelach intuicyjnej teorii zbiorów”, Annals of Pure and Applied Logic , 130: 207-275, 2004. Mimo że w tytule wspomniano o teorii mnogości, technika jest teoretyczna. Zobacz stronę główną Alexa, aby uzyskać więcej przykładów.

Myślę, że zadajesz dwa pytania dotyczące zastosowania, typu A i typu B osobno.

Jak zauważasz, istnieje wiele merytorycznych zastosowań teorii kategorii do tematów typu B: semantyka języków programowania (monady, kartezjańskie kategorie zamknięte), logika i sprawdzalność (topoi, odmiany logiki liniowej).

Wydaje się jednak, że mało jest merytorycznych zastosowań teorii A (algorytmy lub złożoność).

Istnieją pewne zastosowania w obiektach elementarnych, takie jak opisywanie kategorii automatów lub obiektów kombinatorycznych (wykresy, sekwencje, permutacje itp.). Ale nie wydają się one wyjaśniać głębszego zrozumienia teorii języka lub algorytmów.

Spekulacyjnie może to być niedopasowanie obecnych strategii teorii kategorii i przedmiotów teorii A:

• Centralną strategią teorii kategorii jest radzenie sobie z równością (kiedy rzeczy są takie same, a kiedy są różne i jak się ze sobą mapują).

• W przypadku teorii złożoności podstawową strategią są redukcje i ustalanie granic (można by pomyśleć, że redukcja jest jak strzała, ale nie sądzę, aby zbadano coś poza tym powierzchownym podobieństwem).

• W przypadku algorytmów nie ma nadrzędnej strategii innej niż sprytne myślenie kombinatoryczne ad hoc. W przypadku niektórych domen spodziewałbym się, że może być owocna eksploracja (algorytmy algebry?), Ale jeszcze jej nie widziałem.

„TCS-A”, które przychodzą mi na myśl, to gatunki kombinatoryczne Joyal (uogólnienia szeregów mocy na funktory, aby opisać obiekty kombinatoryczne, takie jak drzewa, zbiory, multisety itp.) Oraz formalizacja kryptograficznego „przeskakiwania” przy użyciu relacji, probabilistyczna logika Hoare'a (Easycrypt, Certicrypt, praca Andreasa Lochbihlera). Podczas gdy kategorie nie pojawiają się bezpośrednio w tym ostatnim, były one pomocne w rozwoju podstawowej logiki (np. Monady).

PS: Odkąd wymieniono moje imię w pierwszej odpowiedzi: użycie fibracji grupoidów w celu wykazania niemożności uzyskania pewnej pewnej aksjomatu w teorii typów Martina-Löfa przez Thomasa Streichera i mnie może być również uznane za „solidne” zastosowanie teorii kategorii (choć w logice lub „TCS-B”).

Nowsza książka Seven Sketches in Compositionality wymienia kilka zastosowań teorii kategorii w informatyce i inżynierii. Warto zwrócić uwagę na rozdział dotyczący baz danych, w którym autorzy opisują zapytania, łączenie, migrację i ewolucję baz danych w oparciu o model kategoryczny. Autorzy posunęli się dalej i opracowali język CQL (QuQLical Query Language ) oraz zintegrowane środowisko programistyczne (IDE) w oparciu o ich kategoryczny model baz danych.