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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Pqw (dyskusja | edycje)
Nie podano opisu zmian
 
Pqw (dyskusja | edycje)
wykład 13.1
Linia 28: Linia 28:
'''rekursywnych równań dziedzinowych''' (''ang. recursive domain equations''). Przykładem takiego równania jest <math>D\cong [D\to D]</math>.  Okazuje się, że jego nietrywialne rozwiązania istnieja! Tak więc istnieją posety, które są izomorficzne z przestrzenią swoich
'''rekursywnych równań dziedzinowych''' (''ang. recursive domain equations''). Przykładem takiego równania jest <math>D\cong [D\to D]</math>.  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.
ciągłych endofunkcji! Jeden z takich częściowych porządków skonstruujemy poniżej, pod koniec wykładu.
'''Twierdzenie'''. Rozważmy diagram <math>F</math>  w kategorii '''Dcpo''' taki, że:
1. Wierzchołkami <math>F</math> są posety <math>D_0, D_1, D_2, ...</math>;
2. Dla <math>n\leq m</math>  istnieją funkcje <math>e_{mn}\colon D_n\to D_m</math> i  <math>p_{nm}\colon D_m\to D_n</math>  tworzące parę e-p;
3. Dla każdego <math>n\in \omega</math>  mamy <math>e_{nn} = 1_{D_n}</math>;
4. Dla <math>n\leq m\leq k</math>  mamy <math>e_{kn} = e_{km}\circ e_{mn}</math>  oraz <math>p_{nk} = p_{nm}\circ p_{mk}</math>. 
Zdefiniujmy:
<math>D = \{ (x_0, x_1, ...)\mid (\forall n\leq m)(x_n=p_{nm}(x_m)) \},</math>
<math>p_m\colon D\to D_m,\ \ (x_0, x_1, ...)\mapsto x_m, \ m\in \omega</math>
<math>e_m\colon D_m\to D, \ x\mapsto (\bigvee_{k\geq n,m} p_{nk}\circ e_{km}(x)\mid n\in \omega).</math>
Wtedy:
5. Para <math>(e_m, p_m)</math>  jest parą e-p i zachodzi <math>\bigvee_{n\in \omega} e_n\circ p_n = 1_{D}</math>, 
6.<math>\{p_n\colon D\to D_n\}</math>  jest granicą diagramu <math>F</math>. Jeśli <math>\{g_n\colon C\to D_n\}</math>  jest dowolną inną granicą, to izmorfizm <math>h\colon C\to D</math>  jest dany jako <math>h(x) = (g_n(x)\mid n\in\omega)</math>  lub <math>h = \bigvee_n e_n\circ g_n</math>;
7.<math>\{e_n\colon D_n\to D\}</math>  jest granicą odwrotną diagramu <math>F</math>. Jeśli <math>\{f_n\colon E\to D_n\}</math>  jest dowolną inną granicą, to izmorfizm <math>f\colon D\to E</math>  jest dany jako <math>f(x_n\mid n\in \omega) = \bigvee_n f_n(x_n)</math>  lub <math>f = \bigvee_n f_n\circ p_n</math>.

Wersja z 16:26, 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.