Teoria kategorii dla informatyków/Wykład 15: Algebry i koalgebry endofunktorów

Z Studia Informatyczne
< Teoria kategorii dla informatyków
Wersja z dnia 12:42, 9 cze 2020 autorstwa Luki (dyskusja | edycje) (Zastępowanie tekstu - "\aligned" na "\begin{align}")
Przejdź do nawigacjiPrzejdź do wyszukiwania

Typy danych występujące w językach programowania bardzo dobrze poddają się opisowi algebraicznemu. Na przykład skończone listy czy drzewa są generowane nad pewnym alfabetem za pomocą konstruktorów, które można interpretować jako działania algebraiczne nad zbiorem słów z . Opis algebraiczny, abstrakcyjny, jest szczególnie przydatny we wszystkich tych sytuacjach, w których potrzebujemy specyfikacji danych niezależnych od ich późniejszej implementacji. Standardowe metody algebry uniwersalnej, wsparte na teorii kategorii, dobrze sprawdziły się w analizie skończonych typów danych, które są zwykle modelowane jako algebry początkowe dla odpowiednich funktorów. Tymczasem struktury nieskończone, na przykład: nieskończone listy, drzewa, potoki lub struktury generujące potencjalnie nieskończone obliczenia, jak: systemy tranzycyjne, automaty, nie poddają się łatwo opisowi algebraicznemu. Zupełnie niedawno stało się jasne, że do opisu struktur dynamicznych, nieskończonych, w informatyce znakomicie nadają się koalgebry, czyli obiekty dualne do algebr. Jak zobaczymy poniżej, listy nieskończone, drzewa nieskończone, automaty, itd. możemy modelować jako końcowe koalgebry dla odpowiednich funktorów. Nasz wykład jest jedynie krótkim wprowadzeniem w szeroką tematykę stosowania algebr i koalgebr do modelowania typów danych. Materiał do tego wykładu został w całości przygotowany w oparciu o artykuły naukowe Jana Ruttena z CWI w Amsterdamie i jego współautorów. Gorąco zachęcamy Czytelnika do sięgnięcia po te prace, z których szczególnie polecamy: A Tutorial on (Co)Algebras and (Co)Induction (z B. Jacobsem, Bulletin of Etacs, vol. 62, 1997, str. 222-259), Universal Coalgebra: A Theory of Systems (Raport techniczny CS-R9652, CWI Amsterdam, 1996) oraz On Streams and Coinduction (w: CRM Monograph vol. 23, AMS, 2004). Czytelnik znajdzie tam całe mnóstwo dodatkowych przykładów, wyjaśnień i wyników pogłębiających zaprezentowany tu materiał. W naszym mniemaniu prace nt. koindukcji znakomicie ilustrują odkrywczą rolę teorii kategorii w podstawach informatyki.


Algebry i koalgebry

Algebrę dla funktora definiujemy dokładnie tak samo, jak w Wykładzie 11 definiowalismy algebry dla monady. Różnica między tymi sytuacjami jest taka, że teraz nie wymagamy, by był częścią monady, wystarczy jedynie, że jest endofunktorem bardzo specyficznego typu . Dokładnie rzecz biorąc, mamy:


Definicja 15.1 [-algebra]

Dla funktora , parę , gdzie jest dowolnym zbiorem, natomiast , nazywamy -algebrą.


Algebry tworzą kategorię przy poniższej definicji morfizmu:


Definicja 15.2 [homomorfizm -algebr]

Homomorfizmem -algebr nazywamy każdą funkcję taką, że poniższy diagram komutuje:
Tk-15.0A.png


Dualnie:


Definicja 15.3 [-koalgebra, homomorfizm -koalgebr]

Dla funktora , parę , gdzie jest dowolnym zbiorem, zaś , nazywamy -koalgebrą. Morfizmem -koalgebr , nazywamy każdą funkcję taką, że poniższy diagram komutuje:
Tk-15.0B.png

Morfizm -algebr nazywamy też homomorfizmem -algebr.

Ilustracja3.png

Zbiór możemy nazywać zbiorem stanów, zaś funkcję dynamiką koalgebry (również: systemu) .

Kategorię -algebr będziemy oznaczali jako , zaś kategorię -koalgebr jako .

Algebrę nazywamy początkową, jeśli jest obiektem początkowym w ; koalgebrę nazywamy końcową, jeśli jest obiektem końcowym w kategorii . W praktyce nie mówi się zbyt dużo o algebrach końcowych i koalgebrach początkowych, gdyż są często trywialne. Ale dla równowagi algebry początkowe i koalgebry końcowe są arcyciekawe! Warto wypowiedzieć dokładnie definicje początkowej algebry i końcowej koalgebry. Podamy drugą z nich, zostawiając pierwszą Czytelnikowi:


Definicja 15.4 [-koalgebra końcowa]

-koalgebrę nazywamy końcową wtedy i tylko wtedy, gdy dla dowolnej innej koalgebry istnieje dokładnie jeden homomorfizm taki, że poniższy diagram komutuje:
Tk-15.1.png


Oczywiście własności uniwersalne obiektów początkowych (i końcowych) implikują, że algebry początkowe (i koalgebry końcowe), jeśli istnieją, to są jedyne z dokładnością do izomorfizmu. Warto, o co prosimy, nie mylić tej oczywistej cechy z następującą obserwacją Jima Lambeka:


Stwierdzenie 15.5 [Algebry początkowe są izomorfizmami]

-algebra początkowa jest izomorfizmem.
Uwaga
Twierdzenie Lambeka najłatwiej interpretować w ten sposób, że jeśli jest początkową -algebrą, to jest punktem stałym funktora . Rzeczywiście, skoro jest izomorfizmem, to .

Dowód

Niech będzie algebrą początkową. Aby pokazać, że jest izomorfizmem, musimy pokazać, że ma odwrotność . Funkcja musi być w szczególności homomorfizmem algebr, a co za tym idzie musi mieć strukturę algebry. Podobnie jak w przypadku algebr dla monady (Wykład 11.) widzimy, że jest rzeczywiście dobrym kandydatem, ponieważ z początkowości wynika, że istnieje dokładnie jeden morfizm taki, że poniższy diagram komutuje:
Tk-15.2.png

Wykażemy, że jest odwrotnością , tzn. . Z jednej strony:

Tk-15.3.png

a skoro jest z początkowości jedyną funkcją tego typu, dostajemy . Ale to równanie pozwala nam napisać:

(Pierwsza równość to komutowanie pierwszego z diagramów definiującego .). A zatem pokazaliśmy, że jest izomorfizmem z odwrotnością .

End of proof.gif


Dualnie, koalgebry końcowe są również izomorfizmami. Wielce ciekawym spostrzeżeniem jest również to, że dowód dualny do przedstawionego powyżej pokazuje nie tylko, że koalgebra końcowa jest izomorfizmem, ale również że:


Wniosek 15.6

-algebra jest początkowa wtedy i tylko wtedy, gdy -koalgebra skonstruowana w dowodzie Stwierdzenia 15.5 jest końcowa.


{uwaga|||Każdą -algebrę początkową można zatem uważać za najmniejszy punkt stały funktora , zaś każdą -koalgebrę końcową jako największy punkt stały funktora . Oczywiście algebry początkowe i koalgebry końcowe nie muszą istnieć.}}

Algebry i indukcja

Pokażemy teraz szereg przykładów algebr, wśród nich algebry początkowe. Z tymi ostatnimi jest nierozerwalnie związane pojęcie indukcji, które uogólnia pojęcie indukcji na liczbach naturalnych. W praktyce stykamy się z dwoma sposobami użycia indukcji: do definiowania obiektów (otrzymujemy tzw. definicje indukcyjne) i do dowodów faktów dotyczących obiektów zdefiniowanych indukcyjnie (takie dowody to tzw. dowody indukcyjne). Metoda indukcji jest niczym innym, niż zastosowaniem początkowości danej algebry. Powtórzmy to ważne zdanie jeszcze raz: Metoda indukcji to zastosowanie początkowości algebry. I tak na przykład twierdzenie o indukcji dla liczb naturalnych wynika bezpośrednio z faktu, że -algebra jest początkowa. Analizując rzecz dokładnie, początkowość -algebry oznacza, że dla dowolnej innej algebry istnieje dokładnie jeden} homomorfizm . Istnienie tego homomorfizmu odpowiada definicji indukcyjnej, zaś jedyność odpowiada dowodom indukcyjnym. Oto przykłady:


Przykład 15.7 [liczby naturalne]

{\rm Niech będzie zbiorem liczb naturalnych, zaś liczbą zero i funkcją następnika. Te dwie funkcje można połączyć w jedną: . Oczywiście dodanie obiektu końcowego jest funktorem (dowodzimy tego, używając własności uniwersalnych koproduktu w ). A zatem jest -algebrą. Ta algebra jest początkowa - patrz Zadanie 15.2. Ten fakt, zgodnie z twierdzeniem Lambeka (Stwierdzenie 15.5) daje nam izomorfizm , który w pełni, z dokładnością do izomorfizmu, charakteryzuje zbiór liczb naturalnych. Tak! Dowiedliśmy tego przecież w Wykładzie 1., w Fakcie 1.2!

Spróbujmy zdefiniować funkcję , która daje kolejne przybliżenia złotego środka tj. , , , i ogólnie . Struktura algebry, którą musimy zadać na to:

Tk-15.4.png

Funkcja jest więc - z początkowości algebry liczb naturalnych - jedyną funkcją, która sprawia, że poniższy diagram komutuje:

Tk-15.5.png
Funkcje zależne dodatkowo od pewnego parametru, na przykład typu , również da się zdefiniować, używając ich wersji kuryfikowanej. Dobrym przykładem jest tutaj Zadanie 15.3, gdzie definiujemy dodawanie liczb naturalnych.


Przykład 15.8 [algebra list skończonych]

Dla pewnego ustalonego zbioru rozważmy funktor . Ten funktor jest złożeniem produktu i funktora będącego podstawą poprzedniego przykładu. Pokażemy, że algebrą początkową tego funktora jest - monoid skończonych list nad alfabetem wraz z listą pustą i operacją dołączania litery do listy (czyli konkatenacji litery i listy):

Musimy pokazać, że dla dowolnej algebry istnieje dokładnie jeden homomorfizm jak na diagramie:

Tk-15.6.png

a taką funkcją jest niewątpliwie:

i jest to jedyna taka funkcja.


Uwaga
Przy tej definicji łatwo jest zwrócić uwagę na bardzo charakterystyczną cechę definiowania funkcji przez indukcję: definiujemy ją na wszystkich konstruktorach danej algebry. W tym wypadku wartość funkcji zdefiniowaliśmy na i na . W przypadku koindukcji będziemy postępowali dokładnie dualnie: zdefiniujemy funkcje przez koindukcję przez określenie wartości, jakie przyjmują na niej wszystkie destruktory danej koalgebry. Ale nie wybiegajmy zanadto w przyszłość.


Innym przykładem definiowania przez indukcję jest definicja funkcji określająca długość listy jako jedynej funkcji, która sprawia, że poniższy diagram komutuje:

Tk-15.7.png

gdzie jest rzutem na drugą współrzędną. Komutowanie diagramu oznacza oczywiście, że - po pierwsze: oraz - po drugie:

czego oczywiście się spodziewaliśmy.

Pokażmy teraz pierwszy przykład dowodu przez indukcję, który wynika z jedyności homomorfizmu z algebry początkowej. Niech będzie funkcją podwajającą listę: . Definiujemy ją jako jedyny homomorfizm, który sprawia, że poniższy diagram komutuje:

Tk-15.8.png

Chcielibyśmy teraz udowodnić, że długość listy jest dwukrotnie większa od długości listy , dla dowolnej , czyli że: . Dowód jest bardzo prosty: pokazujemy, że zarówno , jak i są homomorfizmami typu , więc muszą być równe, bo algebra list jest początkowa! Dowody homomorficzności wynikają natychmiast z komutowania poniższych diagramów:

Tk-15.9.png
Tk-15.10.png

To kończy dowód faktu, że .

Koalgebry i koindukcja

Koalgebry końcowe wraz ze swą metodą dowodzenia: koindukcją, pozostawały relatywnie nieznane, być może również dlatego, że wszelkie dowody koindukcyjne można przerobić na indukcyjne (biorąc dualną algebrę...). Istnienie koalgebr końcowych umożliwia nam definiowanie nowych funkcji i dowodzenie ich własności koindukcyjnych. Przyjrzyjmy się kilku przykładom.


Przykład 15.9 [systemy tranzycyjne]

Rozważmy etykietowany system tranzycyjny (porównaj ???) składający się ze zbioru stanów , relacji przejścia i zbioru etykiet . Notacja oznacza oczywiście . Z drugiej strony, rozważmy odwzorowanie . Jest ono funktorem typu , będącym złożeniem funktora potęgowego i funktora produktu. -koalgebrą będzie każda para , na którą możemy patrzeć jak na etykietowany system tranzycji, gdy zdefiniujemy:

Odwrotnie, dowolny system indukuje -koalgebrę , gdzie

Co więcej, każdy homomorfizm -koalgebr , jak łatwo sprawdzić, jest funkcją taką, że spełnione są dwa warunki:

  • Dla każdego , jeśli , to .
  • Dla każdego , jeśli , to
istnieje taki, że i . A zatem etykietowane systemy tranzycyjne wraz z funkcjami zachowującymi i odzwierciedlającymi tranzycje (jak w dwóch warunkach powyżej) tworzą kategorię izomorficzną z kategorią -koalgebr .


W zasadzie powyższa konstrukcja ma kilka możliwych wariacji w zależności od funktora . Dla identyczności, -koalgebry odpowiadają deterministycznym systemom dynamicznym z dynamiką . Dla funktora stałego , , , można pokazać, że kategoria jest izomorficzna z , co oznacza, że na każdym zbiorze można zadać strukturę (trywialnej) -koalgebry. Innym przykładem są systemy dynamiczne z terminacją, które są koalgebrami funktora . Systemy dynamiczne niedeterministyczne to koalgebry funktora potęgowego. A oto jeszcze jeden ważny przykład:


Przykład 15.10 [automaty lub nieskończone listy]

Niech będzie dowolnym zbiorem. Dla funktora , -koalgebrą jest każda para . Gdy interpretujemy jako zbiór stanów, jako zbiór stanów końcowych, funkcję jako wyjście, jako funkcję przejścia, to ta koalgebra jest automatem deterministycznym. Homomorfizm dwóch automatów to funkcja , która spełnia równania , , czyli jest to jedyna funkcja taka, że poniższy diagram komutuje:
Tk-15.11.png

Zwróćmy baczną uwagę na fakt, że - dualnie do sytuacji z algebrami - aby zdefiniować homomorfizm dwóch koalgebr, musimy pokazać w jaki sposób destruktory koalgebry zachowują się na wartościach (dla algebr musieliśmy w takim wypadku wskazać, jakie wartości przyjmował na konstruktorach algebry).

Szczególną -koalgebrę dostaniemy, gdy wybierzemy jako zbiór stanów nieskończone listy (potoki) nad zbiorem , tzn. (czy też, jak kto woli ). Jeśli przyjmiemy dla prostoty zapisu:



to dla , oraz , dostaniemy koalgebrę . (W interpretacji jako listy nieskończonej, funkcja bywa też nazywana , zaś funkcja - .) Zanim pokażemy, że ta koalgebra jest końcowa, wprowadźmy pewną metodę dowodzenia zwaną koindukcją.

Dowodzenie przez koindukcję

Definicja 15.11 [bisymulacja]

Niech i będą dwiema -koalgebrami. Podzbiór nazywamy bisymulacją między i , jeśli na da się zadać strukturę -koalgebry w taki sposób, aby projekcje , były homomorfizmami, tzn. tak, aby poniższy diagram komutował:
Tk-15.12.png

Jeśli , to nz. bisymulacją na .


O bisymulacji na początek wystarczy wiedzieć tyle, że: (a) przekątna jest bisymulacją na ; (b) relacja odwrotna do bisymulacji jest bisymulacją; (c) dowolna suma bisymulacji jest bisymulacją. Dwóch z tych faktów dowodzimy w Zadaniu 15.6. Złożenie dwóch bisymulacji (tam, gdzie ma to sens) nie musi być bisymulacją, gdyż zależy od zachowywania granic przez funktor . W końcu można pokazać, że rodzina wszystkich bisymulacji tego samego typu tworzy kratę zupełną, której elementem największym jest bisymulacja będąca relacją równoważności: wtedy i tylko wtedy, gdy istnieje bisymulacja taka, że .

Zadanie 15.5 opisuje bisymulacje dla funktora z Przykładu 15.9. My wracamy do nieskończonych list, wyróżniając ten szczególny przypadek definicją:


Definicja 15.12 [bisymulacja dla nieskończonych list]

Bisymulacją na jest relacja taka, że dla dowolnych , jeśli , to:
  • oraz
  • .


Jeśli istnieje bisymulacja taka, że , to piszemy i mówimy, iż są bipodobne (ang. bisimilar). Bipodobieństwo jest oczywiście największą z bisymulacji na .


Udowodnimy najważniejsze (a jakże proste!) twierdzenie tego wykładu:


Twierdzenie 15.13 [metoda koindukcji dla nieskończonych list]

Dla dowolnych :

Dowód

Niech będzie bisymulacją taką, że (taka istnieje, bo z założenia ). Prosty dowód używający szkolnej indukcji na liczbach naturalnych pozwoli nam zobaczyć, że , gdzie indeks odnosi się do -tej pochodnej , tj.:

Znów ponieważ jest bisymulacją, , czyli po prostu dla dowolnego . To znaczy, że .

End of proof.gif


Uwaga
Dla dowolnej innej końcowej -koalgebry twierdzenie powyższe uogólnia się do następującej postaci: dla każdej bisymulacji na , . Twierdzenie to wygląda niepozornie, nieprawdaż?


Zastosujmy natychmiast twierdzenie o koindukcji, by udowodnić, że:


Stwierdzenie 15.14

jest koalgebrą końcową funktora .

Dowód

Pokażemy, że dla dowolnego innego automatu istnieje dokładnie jeden homomorfizm taki, że poniższy diagram komutuje:
Tk-15.13.png

Połóżmy dla dowolnego :

Przy tej definicji diagram oczywiście komutuje. Jeśli jest inną funkcją sprawiającą, że tenże diagram komutuje, to aby pokazać równość na mocy twierdzenia o koindukcji, wystarczy wykazać, że relacja:

jest bisymulacją na . Oto dowód: niech . Ponieważ i są homomorfizmami, oraz i . Ponieważ , dowiedliśmy, że jest bisymulacją. Z twierdzenia o koindukcji mamy .

End of proof.gif


Końcowość koalgebry pozwala w sposób formalny definiować nieskończone listy (i operacje na nieskończonych listach), mając dane (podobnie jak w równaniach różniczkowych) warunek początkowy dla listy wraz z pochodną takiej listy. Wyjaśnimy to na przykładzie: załóżmy, że chcemy rozwiązać równanie (posiadające warunek początkowy i warunek na pochodną): przy warunku . Jest oczywiste, że rozwiązaniem musi być lista , ale formalnie postępujemy tak: rozważamy automat . Niech będzie jedynym homomorfizmem w . Dla otrzymujemy oraz . A zatem rozwiązanie szukanego równania istnieje. Jest jedyne, bo jeśli jest innym rozwiązaniem, to jest bisymulacją na , skąd dostajemy: z twierdzenia o koindukcji.

Na koniec pokażmy jeszcze przykład dowodzenia własności nieskończonych list przez koindukcję. W Zadaniu 15.7 definiujemy dwie operacje na listach:

Po pierwsze, istnieje operacja , która spełnia:

oraz

Istnienie udowadniamy tak samo jak w poprzednim przykładzie, zaczynając od równania przy warunku . (Dokładniej mówiąc, dla jedynego homomorfizmu , gdzie , , .)

Pokażemy przez koindukcję, że:

Zdefiniujmy relację:

Zauważmy, że

a także

To dowodzi, że jest bisymulacją, a zatem z twierdzenia o koindukcji dostajemy żądaną równość.

Jeszcze jeden przykład dowodu przez koindukcję znajdzie Czytelnik w Zadaniu 15.8. My zmierzamy do konkluzji: pokazaliśmy, że obok znanej metody indukcji na początkowych algebrach istnieje - zgodnie z kategoryjną zasadą dualności - metoda koindukcji służąca do definiowania i dowodzenia własności struktur nieskończonych, dynamicznych. Pokazaliśmy też, jak użytecznym narzędziem może być własność uniwersalna początkowych algebr i końcowych koalgebr. Zachęcamy Czytelnika do dalszej lektury artykułów, o których wspomnieliśmy na początku wykładu i do studiowania teorii kategorii, która znajduje jeszcze wiele dalszych zastosowań w informatyce, o których nie mieliśmy sposobności wspomnieć. Powodzenia!

Ilustracja1.png