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

{{kotwica|wyklad14|} 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  ?.

Twierdzenie

W $\mathbf {Dcpo}$ istnieją granice dowolnych diagramów.

Uwaga

{{{3}}}

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\to 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||mod14:thm:limitcolimit| 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

{{{3}}}

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  ?. 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ć, $\mathrm {\bf {Dcpo}} _{\bot }^{EP}$ jest kategorią.

Definicja [Omega-kategoria]

Nazwijmy {\bf

$\omega$-kategorią} każdą kategorię, w której diagram

postaci Plik:Tk 14 3.png posiada granicę odwrotną.

Zauważmy, że twierdzenie o zgodności granicy prostej i odwrotnej - Twierdzenie ? - mówi, że Parser nie mógł rozpoznać (Błąd konwersji. Serwer („https://wazniak.mimuw.edu.pl/api/rest_”) zgłosił: „Cannot get mml. TeX parse error: Double exponent: use braces to clarify”): {\displaystyle \mathrm {'} ''Dcpo'''_{\bot }^{EP}} jest $\omega$-kategorią!

Definicja

Funktor $F$ między

$\omega$-kategoriami nazywamy ciągłym, jeśli zachowuje granice odwrotne, t.j. jeśli $D_{\infty }$ jest kogranicą powyższego diagramu, to $F(D_{\infty })$ jest kogranicą diagramu

Plik:Tk 14 4.png

Uwaga

{{{3}}}

Lemat

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ść {\it mocniejsza}, która jest łatwiej weryfikowalna: lokalna ciągłość.

Definicja

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 [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 Parser nie mógł rozpoznać (Błąd konwersji. Serwer („https://wazniak.mimuw.edu.pl/api/rest_”) zgłosił: „Cannot get mml. TeX parse error: Double exponent: use braces to clarify”): {\displaystyle {\widehat {F}}\colon \mathrm {'} ''Dcpo'''_{\bot }^{EP}\times \mathrm {'} ''Dcpo'''_{\bot }^{EP}\to \mathrm {\bf {Dcpo}} _{\bot }^{EP}} , którego działanie na obiekty jest takie

samo, jak funktora $F$.

Dowód

{{{3}}}

Twierdzenie Scotta

Zgodnie z poprzednim twierdzeniem możemy zdefiniować Eksponent Parser nie mógł rozpoznać (Błąd konwersji. Serwer („https://wazniak.mimuw.edu.pl/api/rest_”) zgłosił: „Cannot get mml. TeX parse error: Double exponent: use braces to clarify”): {\displaystyle Exp\colon \mathrm {\bf {Dcpo}} _{\bot }^{EP}\times \mathrm {'} ''Dcpo'''_{\bot }^{EP}\to \mathrm {'} ''Dcpo'''_{\bot }^{EP}} jako ${\widehat {[-,-]}}$, który jest ciągły (ponieważ eksponent $[-,-]$ jest lokalnie ciągły). Rozważmy złożenie

Parser nie mógł rozpoznać (Błąd konwersji. Serwer („https://wazniak.mimuw.edu.pl/api/rest_”) zgłosił: „Cannot get mml. TeX parse error: Double exponent: use braces to clarify”): {\displaystyle \mathrm {'} ''Dcpo'''_{\bot }^{EP}{\stackrel {\Delta }{\rightarrow }}\mathrm {\bf {Dcpo}} _{\bot }^{EP}\times \mathrm {'} ''Dcpo'''_{\bot }^{EP}{\stackrel {Exp}{\rightarrow }}\mathrm {'} ''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: \begin{eqnarray*} F(e,p) & = & Exp((e,p),(e,p))\\

      & = & ([-,-](p,e), [-,-](e,p))\\
      & = & ([p,e], [e,p]).

\end{eqnarray*} 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$ \begin{eqnarray*} [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),

\end{eqnarray*} 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 [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 }].$