TKI Moduł 13: Różnice pomiędzy wersjami

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Pqw (dyskusja | edycje)
mNie podano opisu zmian
Pqw (dyskusja | edycje)
mNie podano opisu zmian
Linia 124: Linia 124:


posiada granicę odwrotną <math>D_{\infty}</math>. Wówczas <math>D_{\infty}\cong F(D_{\infty})</math>.
posiada granicę odwrotną <math>D_{\infty}</math>. Wówczas <math>D_{\infty}\cong F(D_{\infty})</math>.
Dowód: Skoro <math>D_{\infty}</math>  jest granicą odwrotną diagramu
???, to
[DIAGRAM]
komutuje. W szczególności
[DIAGRAM]
komutuje i jak łatwo zauważyć <math>D_{\infty}</math>  jest jego granicą. Ale
z ciągłości <math>F</math> mamy, że diagram
[DIAGRAM]
komutuje i <math>F(D_{\infty})</math> jest jego granicą. A zatem <math>D_{\infty}
\cong F(D_{\infty})</math> wynika z Lematu ???. QED.
'''Przykład'''. Przekątna <math>\Delta\colon \mathbf{Dcpo}\to \mathbf{Dcpo}\times \mathbf{Dcpo}</math>, <math>a\mapsto (a,a)</math>; <math>f\mapsto (f,f)</math>  dla <math>a\in \mathbf{Dcpo}_0</math>  <math>f\in \mathbf{Dcpo}_1</math> 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'''. Funktor <math>F\colon \mathcal{D}\to \mathcal{E}</math> pomiędzy kategoriami posetów <math>\mathcal{D}, \mathcal{E}</math>  jest {\em lokalnie ciągły} jeśli przekształcenia <math>f\mapsto F(f)</math>  typu <math>\mathrm{Hom}(D,D')\to \mathrm{Hom}(F(D),F(D'))</math>  są ciągłe w sensie Scotta dla każdej pary obiektów <math>D,D'\in \mathcal{D}_0</math>.
Dla przykładu przeczytajmy tę definicję dla bifunktora <math>F\colon \mathbf{Dcpo}^{op}\times \mathbf{Dcpo}\to \mathbf{Dcpo}</math>: funktor <math>F</math>  jest lokalnie ciągły, jeśli dla dowolnych zbiorów skierowanych <math>A\subseteq [D_2\to D_1]</math> i <math>B\subseteq [D_3\to D_4]</math>, gdzie <math>D_1, ..., D_4\in \mathbf{Dcpo}_0</math> mamy <math>F(\bigvee A, \bigvee B) = \bigvee_{f\in A, g\in G} F(f,g).</math> Zauważmy, że supremum po prawej stronie istnieje w <math>[F(D_1,D_3)\to F(D_2, D_4)]</math>. 
'''Przykład'''. Eksponent <math>[\_\to \_]\colon\mathbf{Dcpo}^{op}\times \mathbf{Dcpo}\to \mathbf{Dcpo}</math> jest lokalnie ciągły, ponieważ <math>[f\to g] = curry(g\circ ev\circ (1\times f))</math>  jest złożeniem funkcji ciągłych w sensie Scotta.
'''Lemat'''. Niech funktor <math>F\colon \mathbf{Dcpo}^{op}_{\bot}\times \mathbf{Dcpo}_{\bot}\to
\mathbf{Dcpo}_{\bot}</math>  będzie lokalnie ciągły. Wtedy istnieje ciągły funktor <math>\widehat{F}\colon Dcpo^{EP}_{\bot}\times Dcpo^{EP}_{\bot}\to Dcpo^{EP}_{\bot}</math> 
którego działanie na obiekty jest takie samo, jak funktora <math>F</math>. 
Dowód: Połóżmy <math>\widehat{F}(a,b) = F(a,b)</math>, gdzie <math>a,b</math> są posetami ciągłymi z elementami najmniejszymi. Rozważmy pary e-p:
[DIAGRAM]
Możemy wówczas stworzyć diagram
[DIAGRAM]
i para morfizmów powyżej jest parą e-p. Rzeczywiście: <math>F(e,s)\circ F(p,j) = F(p\circ e, s\circ j) = F(1_a, 1_b) = 1_{F(a,b))}.</math> Wykorzystaliśmy kolejno: kontrawariantność <math>F</math> dla pierwszego argumentu, własności par e-p i definicję funktora. Ponadto,
<math>F(p,j)\circ F(e,s)  = F(e\circ p, j\circ s) \sqsubseteq F(1_{a'}, 1_{b'}) = 1_{F(a',b')}.</math>
Wykorzystaliśmy kolejno: definicję funktora, monotoniczność <math>F</math>, która wynika z lokalnej ciągłości i w końcu definicję <math>F</math> jeszcze raz.

Wersja z 17:47, 20 cze 2006

Udowodnijmy teraz podstawowe twierdzenie na temat diagramów w kategorii Dcpo.

Twierdzenie. W Dcpo istnieją granice dowolnych diagramów.

Dowód: Dowód przeprowadzimy dla szczególnego diagramu:

[DIAGRAM]

(Dowód ogólny jest analogiczny lecz wymaga bardziej technicznego zapisu, wiec go pominiemy.) Pokażemy, że granica powyższego diagramu jest dana jako

D={(x0,x1,...)(nω)(fn(xn+1)=xn)}.

Zauważmy, że zbiór D jest posetem, w którym elementy są uporządkowane po współrzędnych (to znaczy, że porządek jest dziedziczony z produktu ΠnωDn. Jeśli GD jest zbiorem skierowanym, to dla każdego nωzbiór πn[G]={xnxG}jest skierowanym podzbiorem Dn. Niech yn={xnxG}. Z ciągłości funkcji tworzących diagram mamy: fn(yn+1)=fn({xn+1xG})={xnxG}=yn. To znaczy, że (y0,y1,...)D i, jak łatwo zauważyć, element ten jest supremum skierowanym zbioru G. Pokazaliśmy więc, że D Dcpo.

Udowodnimy teraz, że D wraz z projekcjami {πn:DDnnω} jest granicą. Po pierwsze, dla GD mamy

πn(G)=yn={xnxG}=πn[G],

a więc projekcje są ciągłe. Po drugie, jeśli {gk:EDkkω} jest dowolną inną granicą, to zdefiniujmy h:ED jako h(x)=(g0(x),g1(x),...). Z definicji powyższej wynika, że dla każdego kω mamy $\pi_k \circ h = g_k</math>. Zauważmy, że to świadczy o jednoznaczności wyboru h. A zatem D jest granicą omawianego diagramu. Co więcej, z jednoznaczności granicy wnioskujemy, że DE. QED

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ć poewne restrykcje zarówno na kształ 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 posetów zupełnych. 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[DD]. Okazuje się, że jego nietrywialne rozwiązania istnieja! Tak więc istnieją posety, które są izomorficzne z przestrzenią swoich ciągłych endofunkcji! Jeden z takich częściowych porządków skonstruujemy poniżej, pod koniec wykładu.

Twierdzenie. Rozważmy diagram F w kategorii Dcpo taki, że:

1. Wierzchołkami F są posety D0,D1,D2,...;

2. Dla nm istnieją funkcje emn:DnDm i pnm:DmDn tworzące parę e-p; 3. Dla każdego nω mamy enn=1Dn;

4. Dla nmk mamy ekn=ekmemn oraz pnk=pnmpmk.

Zdefiniujmy:

D={(x0,x1,...)(nm)(xn=pnm(xm))},

pm:DDm,  (x0,x1,...)xm, mω

em:DmD, x(kn,mpnkekm(x)nω).

Wtedy:

5. Para (em,pm) jest parą e-p i zachodzi nωenpn=1D,

6.{pn:DDn} jest granicą diagramu F. Jeśli {gn:CDn} jest dowolną inną granicą, to izmorfizm h:CD jest dany jako h(x)=(gn(x)nω) lub h=nengn;

7.{en:DnD} jest granicą odwrotną diagramu F. Jeśli {fn:EDn} jest dowolną inną granicą, to izmorfizm f:DE jest dany jako f(xnnω)=nfn(xn) lub f=nfnpn.

Dowód: W Twierdzeniu ??? pokazaliśmy już, że granicą diagramu jest {pn:DDn} i że izomorfizm h:CD ma (pierwszą z) postulowanych postaci. Pokażmy teraz, że funkcje em są dobrze zdefiniowane, tj. że y=em(x) należy do D dla dowolnego mω. Niech m będzie dowolne i załóżmy, że nn. Mamy:

pnn(yn)=pnn(kn,mpnkekm(x))=kn,mpnnpnkekm(x)=kn,mpnkekm(x)=yn.

W dowodzie korzystaliśmy kolejno z: definicji yn, ciągłości pnn i definicji yn. A zatem y=(y0,y1,...)D. Co więcej, funkcje em są ciągłe, gdyż tylko funkcje ciągłe zostały użyte w ich definicji.

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


empm(xnnω)=em(xm)=(kn,mpnkekm(xm)nω)=(kn,mpnkekmpmk(xk)nω)(kn,mpnk(xk)nω)=(knpnk(xk)nω)=(xnnω).

Ponadto, pmem(x)=pm(kn,mpnkekm(x)nω)=kmpmkekm(x)=x.

Bliższa analiza pokazuje, że empm pozostawi niezmienione te elementy ciągu (xnnω) gdzie nm:

pn(empm(xnnω))=...=pn(kn,mpnkekmpmk(xk)nω)=pn(kn,mpnmpmkekmpmk(xk)nω)=pn(kn,mpnmpmk(xk)nω)=pn(knpnk(xk)nω)=pn(knxnnω)=pn(xnnω)=xn.

To dowodzi, że nenpn=1D, czyli (5).

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

h=1Dh=nEnpnh=emgn,

co kończy dowód (6).

Do pokazania pozostała nam (7), czyli fakt, że {en:DnD} jest granicą odwrotną diagramu F Jeśli {fn:EDn} jest dowolną inną granicą, to sprawdźmy najpierw czy funkcja f=nfnpn jest dobrze zdefiniowana, tj. czy supremum jest nad zbiorem skierowanym. Ale tak jest, ponieważ dla nm:

fnpn=fmemnpnmpmfmpm.

Co więcej,

fem=nmfnpnem=nmfnpnenenm=nmfnenm=nmfm=fm.

W końcu pokażemy, że funkcja f o podanych własnościach jest tylko jedna. Jeśli dla f:DE zachodzi fem=fm, to fempm=fmpm, a zatem mfempm=mfmpm, czyli z ciągłości f: f(mempm)=mfmpm. Ale mempm=1D oraz mfmpm=f co daje f1D=f czyli f=f. QED.

Kategoria DcpoEP

W tej kategorii obiektami są posety zupełne posiadające element najmniejszy, zaś morfizmami są pary e-p, o których była mowa na początku wykładu ???. Złożenie morfizmów

[DIAGRAM]

definiujemy w naturalny sposób jako morfizm

[DIAGRAM]

Czy (e2e1,p1p2) jest parą e-p? Tak, ponieważ: e2e1p1p2e21Ep2=e2p21F oraz p1p2e2e1=p11Ee1=p1e1=1D. A zatem złożenie par e-p jest dobrze zdefiniowane, a co za tym idzie, i co łatwo już teraz pokazać, DcpoEP jest kategorią.

Definicja. Nazwijmy ω-kategorią każdą kategorię, w której diagram postaci

[DIAGRAM]

posiada granicę odwrotną.


Zauważmy, że twierdzenie o zgodności granicy prostej i odwrotnej (Twierdzenie ???) mówi, że DcpoEP jest ω-kategorią!

Definicja. Funktor F między ω-kategoriami nazywamy ciągłym, jeśli zachowuje granice odwrotne, t.j. jeśli D jest granicą diagramu ???, to F(D) jest granicą diagramu

[DIAGRAM]

Lemat. Niech 𝐀 będzie ω-kategorią, F:𝐀𝐀 funktorem ciągłym, f:AF(A) morfizmem w 𝐀 oraz niech diagram

[DIAGRAM]

posiada granicę odwrotną D. Wówczas DF(D).


Dowód: Skoro D jest granicą odwrotną diagramu ???, to

[DIAGRAM]

komutuje. W szczególności

[DIAGRAM]

komutuje i jak łatwo zauważyć D jest jego granicą. Ale z ciągłości F mamy, że diagram

[DIAGRAM]

komutuje i F(D) jest jego granicą. A zatem DF(D) wynika z Lematu ???. QED.

Przykład. Przekątna Δ:𝐃𝐜𝐩𝐨𝐃𝐜𝐩𝐨×𝐃𝐜𝐩𝐨, a(a,a); f(f,f) dla a𝐃𝐜𝐩𝐨0 f𝐃𝐜𝐩𝐨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. Funktor F:𝒟 pomiędzy kategoriami posetów 𝒟, jest {\em lokalnie ciągły} jeśli przekształcenia fF(f) typu Hom(D,D)Hom(F(D),F(D)) są ciągłe w sensie Scotta dla każdej pary obiektów D,D𝒟0.

Dla przykładu przeczytajmy tę definicję dla bifunktora F:𝐃𝐜𝐩𝐨op×𝐃𝐜𝐩𝐨𝐃𝐜𝐩𝐨: funktor F jest lokalnie ciągły, jeśli dla dowolnych zbiorów skierowanych A[D2D1] i B[D3D4], gdzie D1,...,D4𝐃𝐜𝐩𝐨0 mamy F(A,B)=fA,gGF(f,g). Zauważmy, że supremum po prawej stronie istnieje w [F(D1,D3)F(D2,D4)].

Przykład. Eksponent [__]:𝐃𝐜𝐩𝐨op×𝐃𝐜𝐩𝐨𝐃𝐜𝐩𝐨 jest lokalnie ciągły, ponieważ [fg]=curry(gev(1×f)) jest złożeniem funkcji ciągłych w sensie Scotta.


Lemat. Niech funktor F:𝐃𝐜𝐩𝐨op×𝐃𝐜𝐩𝐨𝐃𝐜𝐩𝐨 będzie lokalnie ciągły. Wtedy istnieje ciągły funktor F^:DcpoEP×DcpoEPDcpoEP którego działanie na obiekty jest takie samo, jak funktora F.

Dowód: Połóżmy F^(a,b)=F(a,b), gdzie a,b są posetami ciągłymi z elementami najmniejszymi. Rozważmy pary e-p:

[DIAGRAM]

Możemy wówczas stworzyć diagram

[DIAGRAM]

i para morfizmów powyżej jest parą e-p. Rzeczywiście: F(e,s)F(p,j)=F(pe,sj)=F(1a,1b)=1F(a,b)). Wykorzystaliśmy kolejno: kontrawariantność F dla pierwszego argumentu, własności par e-p i definicję funktora. Ponadto, F(p,j)F(e,s)=F(ep,js)F(1a,1b)=1F(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.