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 $\Sigma$ za pomocą konstruktorów, które można interpretować jako działania algebraiczne nad zbiorem słów z $\Sigma$. 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 $T\colon \mathbf {Set} \to \mathbf {Set}$ 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 $T$ był częścią monady, wystarczy jedynie, że jest endofunktorem bardzo specyficznego typu $\mathbf {Set} \to \mathbf {Set}$. Dokładnie rzecz biorąc, mamy:

Definicja 15.1 [$T$-algebra]

Dla funktora $T\colon \mathbf {Set} \to \mathbf {Set}$, parę $(X,a)$, gdzie $X$ jest dowolnym zbiorem, natomiast $a\colon TX\to X$, nazywamy $T$-algebrą.

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

Definicja 15.2 [homomorfizm $T$-algebr]

Homomorfizmem $T$-algebr $f\colon (X,a)\to (Y,b)$ nazywamy każdą funkcję $f\colon X\to Y$ taką, że poniższy diagram komutuje:

Dualnie:

Definicja 15.3 [$T$-koalgebra, homomorfizm $T$-koalgebr]

Dla funktora $T\colon \mathbf {Set} \to \mathbf {Set}$, parę $(X,a)$, gdzie $X$ jest dowolnym zbiorem, zaś $a\colon X\to TX$, nazywamy $T$-koalgebrą. Morfizmem $T$-koalgebr $(X,a)$, $(Y,b)$ nazywamy każdą funkcję $f\colon X\to Y$ taką, że poniższy diagram komutuje:

Morfizm $T$-algebr nazywamy też homomorfizmem $T$-algebr.

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

Kategorię $T$-algebr będziemy oznaczali jako $\mathbf {Set} ^{T}$, zaś kategorię $T$-koalgebr jako $\mathbf {Set} _{T}$.

Algebrę nazywamy początkową, jeśli jest obiektem początkowym w $\mathbf {Set} ^{T}$; koalgebrę nazywamy końcową, jeśli jest obiektem końcowym w kategorii $\mathbf {Set} _{T}$. 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 [$T$-koalgebra końcowa]

$T$-koalgebrę $(X,a)$ nazywamy końcową wtedy i tylko wtedy, gdy dla dowolnej innej koalgebry $(Z,c)$ istnieje dokładnie jeden homomorfizm $f\colon (Z,c)\to (X,a)$ 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]

$T$-algebra początkowa jest izomorfizmem.

Uwaga

Twierdzenie Lambeka najłatwiej interpretować w ten sposób, że jeśli $(X,a)$ jest początkową $T$-algebrą, to $X$ jest punktem stałym funktora $T$. Rzeczywiście, skoro $a\colon TX\to X$ jest izomorfizmem, to $TX\cong X$.

Dowód

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

Wykażemy, że $b$ jest odwrotnością $a$, tzn. $b=a^{-1}$. Z jednej strony:

a skoro $1_{X}\colon (X,a)\to (X,a)$ jest z początkowości jedyną funkcją tego typu, dostajemy $a\circ b=1_{X}$. Ale to równanie pozwala nam napisać:

$b\circ a=T(a)\circ T(b)=T(a\circ b)=T(1_{X})=1_{TX}.$

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

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 $a^{-1}\colon X\to TX$ jest izomorfizmem, ale również że:

Wniosek 15.6

$T$-algebra $(X,a\colon TX\to X)$ jest początkowa wtedy i tylko wtedy, gdy $T$-koalgebra $(TX,a^{-1}\colon X\to TX)$ skonstruowana w dowodzie Stwierdzenia 15.5 jest końcowa.

{uwaga|||Każdą $T$-algebrę początkową można zatem uważać za najmniejszy punkt stały funktora $T$, zaś każdą $T$-koalgebrę końcową jako największy punkt stały funktora $T$. 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 $\mathbf {1} +(-)$-algebra $(\mathbb {N} ,[0,s]\colon \mathbf {1} +\mathbb {N} \to \mathbb {N} )$ jest początkowa. Analizując rzecz dokładnie, początkowość $T$-algebry $(X,a)$ oznacza, że dla dowolnej innej algebry $(Y,b)$ istnieje dokładnie jeden} homomorfizm $f\colon (X,a)\to (Y,b)$. Istnienie tego homomorfizmu odpowiada definicji indukcyjnej, zaś jedyność odpowiada dowodom indukcyjnym. Oto przykłady:

Przykład 15.7 [liczby naturalne]

{\rm Niech $\mathbb {N}$ będzie zbiorem liczb naturalnych, zaś $0\colon \mathbf {1} \to \mathbb {N}$ liczbą zero i $s\colon \mathbb {N} \to \mathbb {N}$ funkcją następnika. Te dwie funkcje można połączyć w jedną: $[0,s]\colon \mathbf {1} +\mathbb {N} \to \mathbb {N}$. Oczywiście dodanie obiektu końcowego $\mathbf {1} +(-)$ jest funktorem (dowodzimy tego, używając własności uniwersalnych koproduktu $+$ w $\mathbf {Set}$). A zatem $(\mathbb {N} ,[0,s])$ jest $\mathbf {1} +(-)$-algebrą. Ta algebra jest początkowa - patrz Zadanie 15.2. Ten fakt, zgodnie z twierdzeniem Lambeka (Stwierdzenie 15.5) daje nam izomorfizm $\mathbb {N} \cong \mathbf {1} +\mathbb {N}$, 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ę $f\colon \mathbb {N} \to \mathbb {Q}$, która daje kolejne przybliżenia złotego środka $\phi =0,6180339...$ tj. $f(0):=1$, $f(1):=1/2$, $f(2):=2/3$, $f(3):=3/5$ i ogólnie $f(n+1):=1/(f(n)+1)$. Struktura algebry, którą musimy zadać na $\mathbb {Q}$ to:

Funkcja $f(n)={\frac {1}{f(n)+1}}$ 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 $\mathbb {N} \times \mathbb {N} \to \mathbb {N}$, 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 $A$ rozważmy funktor $T(-):=\mathbf {1} +(A\times (-))$. 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 $\mathrm {List} (A)$ - monoid skończonych list nad alfabetem $A$ wraz z listą pustą $\varepsilon \colon \mathbf {1} \to \mathrm {List} (A)$ i operacją ${\mathtt {cons}}\colon A\times \mathrm {List} (A)\to \mathrm {List} (A)$ dołączania litery do listy (czyli konkatenacji litery i listy): ${\mathtt {cons}}(a,\alpha ):=a\alpha .$

Musimy pokazać, że dla dowolnej algebry $(X,[u,h]\colon \mathbf {1} +(A\times x)\to X)$ istnieje dokładnie jeden homomorfizm $f\colon \mathrm {List} (A)\to X$ jak na diagramie:

a taką funkcją jest niewątpliwie:

$f(\alpha ):={\begin{cases}u,&\alpha =\varepsilon \\h(a,f(\beta )),&\alpha ={\mathtt {cons}}(a,\beta )\end{cases}}$ 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 $f$ zdefiniowaliśmy na $\varepsilon$ i na ${\mathtt {cons}}$. 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 $l\colon \mathrm {List} (A)\to \mathbb {N}$ określająca długość listy jako jedynej funkcji, która sprawia, że poniższy diagram komutuje:

gdzie $\pi$ jest rzutem na drugą współrzędną. Komutowanie diagramu oznacza oczywiście, że - po pierwsze: $l(\varepsilon )=0$ oraz - po drugie:

$l({\mathtt {cons}}(a,\alpha )=(s\circ \pi )(1_{A}\times l)(a,\alpha )=s(\pi (a,l(\alpha )))=s(l(\alpha ))=l(\alpha )+1,$

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 $d\colon \mathrm {List} (A)\to \mathrm {List} (A)$ będzie funkcją podwajającą listę: $d(\alpha ):=\alpha \alpha$. Definiujemy ją jako jedyny homomorfizm, który sprawia, że poniższy diagram komutuje:

Chcielibyśmy teraz udowodnić, że długość listy $d(\alpha )$ jest dwukrotnie większa od długości listy $\alpha$, dla dowolnej $\alpha$, czyli że: $l\circ d=2(-)\circ l$. Dowód jest bardzo prosty: pokazujemy, że zarówno $l\circ d$, jak i $2(-)\circ l$ są homomorfizmami typu $(\mathrm {List} (A),[\varepsilon ,{\mathtt {cons}}])\to (\mathbb {N} ,[0,s\circ s\circ \pi ])$, 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 $l(d(\alpha ))=2l(\alpha )$.

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 $(S,\longrightarrow ,A)$ (porównaj ???) składający się ze zbioru stanów $S$, relacji przejścia $\longrightarrow \subseteq S\times A\times S$ i zbioru etykiet $A$. Notacja $s{\stackrel {a}{\longrightarrow }}z$ oznacza oczywiście $(s,a,z)\in \longrightarrow$. Z drugiej strony, rozważmy odwzorowanie $T(-):={\mathcal {P}}(A\times (-))$. Jest ono funktorem typu $\mathbf {Set} \to \mathbf {Set}$, będącym złożeniem funktora potęgowego i funktora produktu. $T$-koalgebrą będzie każda para $(S,\alpha \colon S\to TS)$, na którą możemy patrzeć jak na etykietowany system tranzycji, gdy zdefiniujemy: $s{\stackrel {a}{\longrightarrow }}z\iff (a,z)\in \alpha (s).$

Odwrotnie, dowolny system $(S,\to ,A)$ indukuje $T$-koalgebrę $(S,\alpha \colon S\to TS)$, gdzie

$\alpha (s):=\{(a,z)\mid s{\stackrel {a}{\longrightarrow }}z\}.$

Co więcej, każdy homomorfizm $T$-koalgebr $f\colon (S,\to _{S},A)\to (Z,\to _{Z},B)$, jak łatwo sprawdzić, jest funkcją $f\colon S\to Z$ taką, że spełnione są dwa warunki:

• Dla każdego $s'\in S$, jeśli $s{\stackrel {a}{\longrightarrow _{S}}}s'$, to $fs{\stackrel {fa}{\longrightarrow _{Z}}}fs'$.
• Dla każdego $z\in Z$, jeśli $fs{\stackrel {a}{\longrightarrow _{Z}}}z$, to

istnieje $s'\in S$ taki, że $s{\stackrel {a}{\longrightarrow _{S}}}s'$ i $f(s')=z$. 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ą $T$-koalgebr $\mathbf {Set} _{T}$.

W zasadzie powyższa konstrukcja ma kilka możliwych wariacji w zależności od funktora $T$. Dla identyczności, $1_{\mathbf {Set} }$-koalgebry $(S,\alpha )$ odpowiadają deterministycznym systemom dynamicznym z dynamiką $s\to z\iff \alpha (s)=z$. Dla funktora stałego $T\colon \mathbf {Set} \to \mathbf {Set}$, $TX:=\mathbf {1}$, $Tf:=1_{\mathbf {1} }$, można pokazać, że kategoria $\mathbf {Set} _{T}$ jest izomorficzna z $\mathbf {Set}$, co oznacza, że na każdym zbiorze można zadać strukturę (trywialnej) $T$-koalgebry. Innym przykładem są systemy dynamiczne z terminacją, które są koalgebrami funktora $T(-):=\mathbf {1} +(-)$. 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 $A$ będzie dowolnym zbiorem. Dla funktora $T(-):=A\times (-)$, $T$-koalgebrą jest każda para $(Q,(o\colon Q\to A,t\colon Q\to Q)$. Gdy $Q$ interpretujemy jako zbiór stanów, $A$ jako zbiór stanów końcowych, funkcję $o\colon Q\to A$ jako wyjście, $t\colon Q\to Q$ jako funkcję przejścia, to ta koalgebra jest automatem deterministycznym. Homomorfizm dwóch automatów $f\colon (P,o_{p},t_{P})\to (Q,o_{Q},t_{Q})$ to funkcja $P\to Q$, która spełnia równania $o_{P}(p)=o_{Q}(f(p))$, $f(t_{P}(p))=t_{Q}(f(p))$, 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 $f$ dwóch koalgebr, musimy pokazać w jaki sposób destruktory koalgebry $o,t$ zachowują się na wartościach $f$ (dla algebr musieliśmy w takim wypadku wskazać, jakie wartości $f$ przyjmował na konstruktorach algebry).

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

$A^{\omega }:=\{\sigma \mid \sigma \colon \mathbb {N} \to A\},$

$\sigma :=(\sigma (0),\sigma (1),\sigma (2),...),$

$\sigma ':=(\sigma (1),\sigma (2),\sigma (3),...),$ to dla $o\colon A^{\omega }\to A$, $o(\sigma ):=\sigma (0)$ oraz $t\colon A^{\omega }\to A^{\omega }$, $t(\sigma )=\sigma '$ dostaniemy koalgebrę $(A^{\omega },(o,t))$. (W interpretacji $A^{\omega }$ jako listy nieskończonej, funkcja $o$ bywa też nazywana ${\mathtt {head}}$, zaś funkcja $t$ - ${\mathtt {tail}}$.) Zanim pokażemy, że ta koalgebra jest końcowa, wprowadźmy pewną metodę dowodzenia zwaną koindukcją.

Dowodzenie przez koindukcję

Definicja 15.11 [bisymulacja]

Niech $(A,\alpha \colon A\to TA)$ i $(B,\beta \colon B\to TB)$ będą dwiema $T$-koalgebrami. Podzbiór $R\subseteq A\times B$ nazywamy bisymulacją między $A$ i $B$, jeśli na $R$ da się zadać strukturę $T$-koalgebry $(R,\gamma \colon R\to TR)$ w taki sposób, aby projekcje $\pi _{1}\colon R\to A$, $\pi _{2}\colon R\to B$ były homomorfizmami, tzn. tak, aby poniższy diagram komutował:

Jeśli $(A,\alpha )=(B,\beta )$, to $R$ nz. bisymulacją na $A$.

O bisymulacji na początek wystarczy wiedzieć tyle, że: (a) przekątna $\Delta _{A}\subseteq A\times A$ jest bisymulacją na $(A,\alpha )$; (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 $T$. W końcu można pokazać, że rodzina wszystkich bisymulacji tego samego typu tworzy kratę zupełną, której elementem największym jest bisymulacja $\sim$ będąca relacją równoważności: $s\sim t$ wtedy i tylko wtedy, gdy istnieje bisymulacja $R$ taka, że $(s,t)\in R$.

Zadanie 15.5 opisuje bisymulacje dla funktora $T$ 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 $A^{\omega }$ jest relacja $R\subseteq A^{\omega }\times A^{\omega }$ taka, że dla dowolnych $\sigma ,\tau \in A^{\omega }$, jeśli $(\sigma ,\tau )\in A^{\omega }$, to:

• $(\sigma (0),\tau (0))\in R$ oraz
• $(\sigma ',\tau ')\in R$.

Jeśli istnieje bisymulacja $R$ taka, że $\sigma R\tau$, to piszemy $\sigma \sim \tau$ i mówimy, iż $\sigma ,\tau$ są bipodobne (ang. bisimilar). Bipodobieństwo $\sim$ jest oczywiście największą z bisymulacji na $A^{\omega }$.

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

Twierdzenie 15.13 [metoda koindukcji dla nieskończonych list]

Dla dowolnych $\sigma ,\tau \in A^{\omega }$: $\sigma \sim \tau \ \Rightarrow \ \sigma =\tau .$

Dowód

Niech $R$ będzie bisymulacją taką, że $\sigma R\tau$ (taka istnieje, bo z założenia $\sigma \sim \tau$). Prosty dowód używający szkolnej indukcji na liczbach naturalnych pozwoli nam zobaczyć, że $(\sigma ^{(}n),\tau ^{(}n))\in R$, gdzie indeks $n$ odnosi się do $n$-tej pochodnej $\sigma$, tj.: $\sigma ^{(n)}:=(\sigma (n),\sigma (n+1),\sigma (n+2),...).$

Znów ponieważ $R$ jest bisymulacją, $(\sigma ^{(}n)(0),\tau ^{(}n)(0))\in R$, czyli po prostu $(\sigma (n),\tau (n))\in R$ dla dowolnego $n\in \omega$. To znaczy, że $\sigma =\tau$.

Uwaga

Dla dowolnej innej końcowej $T$-koalgebry $(S,\alpha )$ twierdzenie powyższe uogólnia się do następującej postaci: dla każdej bisymulacji $R$ na $S$, $R\subseteq \Delta _{S}$. Twierdzenie to wygląda niepozornie, nieprawdaż?

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

Stwierdzenie 15.14

$(A^{\omega },(o,t))$ jest koalgebrą końcową funktora $A\times (-)$.

Dowód

Pokażemy, że dla dowolnego innego automatu $(Q,(o_{Q},t_{Q}))$ istnieje dokładnie jeden homomorfizm $f\colon (Q,(o_{Q},t_{Q}))\to (A^{\omega },(o,t))$ taki, że poniższy diagram komutuje:

Połóżmy dla dowolnego $q\in Q$:

$f(q):=(oq,otq,ottq,otttq,...).$

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

$R:=\{(f(q),g(q))\mid q\in Q\}$

jest bisymulacją na $A^{\omega }$. Oto dowód: niech $(f(q),g(q))\in R$. Ponieważ $f$ i $g$ są homomorfizmami, $o(f(q))=o_{Q}(q)=o(g(q))$ oraz $t(f(q))=f(t_{Q}(q))$ i $t(g(q))=g(t_{Q}(q))$. Ponieważ $(f(t_{Q}(q)),g(t_{Q}(q)))\in R$, dowiedliśmy, że $R$ jest bisymulacją. Z twierdzenia o koindukcji mamy $f=g$.

Końcowość koalgebry $(A^{\omega },(o,t))$ 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ą): $\sigma =\sigma '$ przy warunku $\sigma (0)=a$. Jest oczywiste, że rozwiązaniem musi być lista $\sigma =(a,a,a,...)$, ale formalnie postępujemy tak: rozważamy automat $(Q=\{q\},o_{Q}(q):=a,t_{Q}(q)=q)$. Niech $l\colon Q\to A^{\omega }$ będzie jedynym homomorfizmem w $A^{\omega }$. Dla $\sigma :=l(q)$ otrzymujemy $\sigma '=t\sigma =tl(q)=lt_{Q}(q)=l(q)-\sigma$ oraz $\sigma (0)=o(\sigma )=o(l(q))=o_{Q}(q)=a$. A zatem rozwiązanie szukanego równania istnieje. Jest jedyne, bo jeśli $\tau$ jest innym rozwiązaniem, to $\{(\sigma ,\tau )\}$ jest bisymulacją na $A^{\omega }$, skąd dostajemy: $\sigma =\tau$ 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:

${\mathtt {par}}(\sigma ):=(\sigma (0),\sigma (2),\sigma (4),...),$ ${\mathtt {npar}}(\sigma ):=(\sigma (1),\sigma (3),\sigma (5),...).$

Po pierwsze, istnieje operacja ${\mathtt {zip}}\colon A^{\omega }\times A^{\omega }\to A^{\omega }$, która spełnia:

${\mathtt {zip}}(\sigma ,\tau )(2n):=\sigma (n)$

oraz

${\mathtt {zip}}(\sigma ,\tau )(2n+1):=\tau (n).$

Istnienie udowadniamy tak samo jak w poprzednim przykładzie, zaczynając od równania ${\mathtt {zip}}(\sigma ,\tau )'={\mathtt {zip}}(\tau ,\sigma ')$ przy warunku ${\mathtt {zip}}(\sigma ,\tau )(0)=\sigma (0)$. (Dokładniej mówiąc, ${\mathtt {zip}}:=l((\sigma ,\tau ))$ dla jedynego homomorfizmu $l\colon Q\to A^{\omega }$, gdzie $Q:=A^{\omega }\times A^{\omega }$, $o_{Q}((\sigma ,\tau )):=\sigma (0)$, $t_{Q}((\sigma ,\tau )):=(\tau ,\sigma ')$.)

Pokażemy przez koindukcję, że:

${\mathtt {par}}({\mathtt {zip}}(\sigma ,\tau ))=\sigma .$

Zdefiniujmy relację:

$R:=\{({\mathtt {par}}({\mathtt {zip}}(\sigma ,\tau )),\sigma )\mid \sigma ,\tau \in A^{\omega }\}.$

Zauważmy, że

${\mathtt {par}}({\mathtt {zip}}(\sigma ,\tau ))(0)={\mathtt {zip}}(\sigma ,\tau )(0)=\sigma (0),$

a także

${\begin{aligned}({\mathtt {par}}({\mathtt {zip}}(\sigma ,\tau ))',\sigma ')&=&({\mathtt {par}}({\mathtt {zip}}(\sigma ,\tau )''),\sigma ')\\&=&({\mathtt {par}}({\mathtt {zip}}(\tau ,\sigma ')'),\sigma ')\\&=&({\mathtt {par}}({\mathtt {zip}}(\sigma ',\tau ')),\sigma ')\in R.\end{aligned}}$

To dowodzi, że $R$ 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!