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

From Studia Informatyczne

==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=\bo.

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ż:

\aligned \begin{eqnarray*}  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). \endaligned

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{}^\downarrow_{n\in \omega} f^n(\bot)) =  \bigvee{}^\downarrow_{n\in \omega}  f(f^n(\bot)) =  \bigvee{}^\downarrow_{n\in \omega} f^{n+1}(\bot) =  \bigvee{}^\downarrow_{n\in \omega} f^{n}(\bot),

co dowodzi, że fix(f) = \bigvee{}^\downarrow_{n\in \omega} 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{}^\downarrow_{n\in \omega}  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:

\aligned it_{n+1}(\bigvee{}^\downarrow F) & = & (\bigvee{}^\downarrow  F)(it_n(\bigvee{}^\downarrow F))\\                     & = & (\bigvee{}^\downarrow F)(\bigvee{}^\downarrow_{f\in F} it_n(f))\\                     & = & \bigvee{}^\downarrow_{g\in F} g(\bigvee{}^\downarrow_{f\in F} it_n(f))\\                     & = & \bigvee{}^\downarrow_{g\in F}\bigvee{}^\downarrow_{f\in F} g(it_n(f))\\                     & = & \bigvee{}^\downarrow_{(f,g)\in F\times F} g(it_n(f))\\                     & = & \bigvee{}^\downarrow_{(f,f)\in F\times F} f(it_n(f))\\                     & = & \bigvee{}^\downarrow_{f\in F} f(it_n(f))\\                     & = & \bigvee{}^\downarrow_{f\in F} it_{n+1}(f). \endaligned

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{}^\downarrow_{a\in A} 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:

\aligned   f(\bigvee{}^\downarrow F) & = & f(\bigvee{}^\downarrow \pi_D[F], \bigvee{}^\downarrow \pi_E[F])\\                & = & \bigvee{}^\downarrow_{a\in \pi_D[F]} f(a, \bigvee{}^\downarrow \pi_E[F])\\                & = & \bigvee{}^\downarrow_{a\in \pi_D[F]}\bigvee{}^\downarrow_{b\in \pi_E[F]}f(a,b)\\                & = & \bigvee{}^\downarrow_{(a,b)\in \pi_D[F]\times \pi_E[F]}f(a,b)\\                & = & \bigvee{}^\downarrow_{(a,b)\in F} f(a,b)\\                & = & \bigvee{}^\downarrow f[F]. \endaligned

==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 A\subseteqdir D będzie taki, że z\sqsubseteq  \bigvee{}^\downarrow A. Wówczas A\times  \{w\}\subseteqdir 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 G\subseteqdir D\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 \ddn (x,y) = \ddn x\times \ddn y; w szczególności zbiór ten jest skierowany. Co więcej:

\bigvee{}^\downarrow \ddn (x,y) =  \bigvee{}^\downarrow \ddn x\times \ddn y = (\bigvee{}^\downarrow  \ddn x,  \bigvee{}^\downarrow \ddn 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]=\uup x. Z ciągłości D wynika, że \uup 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.