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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania

{{kotwica|wyklad14|} Z poprzedniego wykładu wiemy, że - 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 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 . 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 . 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 taka sytuacja, zgodnie z twierdzeniem Cantora nie może mieć miejsca.


{{twierdzenie||mod14:thm:limitcolimit| Rozważmy diagram w kategorii taki, że

  • Wierzchołkami są posety .
  • Dla istnieją funkcje ,
     i   tworzące parę e-p.
  • Dla każdego mamy .
  • Dla mamy oraz

.

Zdefiniujmy

Wtedy:

  • Para jest parą e-p i zachodzi .
  • jest granicą diagramu . Jeśli jest dowolną inną granicą, to izmorfizm jest dany jako lub .
  • jest granicą odwrotną diagramu . Jeśli jest dowolną inną granicą, to izmorfizm jest dany jako lub .

Dowód

W dowodzie Twierdzenia ? podanym w Zadaniu  ?

pokazaliśmy już, że granicą diagramu jest i że izomorfizm ma (pierwszą z) postulowanych postaci.

Pokażmy teraz, że funkcje są dobrze zdefiniowane, tj. że należy do dla dowolnego . Niech będzie dowolne i załóżmy, że . Mamy:

Parser nie mógł rozpoznać (błąd składni): {\displaystyle 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. }

W dowodzie korzystaliśmy kolejno z: definicji , ciągłości i definicji . A zatem . Co więcej, funkcje są ciągłe, gdyż tylko funkcje ciągłe zostały użyte w ich definicji.

Przejdźmy do dowodu (5). Niech . Mamy:


Ponadto,


Bliższa analiza pokazuje, że pozostawi niezmienione te elementy ciągu , gdzie .

Parser nie mógł rozpoznać (błąd składni): {\displaystyle 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. }

To dowodzi, że , czyli (5).

Korzystając z powyższego mamy też natychmiast

co kończy dowód (6).

Do pokazania pozostała nam (7), czyli fakt, że jest granicą odwrotną diagramu . Jeśli jest dowolną inną granicą, to sprawdźmy najpierw czy funkcja jest dobrze zdefiniowana, tj. czy supremum jest nad zbiorem skierowanym. Ale tak jest, ponieważ dla

Co więcej,

W końcu, pokażemy, że funkcja o podanych własnościach jest tylko jedna. Jeśli dla zachodzi , to , a zatem

czyli z ciągłości :

Ale oraz , co daje , czyli . 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

Plik:Tk 14 1.png

definiujemy w naturalny sposób jako morfizm

Plik:Tk 14 2.png

Czy jest parą e-p? Tak, ponieważ:

oraz

A zatem złożenie par e-p jest dobrze zdefiniowane, a co za tym idzie, i co łatwo już teraz pokazać, jest kategorią.

Definicja [Omega-kategoria]

Nazwijmy {\bf

-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 -kategorią!

Definicja

Funktor między

-kategoriami nazywamy ciągłym, jeśli zachowuje granice odwrotne, t.j. jeśli jest kogranicą powyższego diagramu, to jest kogranicą diagramu

Plik:Tk 14 4.png
Uwaga
Tak naprawdę, aby być w zgodzie z definicją funktora ciągłego podaną przed Zadaniem

 ?, 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

Niech będzie -kategorią, funktorem ciągłym, morfizmem w oraz niech diagram

Plik:Tk 14 7.png

posiada granicę odwrotną . Wówczas .


Zauważmy, że przekątna , , dla , 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 pomiędzy kategoriami posetów jest lokalnie ciągły jeśli przekształcenia

typu są ciągłe w sensie Scotta dla

każdej pary obiektów .

Dla przykładu przeczytajmy tę definicję dla bifunktora : funktor jest lokalnie ciągły, jeśli dla dowolnych zbiorów skierowanych i , gdzie , mamy

Zauważmy, że supremum po prawej stronie istnieje w .

Dla przykładu, eksponent jest lokalnie ciągły, ponieważ jest złożeniem funkcji ciągłych w sensie Scotta.


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

Niech

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

Dowód

{{{3}}} End of proof.gif


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 , 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 (jako złożenie dwóch funktorów ciągłych). Jak on działa? Rozważmy parę:

Plik:Tk 14 8.png

Mamy . Podobnie . 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

Plik:Tk 14 9.png

Wiemy już, że para funkcji powyżej tworzy parę e-p! Przypomnijmy jeszcze raz jak działają funkcje i na elementy z odpowiednio i : przykładowo, dla mamy dla \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 . Podobnie dla .

Zauważmy w końcu, że dla dowolnego dcpo , jeśli jako weźmiemy funkcję , zaś jako weźmiemy funkcję , to para jest parą e-p typu .

A zatem otrzymujemy końcowy wniosek:


Twierdzenie [Scott]

Niech będzie dcpo z elementem najmniejszym . Zdefiniujmy diagram w jak następuje:

Plik:Tk 14 10.png

gdzie

  • , ,
  • jest funkcją .

jest funkcją .

  • jest funkcją . jest funkcją .

Niech będzie granicą diagramu

Plik:Tk 14 11.png

w . Wówczas