Teoria kategorii dla informatyków/Wykład 15: Algebry i koalgebry endofunktorów
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 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.
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:
Algebry i koalgebry
Algebrę dla funktora 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:
definiujemy dokładnie tak samo, jak w
Definicja 15.1 [
-algebra]
Algebry tworzą kategorię przy poniższej definicji morfizmu:
Definicja 15.2 [homomorfizm
-algebr]
Dualnie:
Definicja 15.3 [
-koalgebra, homomorfizm -koalgebr]

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]
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]
Dowód

Wykażemy, że
jest odwrotnością , tzn. . Z jednej strony:
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ą .
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
{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]
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:
Funkcja
jest więc - z początkowości algebry liczb naturalnych - jedyną funkcją, która sprawia, że poniższy diagram komutuje:
Przykład 15.8 [algebra list skończonych]
Musimy pokazać, że dla dowolnej algebry
istnieje dokładnie jeden homomorfizm jak na diagramie:
a taką funkcją jest niewątpliwie:
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:

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:
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:

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]
Odwrotnie, dowolny system
indukuje -koalgebrę , gdzieCo 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
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]

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:
Dowodzenie przez koindukcję
Definicja 15.11 [bisymulacja]
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ł:
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]
- 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]
Dowód
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.:
Zastosujmy natychmiast twierdzenie o koindukcji, by udowodnić, że:
Stwierdzenie 15.14
Dowód

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 .
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!
