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

==Zadanie 13.1==

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

w h i l e X > 0 d o (Y : = X * X; X : = X - 1)

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

(x_{1}, y_{1}) ⊑ (x_{2}, y_{2}) ⟺ x_{i} ⊑ y_{i}, i = 1, 2

Rozwiązanie:

Zauważmy, że (zachowując oznaczenia z wykładu) semantyką $θ$ 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_{⊥}$ przypisze wartość true, jeśli $x > 0$ , przypisze wartość false, jeśli $x \leq 0$ oraz przypisze wartość $⊥$ , jeśli $x = ⊥$ .

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

[[Y : = X * Y]] (x, y) = (x, x y)

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 $θ^{'} = [[Y : = X * Y; X = X - 1]]$ jest funkcją daną jako:

θ^{'} (x, y) = (x - 1, x y)

A zatem zgodnie z (fix) mamy:

F (θ) (x, y) = C o n d (p (x, y), θ (θ^{'} (x, y)), (x, y))

czyli

F (θ) (x, y) = {\begin{cases} (x, y), & jeśli x = 0, \\ θ (x - 1, x y), & jeśli x > 0, \\ ⊥, & w przeciwnym przypadku . \end{cases}

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

θ_{1} (x, y) = F (θ_{0}) (x, y) = {\begin{cases} (x, y), & jeśli x = 0, \\ ⊥, & jeśli x \geq 1 \lor (x, y) = ⊥ . \end{cases}

W szczególności, mamy:

θ_{1} (x - 1, x y) = {\begin{cases} (x - 1, x y), & jeśli x - 1 = 0, \\ ⊥, & jeśli x \geq 2 \lor (x, y) = ⊥, \end{cases}

co daje:

θ_{2} (x, y) = F (θ_{1}) (x, y) = {\begin{cases} (x, y), & jeśli x = 0, \\ (0, y), & jeśli x = 1, \\ ⊥, & jeśli x \geq 2 \lor (x, y) = ⊥ . \end{cases}

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

θ_{3} (x, y) = F (θ_{2}) (x, y) = {\begin{cases} (x, y), & jeśli x = 0, \\ (0, y), & jeśli x = 1, \\ (0, 2 y), & jeśli x = 2, \\ ⊥, & jeśli x \geq 3 \lor (x, y) = ⊥, \end{cases}

θ_{4} (x, y) = F (θ_{3}) (x, y) = {\begin{cases} (x, y), & jeśli x = 0, \\ (0, y), & jeśli x = 1, \\ (0, 2 y), & jeśli x = 2, \\ (0, 6 y), & jeśli x = 3, \\ ⊥, & jeśli x \geq 4 \lor (x, y) = ⊥, \end{cases}

i w ogólności:

θ_{n} (x, y) = {\begin{cases} (x, y), & jeśli x = 0, \\ (0, (x!) y), & jeśli 0 < x < n, \\ ⊥, & jeśli x \geq 4 \lor (x, y) = ⊥ . \end{cases}

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

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

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

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

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

Podsumowując, funkcja

θ \overset{d e f}{=} θ_{\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 $⊥$ i $f : P \to P$ funkcją ciągłą. Funkcja $f$ posiada najmniejszy punkt stały $f i x (f)$ dany jako:

f i x (f) = ⋁^{↓} {f^{n} (⊥) ∣ n \in ω}

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

Rozwiązanie:

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

f (⊥) ⊑ f (f (⊥)) = f^{2} (⊥), f^{2} (⊥) ⊑ f^{3} (⊥), . . ., f^{n} (⊥) ⊑ f^{n + 1}, . .

i tak dalej. A zatem zbiór ${f^{n} ∣ b \in ω}$ (</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 (⋁_{n \in ω}^{↓} f^{n} (⊥)) = ⋁_{n \in ω}^{↓} f (f^{n} (⊥)) = ⋁_{n \in ω}^{↓} f^{n + 1} (⊥) = ⋁_{n \in ω}^{↓} f^{n} (⊥)

co dowodzi, że $f i x (f) = ⋁_{n \in ω}^{↓} f^{n} (⊥)$ jest punktem stałym funkcji $f$ .

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

f i x (f) = ⋁_{n \in ω}^{↓} f^{n} (⊥) ⊑ x

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

Pokażemy teraz, że operator

f i x

jest ciągły. Rozważmy dla każdego

n \in ω

funkcję

i t_{n} : [P, P] \to P

:

i t_{n} (f) = f^{n} (⊥)

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

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

\begin{aligned} i t_{n + 1} (⋁^{↓} F) & = & (⋁^{↓} F) (i t_{n} (⋁^{↓} F)) \\ = & (⋁^{↓} F) (⋁_{f \in F}^{↓} i t_{n} (f)) \\ = & ⋁_{g \in F}^{↓} g (⋁_{f \in F}^{↓} i t_{n} (f)) \\ = & ⋁_{g \in F}^{↓} ⋁_{f \in F}^{↓} g (i t_{n} (f)) \\ = & ⋁_{(f, g) \in F \times F}^{↓} g (i t_{n} (f)) \\ = & ⋁_{(f, f) \in F \times F}^{↓} f (i t_{n} (f)) \\ = & ⋁_{f \in F}^{↓} f (i t_{n} (f)) \\ = & ⋁_{f \in F}^{↓} i t_{n + 1} (f) . \end{aligned}

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

Zauważmy, że funkcje

{i t_{n} ∣ n \in ω}

tworzą łańcuch, a więc jego supremum istnieje i jak łatwo pokazać tym supremum jest

f i x

.

==Zadanie 13.3==

Niech $D, E, Z$ będą dcpo oraz $f : 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^{↑} D$ oraz $x \in E$ mamy:

f (⋁^{↓} A, x) = f (⋁^{↓} A, ⋁^{↓} {x}) = ⋁^{↓} f [A \times {x}] = ⋁_{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:

\begin{aligned} f (⋁^{↓} F) & = & f (⋁^{↓} π_{D} [F], ⋁^{↓} π_{E} [F]) \\ = & ⋁_{a \in π_{D} [F]}^{↓} f (a, ⋁^{↓} π_{E} [F]) \\ = & ⋁_{a \in π_{D} [F]}^{↓} ⋁_{b \in π_{E} [F]}^{↓} f (a, b) \\ = & ⋁_{(a, b) \in π_{D} [F] \times π_{E} [F]}^{↓} f (a, b) \\ = & ⋁_{(a, b) \in F}^{↓} f (a, b) \\ = & ⋁^{↓} 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 ⊑ x$ i $b, d ⊑ y$ . Z bc-zupełności $D$ i $E$ wynika, że $a \lor c$ i $b \lor d$ istnieją. A zatem $(a \lor c, b \lor 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) ≪ (z, w) ⟺ (x ≪ z \land y ≪ w)

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

Dla dowodu implikacji odwrotnej, niech $x ≪ z$ i $y ≪ w$ . Załóżmy, że $G D \times E$ będzie taki, że $(z, w) ⊑ ⋁^{↓} G$ . Z definicji porządku na produkcie, $z ⊑ π_{D} [⋁^{↓} G] = ⋁^{↓} π_{D} [G]$ , a zatem z założenia istnieje $(r, s) \in G$ taki, że $x ⊑ r$ . Podobnie, $w ⊑ π_{E} [⋁^{↓} G] = ⋁^{↓} π_{E} [G]$ , a zatem istnieje</math>(r',s')\in G</math> taki, że $y ⊑ s^{'}$ . Ze skierowania $G$ wynika, że istnieje element $(r^{″}, s^{″}) \in G$ powyżej $(r, s)$ i $(r^{'}, s^{'})$ . A zatem $(x, y) ⊑ (r^{″}, s^{″})$ , co dowodzi, że $(x, y) ≪ (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:

⋁^{↓} (x, y) = ⋁^{↓} x \times y = (⋁^{↓} x, ⋁^{↓} 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 ↘ y)

jest funkcją prostą pomiędzy posetami ciągłymi

D

i

E

i

E

posiada element najmniejszy

⊥

. Niech

U

będzie otwarty w

E

. Jeśli

⊥ \in U

, to

U = E

i wtedy

(x ↘ y)^{- 1} [U] = D

. Jeśli natomiast

⊥ \notin U

, to

(x ↘ 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 ↘ y)

jest ciągła.

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

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia