Teoria kategorii dla informatyków/Ćwiczenia 13: Teoria dziedzin II

==Zadanie 13.1==

(Autorem jest Andy Pitts). Przedyskutować semantykę pętli:

${\mathtt {while}}\ X>0\ {\mathtt {do}}\ (Y:=X*X;X:=X-1),$

gdy zbiór stanów programu jest posetem $S_{\bot }$, gdzie $S=\mathbb {N} \times \mathbb {N}$ ma porządek po współrzędnych:

$(x_{1},y_{1})\sqsubseteq (x_{2},y_{2})\iff x_{i}\sqsubseteq y_{i},\ i=1,2.$

Rozwiązanie:

Zauważmy, że (zachowując oznaczenia z wykładu) semantyką $\theta$ powyższej pętli będzie punkt stały równania (fix). Rozszyfrujmy na wstępie postać funkcji $F$ i wszystkich elementów ją definiujących. Po pierwsze, poczyńmy naturalne założenie, że $p=[\![X>0]\!]$ jest funkcją, która parze $(x,y)\in S_{\bot }$ przypisze wartość true, jeśli $x>0$, przypisze wartość false, jeśli $x\leq 0$ oraz przypisze wartość $\bot$, jeśli $x=\bot$.

Po drugie, załóżmy, że $[\![Y:=X*Y]\!]$ jest funkcją daną z góry jako:

$[\![Y:=X*Y]\!](x,y)=(x,xy)$

oraz $[\![X:=X-1]\!]$ jest funkcją daną z góry jako:

$[\![X:=X-1]\!](x,y)=(x-1,y).$

Zgodnie z definicją semantyki IMPmamy więc, że $\theta '=[\![Y:=X*Y;X=X-1]\!]$ jest funkcją daną jako:

$\theta '(x,y)=(x-1,xy).$

A zatem zgodnie z (fix) mamy:

$F(\theta )(x,y)=Cond(p(x,y),\theta (\theta '(x,y)),(x,y))$

czyli

$F(\theta )(x,y)={\begin{cases}(x,y),&{\text{ jeśli }}x=0,\\\theta (x-1,xy),&{\text{ jeśli }}x>0,\\\bot ,&{\text{ w przeciwnym przypadku }}.\end{cases}}$

Aby znaleźć funkcję $\theta \colon S_{\bot }\to S_{\bot }$ zastosujemy metodę kolejnych przybliżeń (metoda ta będzie precyzyjnie opisana w Zadaniu 13.2). Zdefiniujmy pierwsze przybliżenie $\theta$ jako funkcję $\theta _{0}\colon S_{\bot }\to S_{\bot }$, która każdemu elementowi $(x,y)\in S_{\bot }$ przypisuje element $\bot \in S_{\bot }$. Następnie budujemy ciąg dalszych przybliżeń jako $\theta _{n+1}=F(\theta _{n})$ dla $n\in \omega$. A zatem:

$\theta _{1}(x,y)=F(\theta _{0})(x,y)={\begin{cases}(x,y),&{\text{ jeśli }}x=0,\\\bot ,&{\text{ jeśli }}x\geq 1\vee (x,y)=\bot .\end{cases}}$

W szczególności, mamy:

$\theta _{1}(x-1,xy)={\begin{cases}(x-1,xy),&{\text{ jeśli }}x-1=0,\\\bot ,&{\text{ jeśli }}x\geq 2\vee (x,y)=\bot ,\end{cases}}$

co daje:

$\theta _{2}(x,y)=F(\theta _{1})(x,y)={\begin{cases}(x,y),&{\text{jeśli}}\ x=0,\\(0,y),&{\text{jeśli}}\ x=1,\\\bot ,&{\text{jeśli}}\ x\geq 2\vee (x,y)=\bot .\end{cases}}$

Kontynuując obliczenia w ten sam sposób, widzimy, że:

$\theta _{3}(x,y)=F(\theta _{2})(x,y)={\begin{cases}(x,y),&{\text{jeśli}}\ x=0,\\(0,y),&{\text{jeśli}}\ x=1,\\(0,2y),&{\text{jeśli}}\ x=2,\\\bot ,&{\text{jeśli}}\ x\geq 3\vee (x,y)=\bot ,\end{cases}}$ $\theta _{4}(x,y)=F(\theta _{3})(x,y)={\begin{cases}(x,y),&{\text{jeśli}}\ x=0,\\(0,y),&{\text{jeśli}}\ x=1,\\(0,2y),&{\text{jeśli}}\ x=2,\\(0,6y),&{\text{jeśli}}\ x=3,\\\bot ,&{\text{jeśli}}\ x\geq 4\vee (x,y)=\bot ,\end{cases}}$

i w ogólności:

$\theta _{n}(x,y)={\begin{cases}(x,y),&{\text{jeśli}}\ x=0,\\(0,(x!)y),&{\text{jeśli}}\ 0<x<n,\\\bot ,&{\text{jeśli}}\ x\geq 4\vee (x,y)=\bot .\end{cases}}$

Widzimy, że wartości funkcji $\theta _{0},\theta _{1},\theta _{2},...$ zgadzają się na wspólnych argumentach, a więc ich suma mnogościowa jest dobrze zdefiniowaną funkcją; nazwijmy ją $\theta _{\infty }$. Jak łatwo sprawdzić, $\theta _{\infty }$ jest dana jako:

$\theta _{\infty }(x,y)={\begin{cases}(x,y)&{\text{jeśli}}\ x=0\\(0,(x!)y)&{\text{jeśli}}\ x>0.\end{cases}}$

Czy $\theta _{\infty }$ spełnia równanie (fix)? Tak, ponieważ:

${\begin{aligned}F(\theta _{\infty })(x,y)&=&{\begin{cases}(x,y),&{\text{jeśli}}\ x=0,\\\theta _{\infty }(x-1,xy),&{\text{jeśli}}\ x>0,\end{cases}}\\&=&{\begin{cases}(x,y),&{\text{jeśli}}\ x=0,\\(0,y),&{\text{jeśli}}\ x=1,\\(0,(x-1)!xy),&{\text{jeśli}}\ x>1\\\end{cases}}\\&=&\theta _{\infty }(x,y).\end{aligned}}$

Tak naprawdę Zadanie 13.2 pokaże, że $\theta _{\infty }$ jest najmniejszym punktem stałym funkcji $F$.

Podsumowując, funkcja $\theta {\stackrel {def}{=}}\theta _{\infty }$ spełnia wszystkie warunki, aby móc pretendować do roli semantyki pętli while.

==Zadanie 13.2==

Udowodnij twierdzenie Scotta o punkcie stałym: niech $P$ będzie dcpo posiadającym element najmniejszy $\bot$ i $f\colon P\to P$ funkcją ciągłą. Funkcja $f$ posiada najmniejszy punkt stały $fix(f)$ dany jako:

$fix(f)=\bigvee {}^{\downarrow }\{f^{n}(\bot )\mid n\in \omega \}.$

Co więcej, operator $fix\colon [P,P]\to P$, $f\mapsto fix(f)$ przyporządkowujący funkcji $f$ jej najmniejszy punkt stały, jest również funkcją ciągłą.

Rozwiązanie:

Ponieważ $\bot$ jest elementem najmniejszym, to $\bot \sqsubseteq f(\bot )$. Z monotoniczności $f$ wynika też, że:

$f(\bot )\sqsubseteq f(f(\bot ))=f^{2}(\bot ),f^{2}(\bot )\sqsubseteq f^{3}(\bot ),...,f^{n}(\bot )\sqsubseteq f^{n+1},...$

i tak dalej. A zatem zbiór $\{f^{n}\mid b\in \omega \}$ (</math>\omega</math> oznacza liczby naturalne) jest łańcuchem. Ponieważ $P$ jest dcpo, jego supremum istnieje. Z ciągłości $f$ mamy więc, że:

$f(\bigvee {}_{n\in \omega }^{\downarrow }f^{n}(\bot ))=\bigvee {}_{n\in \omega }^{\downarrow }f(f^{n}(\bot ))=\bigvee {}_{n\in \omega }^{\downarrow }f^{n+1}(\bot )=\bigvee {}_{n\in \omega }^{\downarrow }f^{n}(\bot ),$

co dowodzi, że $fix(f)=\bigvee {}_{n\in \omega }^{\downarrow }f^{n}(\bot )$ jest punktem stałym funkcji $f$.

Jeśli $x\in D$ jest innym punktem stałym $f$, to $\bot \sqsubseteq x$ oraz $f(\bot )\sqsubseteq f(x)=x,...,f^{n}(\bot )\sqsubseteq f^{n}(x)=x$; prosta indukcja pokazuje więc, że:

$fix(f)=\bigvee {}_{n\in \omega }^{\downarrow }f^{n}(\bot )\sqsubseteq x.$

Dowiedliśmy zatem, że $fix(f)$ jest najmniejszym punktem stałym funkcji $f$.

Pokażemy teraz, że operator $fix$ jest ciągły. Rozważmy dla każdego $n\in \omega$ funkcję $it_{n}\colon [P,P]\to P$: $it_{n}(f)=f^{n}(\bot ).$

Zauważmy, że $it_{0}$, przyporządkowująca każdej funkcji $f$ element najmniejszy $\bot$, jest funkcją ciągłą. Załóżmy więc, że $it_{n}$ jest funkcją ciągłą. Pokażemy, że $it_{n+1}$ jest ciągła.

Niech $F$ będzie skierowaną rodziną funkcji ciągłych z supremum $\bigvee {}^{\downarrow }F$. To supremum zawsze istnieje, bo $[P,P]$ jest dcpo. Mamy:

${\begin{aligned}it_{n+1}(\bigvee {}^{\downarrow }F)&=&(\bigvee {}^{\downarrow }F)(it_{n}(\bigvee {}^{\downarrow }F))\\&=&(\bigvee {}^{\downarrow }F)(\bigvee {}_{f\in F}^{\downarrow }it_{n}(f))\\&=&\bigvee {}_{g\in F}^{\downarrow }g(\bigvee {}_{f\in F}^{\downarrow }it_{n}(f))\\&=&\bigvee {}_{g\in F}^{\downarrow }\bigvee {}_{f\in F}^{\downarrow }g(it_{n}(f))\\&=&\bigvee {}_{(f,g)\in F\times F}^{\downarrow }g(it_{n}(f))\\&=&\bigvee {}_{(f,f)\in F\times F}^{\downarrow }f(it_{n}(f))\\&=&\bigvee {}_{f\in F}^{\downarrow }f(it_{n}(f))\\&=&\bigvee {}_{f\in F}^{\downarrow }it_{n+1}(f).\end{aligned}}$

W dowodzie powyższym wykorzystaliśmy kolejno: definicję $it$, hipotezę indukcyjną, definicję $\bigvee {}^{\downarrow }F$, ciągłość $g$, własność supremów, współkońcowość zbioru $\{(f,f)\mid f\in F\}$ w $F\times F$, prostą własność indeksów i definicję $it$. Z twierdzenia o indukcji wynika więc, że $it_{n}$ jest funkcją ciągłą dla każdego $n\in \omega$.

Zauważmy, że funkcje $\{it_{n}\mid n\in \omega \}$ tworzą łańcuch, a więc jego supremum istnieje i jak łatwo pokazać tym supremum jest $fix$.

==Zadanie 13.3==

Niech $D,E,Z$ będą dcpo oraz $f\colon D\times E\to Z$ będzie funkcją dwóch argumentów. Funkcja $f$ jest ciągła wtedy i tylko wtedy, gdy jest ciągła ze względu na każdy z argumentów.

Rozwiązanie:

Jeśli $f$ jest ciągła, to oczywiście dla dowolnego $A\subseteq ^{\uparrow }D$ oraz $x\in E$ mamy:

$f(\bigvee {}^{\downarrow }A,x)=f(\bigvee {}^{\downarrow }A,\bigvee {}^{\downarrow }\{x\})=\bigvee {}^{\downarrow }f[A\times \{x\}]=\bigvee {}_{a\in A}^{\downarrow }f(a,x).$

Dowód ciągłości ze względu na drugi argument jest analogiczny.

Załóżmy więc, że $f$ jest ciągła ze względu na każdy z argumentów. Pokażemy, że $f$ jest ciągła. Niech $F$ będzie skierowanym podzbiorem $D\times E$. Mamy:

${\begin{aligned}f(\bigvee {}^{\downarrow }F)&=&f(\bigvee {}^{\downarrow }\pi _{D}[F],\bigvee {}^{\downarrow }\pi _{E}[F])\\&=&\bigvee {}_{a\in \pi _{D}[F]}^{\downarrow }f(a,\bigvee {}^{\downarrow }\pi _{E}[F])\\&=&\bigvee {}_{a\in \pi _{D}[F]}^{\downarrow }\bigvee {}_{b\in \pi _{E}[F]}^{\downarrow }f(a,b)\\&=&\bigvee {}_{(a,b)\in \pi _{D}[F]\times \pi _{E}[F]}^{\downarrow }f(a,b)\\&=&\bigvee {}_{(a,b)\in F}^{\downarrow }f(a,b)\\&=&\bigvee {}^{\downarrow }f[F].\end{aligned}}$

==Zadanie 13.4==

Udowodnij Twierdzenie 13.4.

Wskazówka:

Poset $D\times E$ jest oczywiście dcpo, co wynika z Twierdzenia 13.1.

Rozwiązanie:

Załóżmy, że elementy $(a,b),(c,d)$ są ograniczone z góry przez element $(x,y)\in D\times E$. Z definicji porządku na $D\times E$ wynika, że $a,c\sqsubseteq x$ i $b,d\sqsubseteq y$. Z bc-zupełności $D$ i $E$ wynika, że $a\vee c$ i $b\vee d$ istnieją. A zatem $(a\vee c,b\vee d)$ istnieje i jest supremum elementów $(a,b)$ i $(c,d)$.

Pokażemy teraz, że $D\times E$ jest ciągły. Na początek dowiedziemy, że:

$(x,y)\ll (z,w)\iff (x\ll z\wedge y\ll w).$

Załóżmy, że $(x,y)\ll (z,w)$. Niech $AD$ będzie taki, że $z\sqsubseteq \bigvee {}^{\downarrow }A$. Wówczas $A\times \{w\}D\times E$ i z założenia istnieje element $a\in A$ taki, że $(x,y)\sqsubseteq (a,w)$. A zatem $x\sqsubseteq a$ dla $a\in A$, co dowodzi, że $x\ll z$. Podobnie pokazujemy, że założenie $(x,y)\ll (z,w)$ implikuje $y\ll w$.

Dla dowodu implikacji odwrotnej, niech $x\ll z$ i $y\ll w$. Załóżmy, że $GD\times E$ będzie taki, że $(z,w)\sqsubseteq \bigvee {}^{\downarrow }G$. Z definicji porządku na produkcie, $z\sqsubseteq \pi _{D}[\bigvee {}^{\downarrow }G]=\bigvee {}^{\downarrow }\pi _{D}[G]$, a zatem z założenia istnieje $(r,s)\in G$ taki, że $x\sqsubseteq r$. Podobnie, $w\sqsubseteq \pi _{E}[\bigvee {}^{\downarrow }G]=\bigvee {}^{\downarrow }\pi _{E}[G]$, a zatem istnieje </math>(r',s')\in G</math> taki, że $y\sqsubseteq s'$. Ze skierowania $G$ wynika, że istnieje element $(r'',s'')\in G$ powyżej $(r,s)$ i $(r',s')$. A zatem $(x,y)\sqsubseteq (r'',s'')$, co dowodzi, że $(x,y)\ll (z,w)$.

Z powyższych rozważań wynika, że dla dowolnego $(x,y)\in D\times E$ mamy $(x,y)=x\times y$; w szczególności zbiór ten jest skierowany. Co więcej:

$\bigvee {}^{\downarrow }(x,y)=\bigvee {}^{\downarrow }x\times y=(\bigvee {}^{\downarrow }x,\bigvee {}^{\downarrow }y)=(x,y).$ To znaczy, że $D\times E$ jest posetem ciągłym.

==Zadanie 13.5==

Udowodnij, że funkcje proste są ciągłe.

Rozwiązanie:

Załóżmy, że $(x\searrow y)$ jest funkcją prostą pomiędzy posetami ciągłymi $D$ i $E$ i $E$ posiada element najmniejszy $\bot$. Niech $U$ będzie otwarty w $E$. Jeśli $\bot \in U$, to $U=E$ i wtedy $(x\searrow y)^{-1}[U]=D$. Jeśli natomiast $\bot \notin U$, to $(x\searrow y)^{-1}[U]=x$. Z ciągłości $D$ wynika, że $x$ jest zbiorem otwartym. Pokazaliśmy, że przeciwobraz dowolnego zbioru $U\subseteq E$ jest otwartym podzbiorem $D$. A zatem funkcja $(x\searrow y)$ jest ciągła.