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:
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:
Morfizm
-algebr nazywamy też homomorfizmem
-algebr.
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:
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:
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

-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ą:
![{\displaystyle [0,s]\colon \mathbf {1} +\mathbb {N} \to \mathbb {N} }](https://wazniak.mimuw.edu.pl/api/rest_v1/media/math/render/svg/4fa4884121a27c95766772fd4d66f83f3a42922f)
. Oczywiście dodanie obiektu końcowego

jest funktorem (dowodzimy tego, używając własności uniwersalnych koproduktu

w

). A zatem
![{\displaystyle (\mathbb {N} ,[0,s])}](https://wazniak.mimuw.edu.pl/api/rest_v1/media/math/render/svg/a0ce2e6ba7b7e4f7f3e94901d8f78ca04a3c8c3b)
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:
Funkcja
jest więc - z początkowości algebry liczb naturalnych - jedyną funkcją, która sprawia, że poniższy diagram komutuje:

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:
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:
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]
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:
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ł:
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
.

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