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

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.

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

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 {}_{k\geq n,m}^{\downarrow }p_{nk}\circ e_{km}(x)\mid n\in \omega ).$

Wtedy:

• Para $(e_{m},p_{m})$ jest parą e-p i zachodzi $\bigvee {}_{n\in \omega }^{\downarrow }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 {}_{n}^{\downarrow }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 {}_{n}^{\downarrow }f_{n}(x_{n})$ lub $f=\bigvee {}_{n}^{\downarrow }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:

${\begin{aligned}p_{nn'}(y_{n'})&=&p_{nn'}(\bigvee {}_{k\geq n',m}^{\downarrow }p_{n'k}\circ e_{km}(x))\\&=&\bigvee {}_{k\geq n',m}^{\downarrow }p_{nn'}\circ p_{n'k}\circ e_{km}(x)\\&=&\bigvee {}_{k\geq n',m}^{\downarrow }p_{nk}\circ e_{km}(x)=y_{n}.\end{aligned}}$

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:

${\begin{aligned}e_{m}\circ p_{m}(x_{n}\mid n\in \omega )&=&e_{m}(x_{m})=(\bigvee {}_{k\geq n,m}^{\downarrow }p_{nk}\circ e_{km}(x_{m})\mid n\in \omega )\\&=&(\bigvee {}_{k\geq n,m}^{\downarrow }p_{nk}\circ e_{km}\circ p_{mk}(x_{k})\mid n\in \omega )\sqsubseteq (\bigvee {}_{k\geq n,m}^{\downarrow }p_{nk}(x_{k})\mid n\in \omega )\\&=&(\bigvee {}_{k\geq n}^{\downarrow }p_{nk}(x_{k})\mid n\in \omega )=(x_{n}\mid n\in \omega ).\end{aligned}}$

Ponadto:

${\begin{aligned}p_{m}\circ e_{m}(x)&=&p_{m}(\bigvee {}_{k\geq n,m}^{\downarrow }p_{nk}\circ e_{km}(x)\mid n\in \omega )\\&=&\bigvee {}_{k\geq m}^{\downarrow }p_{mk}\circ e_{km}(x)\\&=&x.\end{aligned}}$

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

${\begin{aligned}p_{n}(e_{m}\circ p_{m}(x_{n}\mid n\in \omega ))&=&...\\&=&p_{n}(\bigvee {}_{k\geq n,m}^{\downarrow }p_{nk}\circ e_{km}\circ p_{mk}(x_{k})\mid n\in \omega )\\&=&p_{n}(\bigvee {}_{k\geq n,m}^{\downarrow }p_{nm}\circ p_{mk}\circ e_{km}\circ p_{mk}(x_{k})\mid n\in \omega )\\&=&p_{n}(\bigvee {}_{k\geq n,m}^{\downarrow }p_{nm}\circ p_{mk}(x_{k})\mid n\in \omega )\\&=&p_{n}(\bigvee {}_{k\geq n}^{\downarrow }p_{nk}(x_{k})\mid n\in \omega )\\&=&p_{n}(\bigvee {}_{k\geq n}^{\downarrow }x_{n}\mid n\in \omega )\\&=&p_{n}(x_{n}\mid n\in \omega )\\&=&x_{n}.\end{aligned}}$

To dowodzi, że $\bigvee {}_{n}^{\downarrow }e_{n}\circ p_{n}=1_{D}$, czyli (5).

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

$h=1_{D}\circ h=\bigvee {}_{n}^{\downarrow }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 {}_{n}^{\downarrow }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 {}_{n\leq m}^{\downarrow }f_{n}\circ p_{n}\circ e_{m}=\bigvee {}_{n\leq m}^{\downarrow }f_{n}\circ p_{n}\circ e_{n}\circ e_{nm}=\bigvee {}_{n\leq m}^{\downarrow }f_{n}\circ e_{nm}=\bigvee {}_{n\leq m}^{\downarrow }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 {}_{m}^{\downarrow }f'\circ e_{m}\circ p_{m}=\bigvee {}_{m}^{\downarrow }f_{m}\circ p_{m},$

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

$f'(\bigvee {}_{m}^{\downarrow }\circ e_{m}\circ p_{m})=\bigvee {}_{m}^{\downarrow }f_{m}\circ p_{m}.$ Ale $\bigvee {}_{m}^{\downarrow }\circ e_{m}\circ p_{m}=1_{D}$ oraz $\bigvee {}_{m}^{\downarrow }f_{m}\circ p_{m}=f$, co daje $f'\circ 1_{D}=f$, czyli $f'=f$.

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

definiujemy w naturalny sposób jako morfizm

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} _{\bot }^{EP}$ jest kategorią.

Definicja 14.3 [Omega-kategoria]

Nazwijmy $\omega$-kategorią każdą kategorię, w której diagram postaci: posiada granicę odwrotną.

Zauważmy, że twierdzenie o zgodności granicy prostej i odwrotnej - Twierdzenie 14.2 - mówi, że $\mathbb {Dcpo} _{\bot }^{EP}$ 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:

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: 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 {}_{f\in A,g\in G}^{\downarrow }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} _{\bot }^{op}\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} _{\bot }^{EP}\times \mathbf {Dcpo} _{\bot }^{EP}\to \mathbf {Dcpo} _{\bot }^{EP}$, 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:

Możemy wówczas stworzyć diagram:

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} _{\bot }^{EP}\times \mathbf {Dcpo} _{\bot }^{EP}$ 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 {}_{n}^{\downarrow }e_{n}\circ p_{n}$ oraz $1_{E}=\bigvee {}_{n}^{\downarrow }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} _{\bot }^{EP}$

${\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ć.

Dana S. Scott ur. 1932
Zobacz biografię

Twierdzenie Scotta

Zgodnie z poprzednim twierdzeniem możemy zdefiniować Eksponent $Exp\colon \mathbf {Dcpo} _{\bot }^{EP}\times \mathbf {Dcpo} _{\bot }^{EP}\to \mathbf {Dcpo} _{\bot }^{EP}$ jako ${\widehat {[-,-]}}$, który jest ciągły (ponieważ eksponent $[-,-]$ jest lokalnie ciągły). Rozważmy złożenie $\mathbf {Dcpo} _{\bot }^{EP}{\stackrel {\Delta }{\rightarrow }}\mathbf {Dcpo} _{\bot }^{EP}\times \mathbf {Dcpo} _{\bot }^{EP}{\stackrel {Exp}{\rightarrow }}\mathbf {Dcpo} _{\bot }^{EP}.$ 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ę:

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:

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:

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:

w $\mathbf {Dcpo}$. Wówczas:

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