Teoria kategorii dla informatyków/Wykład 14: Teoria dziedzin III

From Studia Informatyczne

Z poprzedniego wykładu wiemy, że \mathbf{Dcpo} - kategoria wszystkich dcpo wraz z funkcjami ciągłymi w sensie Scotta - patrz Wykład 12. - jest kartezjańsko zamknięta. Kategoria ta jest również zupełna. Dowód poniższego twierdzenia znajdziemy w rozwiązaniu Zadania 14.1.


Twierdzenie 14.1

W \mathbf{Dcpo} istnieją granice dowolnych diagramów.
Uwaga
Powyższe twierdzenie nie zachodzi dla klas dziedzin ciągłych i algebraicznych w ogólności. Aby granica była również posetem odpowiedniej klasy, musimy nałożyć pewne restrykcje zarówno na kształt diagramów, jak i na własności funkcji tworzących diagram.


Spis treści

Twierdzenie o zgodności granicy prostej i odwrotnej

Przedstawimy teraz twierdzenie o zgodności granicy prostej i odwrotnej pewnych szczególnych diagramów w kategorii \mathbf{Dcpo}. Wynik ten jest znany w literaturze angielskojęzycznej jako limit-colimt coincidence i jest jednym z kamieni milowych w teorii dziedzin. Twierdzenie to wykorzystuje się przede wszystkim przy rozwiązywaniu tak zwanych rekursywnych równań dziedzinowych (ang. recursive domain equations).

Grafika:ilustracja2.png

Przykładem takiego równania jest D\cong [D,D]. Okazuje się, że jego nietrywialne rozwiązania istnieją! Tak więc istnieją posety więcej niż jednoelementowe, które są izomorficzne z przestrzenią swoich ciągłych endofunkcji! Wynik jest o tyle zaskakujący, że w \mathbf{Set} taka sytuacja, zgodnie z twierdzeniem Cantora nie może mieć miejsca.


Twierdzenie 14.2

Rozważmy diagram F w kategorii \mathbf{Dcpo} taki, że:
  • Wierzchołkami F są posety D_0, D_1, D_2, ...
  • Dla n\leq m istnieją funkcje e_{mn}\colon D_n\to D_m, i p_{nm}\colon D_m\to D_n tworzące parę e-p.
  • Dla każdego n\in \omega mamy e_{nn} = 1_{D_n}.
  • Dla n\leq m\leq k mamy e_{kn} = e_{km}\circ e_{mn} oraz

p_{nk} = p_{nm}\circ p_{mk}.

Zdefiniujmy:

D = \{ (x_0, x_1, ...)\mid (\forall n\leq m)(x_n=p_{nm}(x_m)) \},
p_m\colon D\to D_m, \qquad (x_0, x_1, ...)\mapsto x_m, \ m\in \omega,
e_m\colon D_m\to D, \ x\mapsto (\bigvee{}^\downarrow_{k\geq n,m} p_{nk}\circ e_{km}(x)\mid n\in \omega).

Wtedy:

  • Para (e_m, p_m) jest parą e-p i zachodzi \bigvee{}^\downarrow_{n\in \omega} e_n\circ p_n = 1_{D}.
  • \{p_n\colon D\to D_n\} jest granicą diagramu F. Jeśli \{g_n\colon C\to D_n\} jest dowolną inną granicą, to izmorfizm h\colon C\to D jest dany jako h(x) = (g_n(x)\mid n\in \omega) lub h = \bigvee{}^\downarrow_n e_n\circ g_n.
  • \{e_n\colon D_n\to D\} jest granicą odwrotną diagramu F. Jeśli \{f_n\colon E\to D_n\} jest dowolną inną granicą, to izmorfizm f\colon D\to E jest dany jako f(x_n\mid n\in \omega) = \bigvee{}^\downarrow_n f_n(x_n) lub f = \bigvee{}^\downarrow_n f_n\circ p_n.

Dowód

W dowodzie Twierdzenia 14.1 podanym w Zadaniu 14.1

pokazaliśmy już, że granicą diagramu jest \{p_n\colon D\to D_n\} i że izomorfizm h\colon C\to D ma (pierwszą z) postulowanych postaci.

Pokażmy teraz, że funkcje e_m są dobrze zdefiniowane, tj. że y = e_m(x) należy do D dla dowolnego m\in \omega. Niech m będzie dowolne i załóżmy, że n\leq n'. Mamy:

\aligned p_{nn'}(y_{n'})  & = & p_{nn'}(\bigvee{}^\downarrow_{k\geq n',m} p_{n'k}\circ  e_{km}(x))\\ & = & \bigvee{}^\downarrow_{k\geq  n',m} p_{nn'}\circ p_{n'k}\circ e_{km}(x)\\ & = & \bigvee{}^\downarrow_{k\geq n',m} p_{nk}\circ e_{km}(x)=y_n. \endaligned

W dowodzie korzystaliśmy kolejno z: definicji y_{n'}, ciągłości p_{nn'} i definicji y_n. A zatem y = (y_0, y_1, ...)\in D. Co więcej, funkcje e_m są ciągłe, gdyż tylko funkcje ciągłe zostały użyte w ich definicji.

Przejdźmy do dowodu (5). Niech m\in \omega. Mamy:


\aligned e_m\circ p_m (x_n\mid n\in \omega) &=& e_m(x_m)= (\bigvee{}^\downarrow_{k\geq n,m} p_{nk}\circ e_{km} (x_m)\mid  n\in\omega)\\ &=& (\bigvee{}^\downarrow_{k\geq n,m} p_{nk}\circ e_{km} \circ p_{mk} (x_k)\mid n\in\omega)\sqsubseteq (\bigvee{}^\downarrow_{k\geq n,m} p_{nk} (x_k)\mid n\in\omega)\\ &=& (\bigvee{}^\downarrow_{k\geq n} p_{nk} (x_k)\mid n\in\omega)=(x_n\mid n\in\omega). \endaligned

Ponadto:

\aligned p_m\circ e_m (x) &=& p_m (\bigvee{}^\downarrow_{k\geq  n,m} p_{nk}\circ e_{km}(x)\mid n\in\omega )\\ &=& \bigvee{}^\downarrow_{k\geq m} p_{mk}\circ e_{km}(x)\\ &=&  x.\endaligned


Bliższa analiza pokazuje, że e_m\circ p_m pozostawi niezmienione te elementy ciągu (x_n\mid n\in\omega), gdzie n\leq m.

\aligned p_n(e_m\circ p_m (x_n\mid n\in \omega))&=& ...\\ &=& p_n(\bigvee{}^\downarrow_{k\geq n,m} p_{nk}\circ e_{km} \circ p_{mk} (x_k)\mid n\in\omega)\\ &=& p_n(\bigvee{}^\downarrow_{k\geq n,m} p_{nm}\circ p_{mk} \circ e_{km} \circ p_{mk} (x_k)\mid n\in\omega)\\ &=& p_n(\bigvee{}^\downarrow_{k\geq n,m} p_{nm}\circ  p_{mk} (x_k)\mid n\in\omega)\\ &=& p_n(\bigvee{}^\downarrow_{k\geq n} p_{nk} (x_k)\mid n\in\omega)\\ &=& p_n(\bigvee{}^\downarrow_{k\geq n} x_n\mid n\in\omega)\\ &=& p_n(x_n\mid n\in\omega)\\ & = & x_n.\endaligned


To dowodzi, że \bigvee{}^\downarrow_n e_n\circ p_n = 1_{D}, czyli (5).

Korzystając z powyższego, mamy też natychmiast:

h = 1_D\circ h = \bigvee{}^\downarrow_n E_n\circ p_n\circ h = \bigvee{}^\downarrow e_m \circ g_n,

co kończy dowód (6).

Do pokazania pozostała nam (7), czyli fakt, że \{e_n\colon D_n\to D\} jest granicą odwrotną diagramu F. Jeśli \{f_n\colon E\to D_n\} jest dowolną inną granicą, to sprawdźmy najpierw, czy funkcja f = \bigvee{}^\downarrow_n f_n\circ p_n jest dobrze zdefiniowana, tj., czy supremum jest nad zbiorem skierowanym. Ale tak jest, ponieważ dla n\leq m:

f_n \circ p_n = f_m \circ e_{mn}\circ p_{nm}\circ p_m\sqsubseteq f_m\circ p_m.

Co więcej:

f\circ e_m=\bigvee{}^\downarrow_{n\leq m} f_n\circ p_n\circ e_m= \bigvee{}^\downarrow_{n\leq m} f_n\circ p_n\circ e_n\circ e_{nm}=\bigvee{}^\downarrow_{n\leq m} f_n\circ e_{nm}=\bigvee{}^\downarrow_{n\leq m} f_m=f_m.

W końcu, pokażemy, że funkcja f o podanych własnościach jest tylko jedna. Jeśli dla f'\colon D\to E zachodzi f'\circ e_m = f_m, to f'\circ e_m \circ p_m = f_m\circ p_m, a zatem:

\bigvee{}^\downarrow_m f'\circ e_m \circ p_m =  \bigvee{}^\downarrow_m f_m\circ p_m,

czyli z ciągłości f':

f'(\bigvee{}^\downarrow_m \circ e_m \circ p_m) = \bigvee{}^\downarrow_m f_m\circ p_m.
Ale \bigvee{}^\downarrow_m \circ e_m \circ p_m = 1_D oraz \bigvee{}^\downarrow_m f_m\circ p_m = f, co daje f'\circ 1_D = f, czyli f'=f. image:End_of_proof.gif

Kategoria dcpo i par e-p

W tej kategorii obiektami są dcpo posiadające element najmniejszy, zaś morfizmami są pary e-p, o których była mowa podczas Wykładu 2. Złożenie morfizmów

Grafika:tk-14.1.png

definiujemy w naturalny sposób jako morfizm

Grafika:tk-14.2.png

Czy (e_2\circ e_1, p_1\circ p_2) jest parą e-p? Tak, ponieważ:

e_2\circ e_1\circ p_1\circ p_2 \sqsubseteq e_2\circ 1_E\circ p_2 = e_2\circ p_2\sqsubseteq 1_F

oraz

p_1\circ p_2\circ e_2\circ e_1 = p_1\circ 1_E\circ e_1 = p_1\circ e_1 = 1_D.

A zatem złożenie par e-p jest dobrze zdefiniowane, a co za tym idzie, i co łatwo już teraz pokazać, \mathbf{Dcpo}^{EP}_{\bot} jest kategorią.


Definicja 14.3 [Omega-kategoria]

Nazwijmy \omega-kategorią każdą kategorię, w której diagram postaci:
Grafika:tk-14.3.png
posiada granicę odwrotną.
Zauważmy, że twierdzenie o zgodności granicy prostej i odwrotnej - Twierdzenie 14.2 - mówi, że \mathvf{Dcpo}^{EP}_{\bot} jest \omega-kategorią!


Definicja 14.4 [Funktor ciągły]

Funktor F między \omega-kategoriami nazywamy ciągłym, jeśli zachowuje granice odwrotne, tj.: jeśli D_{\infty} jest kogranicą powyższego diagramu, to F(D_{\infty}) jest kogranicą diagramu:
Grafika:tk-14.4.png
Uwaga
Tak naprawdę, aby być w zgodzie z definicją funktora ciągłego podaną przed Zadaniem Zadaniem 3.3, powinniśmy powyższą własność nazwać nie: ciągłością, ale ciągłością dualną, a funktor - funktorem dualnie ciągłym. Dla potrzeb tego wykładu przyjmijmy jednak powyższą nomenklaturę.


Lemat 14.5

Niech \mathbf{A} będzie \omega-kategorią, F\colon \mathbf{A}\to \mathbf{A} funktorem ciągłym, f\colon A\to F(A) morfizmem w \mathbf{A} oraz niech diagram:
Grafika:tk-14.7.png
posiada granicę odwrotną D_{\infty}. Wówczas D_{\infty}\cong F(D_{\infty}).


Zauważmy, że przekątna \Delta\colon \mathbf{Dcpo}\to \mathbf{Dcpo}\times \mathbf{Dcpo}, a\mapsto (a,a), f\mapsto (f,f) dla a\in  \mathbf{Dcpo}_0, f\in \mathbf{Dcpo}_1 jest ciągłym funktorem.

Lokalna ciągłość funktorów

Ciągłość funktora jest często niełatwa do sprawdzenia. Na szczęście istnieje własność mocniejsza, która jest łatwiej weryfikowalna: lokalna ciągłość.


Definicja 14.6

Funktor F\colon \mathbf{D}\to \mathbf{E} pomiędzy kategoriami posetów \mathbf{D}, \mathbf{E} jest lokalnie ciągły jeśli przekształcenia f\mapsto F(f) typu \mathrm{Hom}(D,D')\to \mathrm{Hom}(F(D),F(D')) są ciągłe w sensie Scotta dla każdej pary obiektów D,D'\in \mathbf{D}_0.


Dla przykładu przeczytajmy tę definicję dla bifunktora F\colon \mathbf{Dcpo}^{op}\times \mathbf{Dcpo}\to  \mathbf{Dcpo}: funktor F jest lokalnie ciągły, jeśli dla dowolnych zbiorów skierowanych A\subseteq^{\uparrow} [D_2, D_1] i B\subseteq^{\uparrow} [D_3, D_4], gdzie D_1, ..., D_4\in \mathbf{Dcpo}_0, mamy:

F(\bigvee{}^\downarrow A, \bigvee{}^\downarrow B) = \bigvee{}^\downarrow_{f\in A, g\in G} F(f,g).

Zauważmy, że supremum po prawej stronie istnieje w [F(D_1,D_3), F(D_2, D_4)].

Dla przykładu, eksponent [-,-]\colon\mathbf{Dcpo}^{op}\times \mathbf{Dcpo}\to  \mathbf{Dcpo} jest lokalnie ciągły, ponieważ [f\to g] = curry(g\circ ev\circ (1\times f)) jest złożeniem funkcji ciągłych w sensie Scotta.


Lemat 14.7 [istnienie funktorów ciągłych]

Niech funktor F\colon \mathbf{Dcpo}^{op}_{\bot}\times \mathbf{Dcpo}_{\bot}\to \mathbf{Dcpo}_{\bot} będzie lokalnie ciągły. Wtedy istnieje ciągły funktor \widehat{F}\colon \mathbf{Dcpo}^{EP}_{\bot}\times \mathbf{Dcpo}^{EP}_{\bot}\to \mathbf{Dcpo}^{EP}_{\bot}, którego działanie na obiekty jest takie samo, jak funktora F.


Dowód

Połóżmy \widehat{F}(A,B) = F(A,B), gdzie A,B są dcpo z elementami najmniejszymi. Rozważmy pary e-p:
Grafika:tk-14.5.png

Możemy wówczas stworzyć diagram:

Grafika:tk-14.6.png

i para morfizmów powyżej jest parą e-p. Rzeczywiście:

F(e,s)\circ F(p,j) = F(p\circ e, s\circ j) = F(1_A, 1_B) =1_{F(A,B))}.

Wykorzystaliśmy kolejno: kontrawariantność F dla pierwszego argumentu, własności par e-p i definicję funktora. Ponadto:

F(p,j)\circ F(e,s)  = F(e\circ p, j\circ s) \sqsubseteq F(1_{A'}, 1_{B'}) = 1_{F(A',B')}.

Wykorzystaliśmy kolejno: definicję funktora, monotoniczność F, która wynika z lokalnej ciągłości i w końcu definicję F jeszcze raz.

Zdefiniujmy zatem:

\widehat{F}((e,p),(j,s)) = (F(p,j),F(e,s)).

Oczywiście, \widehat{F} jest funktorem. Aby pokazać ciągłość, załóżmy, że mamy w \mathbf{Dcpo}^{EP}_{\bot}\times \mathbf{Dcpo}^{EP}_{\bot} diagram:

(A_1,B_1)\to  (A_2,B_2)\to (A_3,B_3)\to...,

który ma granicę odwrotną (D,E). A to znaczy, że w \mathbf{Dcpo} mamy dwa diagramy:

A_1\to A_2\to A_3\to...

i

B_1\to B_2\to B_3\to...,

których granicami są odpowiednio D i E. Z twierdzenia o koincydencji granicy prostej i odwrotnej (Twierdzenie 14.2) wiemy, że zachodzi 1_D = \bigvee{}^\downarrow_n e_n\circ p_n oraz 1_E = \bigvee{}^\downarrow_n j_n\circ s_n, a więc 1_{(D,E)} = \bigvee{}^\downarrow (e_n\circ p_n, j_n\circ s_n). Aplikując lokalną ciągłość F do ostatniej równości, mamy:

1_{\widehat{F}(D,E)} & = & \widehat{F}(1_{(D,e)})=(F(1_D,1_E),F(1_D,1_E))= \bigvee{}^\downarrow (F(e_n\circ p_n, j_n\circ s_n),F(e_n\circ p_n, j_n\circ s_n)).

Ale Twierdzenie 14.2 mówi, że ostatnia równość charakteryzuje granicę odwrotną diagramu w \mathbf{Dcpo}^{EP}_{\bot}

\widehat{F}(A_1,B_1)\to \widehat{F}(A_2,B_2)\to \widehat{F}(A_3,B_3)\to ...
a zatem \widehat{F}(D,E)=F(D,E) jest tą szukaną granicą odwrotną, co należało pokazać. image:End_of_proof.gif


Dana S. Scott ur. 1932Zobacz biografię
Enlarge
Dana S. Scott ur. 1932
Zobacz biografię

Twierdzenie Scotta

Zgodnie z poprzednim twierdzeniem możemy zdefiniować Eksponent Exp\colon \mathbf{Dcpo}^{EP}_{\bot}\times \mathbf{Dcpo}^{EP}_{\bot} \to \mathbf{Dcpo}^{EP}_{\bot} jako \widehat{[-,-]}, który jest ciągły (ponieważ eksponent [-,-] jest lokalnie ciągły). Rozważmy złożenie \mathbf{Dcpo}^{EP}_{\bot}  \stackrel{\Delta}{\rightarrow} \mathbf{Dcpo}^{EP}_{\bot}\times\mathbf{Dcpo}^{EP}_{\bot} \stackrel{Exp}{\rightarrow} \mathbf{Dcpo}^{EP}_{\bot} . Definiuje ono funktor ciągły F (jako złożenie dwóch funktorów ciągłych). Jak on działa? Rozważmy parę:

Grafika:tk-14.8.png

Mamy F(P) = Exp\circ \Delta(P) = Exp(P,P) = [-,-](P,P) =[P,P]. Podobnie F(Q) = [Q,Q]. Działanie na morfizmach:

F(e,p) = Exp((e,p),(e,p))= ([-,-](p,e), [-,-](e,p)) = ([p,e], [e,p]).

A zatem otrzymujemy:

Grafika:tk-14.9.png

Wiemy już, że para funkcji powyżej tworzy parę e-p! Przypomnijmy jeszcze raz, jak działają funkcje [p,e] i [e,p] na elementy z odpowiednio [P,P] i [Q,Q]. Przykładowo, dla f\in [P,P] mamy dla q\in Q:

[p\to e](f)(q) = curry(e\circ ev\circ (1\times p))(f)(q) = (e\circ ev\circ (1\times p))(f,q)= e(ev((f,p(q)))) = e(f(p(q))) = e\circ f\circ p (q),

to znaczy [p,e](f) = e\circ f\circ p. Podobnie [e,p](g) = p\circ g\circ e dla g\in [Q,Q].

Zauważmy w końcu, że dla dowolnego dcpo P, jeśli jako e\colon P\to F(P) weźmiemy funkcję y\mapsto \lambda x.y, zaś jako p\colon F(P)\to P weźmiemy funkcję f\mapsto f(\bot), to para (e,p) jest parą e-p typu P\to F(P).

A zatem otrzymujemy końcowy wniosek:

Twierdzenie 14.8 [Scott]

Niech P będzie dcpo z elementem najmniejszym \bot. Zdefiniujmy diagram w \mathbf{Dcpo}, jak następuje:
Grafika:tk-14.10.png

gdzie:

  • D_0 = P, D_{n+1} = [D_n,D_n],
  • e_0\colon P\to [P,P] jest funkcją \lambda y .\lambda x .y.

p_0\colon [P,P]\to P jest funkcją \lambda f.f(\bot).

  • e_{n+1}\colon [D_n,D_n] = D_{n+1} \to [D_{n+1},D_{n+1}] jest funkcją \lambda f.e_n\circ f\circ p_n. p_{n+1}\colon [D_{n+1},D_{n+1}]\to [D_n,D_n] jest funkcją \lambda g.p_n \circ g\circ e_n.

Niech D_{\infty} będzie granicą diagramu:

Grafika:tk-14.11.png

w \mathbf{Dcpo}. Wówczas:

D_{\infty}\cong [D_{\infty},D_{\infty}].