Teoria kategorii dla informatyków/Wykład 13: Teoria dziedzin II

From Studia Informatyczne

Wiedząc już z poprzedniego wykładu, czym są dziedziny, pokażemy, dlaczego kategorie dziedzin są ważne w informatyce, zwłaszcza w semantyce języków funkcyjnych. Zaczniemy od krótkiego wprowadzenia w tematykę, która jest tematem oddzielnego przedmiotu pt. Semantyka i weryfikacja programów.


Spis treści

Języki funkcyjne versus języki imperatywne.

Funkcyjne języki programowania są w zasadzie tak stare, jak lepiej znane języki imperatywne: FORTRAN, Pascal, C. Najstarszym językiem funkcyjnym jest LISP stworzony w latach pięćdziesiątych przez Johna McCarthy'ego LISP powstał w tym samym czasie co FORTRAN.) Podczas gdy języki imperatywne zostały stworzone głównie do usprawnienia obliczeń numerycznych, języki funkcyjne powstały z myślą o manipulacji symbolicznych struktur danych: drzew, list, kolejek, itd.

Podstawowym elementem składni języków imperatywnych są rozkazy, które zmieniają stan programu (np. poprzez przypisanie nowej wartości zadeklarowanej wcześniej zmiennej numerycznej), wyrażenia warunkowe (if...then...else) i pętle (np. while). Co więcej, języki imperatywne operują głównie na tablicach za pomocą wskaźników (tablice są najważniejszą strukturą danych dla obliczeń numerycznych).

W językach funkcyjnych nie ma natomiast pojęcia stanu programu ani rozkazów zmieniających tenże stan. Podstawowymi pojęciami są natomiast aplikacja funkcji do argumentu i definicja funkcji, która może być albo bezpośrednia, np. f(x) = x*x+1, albo rekursywna, np.:

f(x) = \mathtt{if}\ x=0\ \mathtt{then}\  1\  \mathtt{else}\  x*f(x-1).

Ponadto, skoro mamy do czynienia z funkcjami, potrzebne będą również podstawowe typy danych: liczby naturalne czy typ boolowski oraz wyrażenia warunkowe, by móc definiować funkcje przez przypadki. Dodatkowo, w znanych językach funkcyjnych takich jak LISP, Scheme, ML czy Haskell można definiować również rekursywne typy danych, np: drzewa.

Mówiąc w dużym uproszczeniu, programowanie imperatywne polega więc na wykonywaniu krok po kroku poszczególnych komend języka, zaś programowanie funkcyjne - na zdefiniowaniu odpowiedniej funkcji. W praktyce ta definicja składa się najczęściej z kombinacji mniej złożonych funkcji. Typowy program (w przeciwieństwie do definicjifunkcji) jest więc aplikacją funkcji do danych wejściowych, to znaczy ma formę f(e_1, e_2, ..., e_n); funkcja ta jest następnie obliczana (ewaluowana) przez interpreter języka. W praktyce, implementacje języków funkcyjnych pozwalają na kompilację programów.

Podkreślmy więc, że programowanie w języku funkcyjnym polega na definiowaniu funkcji i w przeciwieństwie do języków imperatywnych nie musimy się martwić o dynamiczne zachowanie programu, gdyż o to martwi się wyłącznie interpreter. Programista może więc skoncentrować się na tym co i nie myśleć o tym jak.

Style semantyki.

Semantyka to po prostu znaczenie. Gdy mówimy o semantyce (fragmentu) programu, to mamy na myśli oczekiwany wynik, rezultat wykonania programu, który stanowi jego znaczenie. Na przykład, semantyką fragmentu programu

f(x) = \mathtt{if}\  x=0\ \mathtt{then}\ 1\ \mathtt{else}\  x*f(x-1)

jest funkcja silnia. Semantyka języka programowania jest więc niczym innym, tylko znaczeniem poszczególnych konstrukcji składniowych definiujących język.

Zwykle mówi się o trzech stylach semantyki. Są to:


Semantyka aksjomatyczna

Znaczenie fragmentów programu definiuje się aksjomatycznie podając również reguły pewnej logiki własności programu.

===Semantyka operacyjna=== Znaczenie programu definiuje się, podając dozwolone kroki obliczeniowe dla poszczególnych fragmentów programu. Mówiąc konkretnie, semantyka operacyjna jest dana często poprzez indukcyjnie zdefiniowaną relację ewaluacji E\Downarrow V opisującą wszystkie sytuacje, gdy wyrażenie E redukuje się do wartości V (wartości to wyrażenia, które nie mogą być już uproszczone). Na przykład, jeśli E jest wyrażeniem typu boolowskiego, to E\Downarrow V opisuje sytuację, gdy E przyjmuje wartość V \in \{true, false\}.

Zwróćmy uwagę, że w ogólności nie istnieje wartość V dla każdego wyrażenia E taka, że E\Downarrow V, gdyż nie każdy program E kończy obliczenia (posiada własność stopu)!

Semantyka oparta na relacji \Downarrow pozwala zdefiniować równość (fragmentów) programów: mówimy, że dwa programy (wyrażenia) E_1 i E_2obserwowalnie równe (ang. observationally equal) wtedy i tylko wtedy, gdy

C[E_1]\Downarrow V \iff C[E_2]\Downarrow V      (*)

dla wszystkich kontekstów C[\cdot] i wszystkich wartości V. (w tej chwili wystarczy wiedzieć, że o kontekstach można myśleć jako o testach jakim poddajemy programy E_1, E_2). W tej interpretacji obserwacja programu to po prostu matematyczne sformułowanie koncepcji testowania programów; dwa programy są obserwowalnie równe, gdy przejdą te same testy.

Należy zauważyć, że obserwowalna równość jest trudna do sprawdzenia, gdyż definicja ((*)) wymaga kwantyfikacji po wszystkich kontekstach, a te tworzą kolekcję, którą niełatwo opisać. W związku z tym rodzi się potrzeba znalezienia takich kryteriów, które stwierdzają obserwowalną równość programów, lecz są niezależne od relacji ewaluacji \Downarrow i kontekstów. Dlatego wprowadza się również trzeci styl semantyki, zwany semantyką denotacyjną.

===Semantyka denotacyjna=== Tu każdemu fragmentowi programu E jest przypisana jego denotacja [\! [ E]\! ], czyli matematyczny obiekt reprezentujący jego znaczenie, np.

[\! [ f(x) = \mathtt{if}\  x=0\ \mathtt{then}\  1\ \mathtt{else}\  x*f(x-1)]\! ] =\  !\  \mathrm{(silnia)}.

Obiekt [\! [ E ]\! ]\in D jest nazywany również znaczeniem, semantyką, obiektem semantycznym i jest elementem pewnego zbioru D zwanego dziedziną semantyczną lub dziedziną. Tak właśnie dziedziny pojawiają się naturalnie w semantyce denotacyjnej!

Cechą charakterystyczną semantyki denotacyjnej jest to, że znaczenie fragmentu programu zależy wyłącznie od znaczenia jego podfragmentów. Ta cecha semantyki denotacyjnej jest nazywana kompozycyjnością (ang. compositionality). Przejdźmy do przykładów.

Prosty język imperatywny.

Użyjemy przykładu, który pojawia się w skrypcie prof. Gordona Plotkina pt. Pisa Notes (On Domain Theory).

Zdefiniujmy - za Plotkinem - prosty język imperatywny i nazwijmy go IMP.

SKŁADNIA:

  • BEx - zbiór wyrażeń boolowskich (oznaczanych metazmienną b),
  • Act - zbiór prymitywnych komend (oznaczanych metazmienną a),
  • Stat - zbiór zdań (oznaczanych metazmienną s) dany przez następującą gramatykę:
s ::= a \ \mid\ \mathtt{skip} \ \mid\ s\mathtt{;}s\ \mid\ (\mathtt{if }\ b \ \mathtt{then }\ s\ \mathtt{else}\ s).

OBIEKTY SEMANTYCZNE (DZIEDZINY):

  • \mathbf{Bool} =\{true, false\} - zbiór wartości logicznych (oznaczanych metazmienną t),
  • S - zbiór stanów programu (oznaczanych metazmienną \sigma),
  • C \subseteq (S\to S) - zbiór komend (oznaczanych metazmienną \theta).


SEMANTYKA: Semantykę określamy w tym wypadku poprzez podanie trzech funkcji}, po jednej dla każdego zbioru definiującego składnię. Niemniej jednak, zgodnie ze zwyczajem, każdą z tych funkcji oznaczamy w ten sam sposób poprzez podwójne nawiasy kwadratowe [\! [\cdot]\! ].

  • [\! [\cdot]\! ]\colon BEx\to (S\to \mathbf{Bool}) jest zadana z góry,
  • [\! [\cdot]\! ]\colon Act\to C jest zadana z góry,
  • [\! [\cdot]\! ]\colon Stat \to C jest zdefiniowana za pomocą dwóch poprzednich funkcji zgodnie z wymogiem składalności, jak następuje:
  • [\! [ \mathtt{skip} ]\! ] (\sigma) = \sigma,
  • [\! [ s_1;s_2]\! ] (\sigma)=[\! [ s_2]\! ]([\! [ s_1 ]\! ] (\sigma)),
  • [\! [ \mathtt{if }\ b \ \mathtt{then }\ s_1\ \mathtt{else}\ s_2]\! ](\sigma) = Cond([\! [ b]\! ](\sigma), [\! [ s_1]\! ](\sigma), [\! [ s_2]\! ](\sigma)), gdzie funkcja Cond\colon \mathbf{Bool} \times S\times S\to S jest dana jako: Cond(t, \sigma_1, \sigma_2) = \begin{cases} \sigma_1, & \text{jeśli} t=T, \\ \sigma_2, & \text{jeśli} t=F. \end{cases}

Dziedziny

Postaramy się teraz uzasadnić (znów za skryptem Pisa Notes (On Domain Theory) prof. Gordona Plotkina) dlaczego struktura częściowego porządku na dziedzinach jest konieczna i dlaczego zwykłezbiory nie są adekwatne jako modele programów i ich fragmentów.

Przypuśćmy, że rozszerzyliśmy nasz język IMP o dodatkowe zdanie:
s::= \mathtt{while}\ b\ \mathtt{do}\ s.
Oczekujemy, że semantyka pętli będzie taka sama jak semantyka frazy:
\mathtt{if}\ b\ \mathtt{then}\ s;\ \mathtt{while}\ b\ \mathtt{do}\ s\ \mathtt{else}\ \mathtt{skip}.

Stąd, jeśli oznaczymy semantykę powyższego jako \theta oraz przyjmiemy:

[\! [ b]\! ] = p\colon S\to  \mathbf{Bool},
[\! [ s]\! ] = \theta'\colon S\to S,

to oczekujemy (z definicji semantyki if...then...else), że:

\theta(\sigma) = Cond(p(\sigma), \theta(\theta'(\sigma)), \sigma).

W szczególnym przypadku, jeśli b=T i s=\mathtt{skip}, to:

\theta(\sigma) = \theta(\sigma),

czyli \theta może być dowolną funkcją! To przeczy jednak naszej intuicji, gdyż oczekiwalibyśmy, że w tym wypadku funkcja \theta powinna być po prostu niezdefiniowana. Innymi słowy, oczekujemy, że funkcje takie jak \theta pomiędzy dziedzinami semantycznymi będą definiowane jedynie dla niektórych argumentów. O funkcjach takich mówimy, że są częściowe.

Z matematycznego punktu widzenia, każda funkcja częściowa p\colon A\to B jest równoważna funkcji totalnej p'\colon A\to B_{\bot}, gdzie B_{\bot} jest sumą prostą zbioru B i elementu \bot nienależącego do B. Zdanie p'(x)=\bot jest interpretowane jako stwierdzenie, że funkcja p przyjmuje dla argumentu x wartość niezdefiniowaną\bot (znak \bot w języku angielskim czyta się bottom). Ten punkt widzenia jest bardzo ciekawy, gdyż okazuje się, że w tej interpretacji nic nie stoi na przeszkodzie, by pewien fragment programu miał niezdefiniowane znaczenie, a fragment większy, zawierający go, miał już nietrywialną semantykę. Wyciągnijmy pierwsze wnioski: dziedziny semantyczne powinny być wyposażone w dodatkowy element \bot oznaczający wartość niezdefiniowaną. Interpretacja elementu \bot sugeruje również, że dowolna funkcja p pomiędzy dziedzinami powinna spełniać p(\bot)=\bot.

W semantyce języków programowania, w których istnieje możliwość dokonywania obliczeń numerycznych, pojawią się z pewnością liczby naturalne, a konkretnie dziedzina \mathbb{N}_{\bot}. Definiując częściowy porządek na \mathbb{N}_{\bot} poprzez:

x\sqsubseteq y \iff (x=\bot) \vee  (x=y),
widzimy, że warunek p(\bot)=\bot jest równoważny stwierdzeniu, że funkcja p jest monotoniczna. Porządek na dziedzinie \mathbf{Bool}_{\bot} oznaczamy \mathbb{T} i definiujemy analogicznie. Podobnie dla innych dziedzin. Tak naprawdę każdy zbiór X może być zmieniony na poset X_{\bot} = X\cup\{\bot\} (gdzie \bot\notin X) poprzez:

(\forall x,y\in X) (x\sqsubseteq y\iff (x=\bot \vee x=y)).      (eq:flat)

Konsekwentnie, funkcja Cond omawiana powyżej typu \mathbb{T}\times S_{\bot}\times S_{\bot}\to S_{\bot} i jest zdefiniowana jako:
Cond (\bot, \sigma, \sigma') = \bot,
Cond (T, \sigma, \sigma') = \sigma,
Cond (F, \sigma, \sigma') = \sigma'.

Łatwo zauważyć, że jest to również funkcja monotoniczna. Podsumujmy więc nasze wymagania dotyczące dziedzin:

  • Dziedziny semantyczne są zbiorami częściowo uporządkowanymi.
  • Funkcje między dziedzinami (stanowiące matematyczny opis znaczenia fragmentów programu) zachowują częściowy porządek.
  • Funkcje między dziedzinami również tworzą dziedziny.

Rozwój semantyki denotacyjnej w ostatnich czterdziestu latach pokazał, że pomysł wyposażenia obiektów semantycznych w częściowy porządek między elementami jest naprawdę trafiony. Teoria dziedzin i, co za tym idzie, semantyka denotacyjna zostały stworzone pod koniec lat 60. na uniwersytecie w Oxfordzie przez Danę Scotta i Christophera Stracheya. Od początku lat 70. teoria dziedzin, jako odrębna teoria matematyczna, rozwijała się niezależnie w wielu ośrodkach naukowych, m.in. w Edynburgu (G. Plotkin), w Darmstadt (K.-H. Hofmann, K. Keimel, A. Jung), Cambridge (M. Fiore), Birmingham (M. Escard\'{o}), Tulane University w Nowym Orleanie (M. Mislove), Oxfordzie (S. Abramsky), Imperial College w Londynie (A. Edalat, M.B. Smyth) czy w Louisiana State University (J.D. Lawson).

Wróćmy na zakończenie do naszej próby zdefiniowania semantyki while; równość
[\! [ \mathtt{while}\ b\  \mathtt{do}\ s]\! ] = [\! [ \mathtt{if}\ b\ \mathtt{ then}\ s;\ \mathtt{while}\ b\ \mathtt{do}\ s\ \mathtt{ else}\ \mathtt{skip}]\! ]
pokazuje, że:

\theta =F(\theta)      (fix)

dla pewnej funkcji F zależnej od semantyki b i s. Konkretnie:
F = \lambda x.Cond (p, x\theta', 1),

gdzie 1 jest funkcją identycznościową na S_{\bot}. Równość (fix) oznacza, że znaczenie pętli \mathtt{while} jest niczym innym, tylko punktem stałym funkcji F typu (S_{\bot}\to S_{\bot}) \to (S_{\bot}\to S_{\bot}). Dodajmy więc jeszcze jedno wymaganie dotyczące struktury dziedzin semantycznych:

  • Każda funkcja między dziedzinami powinna posiadać punkt stały (a najlepiej - najmniejszy punkt stały, gdy okaże się, że równanie (fix) ma więcej niż jedno rozwiązanie).


Zarówno kategoria wszystkich dcpo z elementem najmniejszym (z funkcjami ciągłymi jako morfizmami, jak i kategoria dziedzin bc-zupełnych (również z funkcjami ciągłymi jako morfizmami) spełniają wszystkie powyższe wymagania, a nawet więcej. Pokażmy najpierw, że obie te kategorie są kartezjańsko zamknięte. Problemem istnienia punktów stałych funkcji ciągłych zajmiemy się w Ćwiczeniach do tego wykładu - Zadanie 13.2.

Kartezjańsko zamknięte kategorie dziedzin

Nie jest prawdą, że klasa dziedzin ciągłych jest domknięta ze względu na przestrzeń funkcyjną: można na przykład pokazać, że dla dziedziny ciągłej \mathbb{Z}^{-} liczb całkowitych ujemnych z porządkiem naturalnym, poset [\mathbb{Z}^{-}\to \mathbb{Z}^{-}] nie jest ciągły. Wiele podstawowych pytań dotyczących przestrzeni funkcyjnych między różnymi klasami dziedzin pozostaje do dziś bez odpowiedzi. Wiemy jednak, że kategorie \mathbf{Dcpo} (dcpo z funkcjami ciągłymi), \mathbf{Dcpo}_{\bot} - dcpo z elementami najmniejszymi plus funkcje ciągłe oraz \mathbf{BC} (bc-dziedziny i funkcje ciągłe) są kartezjańsko zamknięte. Dalsza część wykładu stanowi niespieszny dowód tych faktów.


Dcpo

Zaczynamy od produktu w kategorii \mathbf{Dcpo} (DCPO_{\bot}).

Twierdzenie 13.1 [Produkt dcpo]

Niech D,E będą dcpo. Mamy:
  • Zbiór D\times E = \{(d,e)\mid d\in D, e\in E\} z porządkiem po współrzędnych
(x_1,y_1)\sqsubseteq (x_2, y_2) \iff  (x_1\sqsubseteq x_2 \wedge y_1\sqsubseteq y_2)

jest dcpo.

  • Jeśli D i E posiadają elementy najmniejsze, to D\times E ma element najmniejszy (\bot_D,\bot_E).
  • Projekcje \pi_D\colon D\times E\to D i \pi_E\colon D\times E\to E dane odpowiednio przez \pi_D(x,y)=x, \pi_E(x,y)=y są funkcjami ciągłymi.
  • Jeśli Z jest dowolnym dcpo, a funkcje f\colon Z\to D oraz g\colon Z\to E są ciągłe, to funkcja \langle f, g\rangle \colon Z\to D\times E definiowana jako:
\forall z\in Z\  \langle f,g\rangle (z) = (f(z), g(z))

jest ciągła.

Dowód

Po pierwsze, zauważmy, że relacja po współrzędnych jest częściowym porządkiem; dowód jest elementarny, więc go pomijamy. Po drugie, pokażemy, że suprema zbiorów skierowanych w produkcie można liczyć po współrzędnych: niech F\subseteq D\times E będzie zbiorem skierowanym. Z definicji porządku na produkcie wynika, że projekcje \pi_D[F], \pi_E[F] są zbiorami skierowanymi. Pokażemy, że:
\bigvee{}^\downarrow F =(\bigvee{}^\downarrow\pi_D[F],\bigvee{}^\downarrow \pi_E[F])\ \ \ \ (dir)

Niech bowiem F\sqsubseteq (x,y) dla pewnego (x,y)\in D\times E. Wówczas z definicji porządku na produkcie mamy, że \pi_D[F]\sqsubseteq x oraz \pi_E[F]\sqsubseteq y, co daje \bigvee{}^\downarrow \pi_D[F]\sqsubseteq x oraz \bigvee{}^\downarrow \pi_E[F]\sqsubseteq y. A zatem, F\sqsubseteq (\bigvee{}^\downarrow  \pi_D[F],\bigvee{}^\downarrow \pi_E[F])\sqsubseteq (x,y). To dowodzi, że supremum \bigvee{}^\downarrow F istnieje i jest równe (\bigvee{}^\downarrow  \pi_D[F],\bigvee{}^\downarrow \pi_E[F]), co należało pokazać.

Zauważmy, że równość (dir) implikuje, że dla zbiorów skierowanych A\subseteq^{\uparrow} D i B\subseteq^{\uparrow} E mamy:

\bigvee{}^\downarrow A\times B = (\bigvee{}^\downarrow A,\bigvee{}^\downarrow B).\ \ \ \ (dir')

Część (2) twierdzenia jest trywialna. Aby udowodnić (3), zauważmy, że jeśli F jest zbiorem skierowanym w D\times E, to:

\pi_D(\bigvee{}^\downarrow  F)=\pi_D(\bigvee{}^\downarrow \pi_D[F],\bigvee{}^\downarrow  \pi_E[F]) = \bigvee{}^\downarrow \pi_D[F].

Analogiczny dowód można przeprowadzić dla funkcji \pi_E.

Dla (4), załóżmy, że Z jest dcpo i niech f\colon Z\to D oraz g\colon Z\to E będą funkcjami ciągłymi. Ponadto niech G będzie skierowanym podzbiorem Z. Wówczas:

\aligned   \langle f,g\rangle (\bigvee{}^\downarrow G)    & = & (f(\bigvee{}^\downarrow G), g(\bigvee{}^\downarrow G)) \\    & = & (\bigvee{}^\downarrow f[G], \bigvee{}^\downarrow g[G])\\    & = & (\bigvee{}^\downarrow_{r\in G} f(r), \bigvee{}^\downarrow_{s\in G} g(s))\\    & = & \bigvee{}^\downarrow_{(r,s)\in G\times G} (f(r), g(s))\\    & = & \bigvee{}^\downarrow_{(r,r)\in G\times G} (f(r), g(r))\\    & = & \bigvee{}^\downarrow_{r\in G} (f(r), g(r))\\    & = & \bigvee{}^\downarrow_{r\in G}  \langle f, g\rangle(r)\\    & = & \bigvee{}^\downarrow  \langle f, g\rangle [G]. \endaligned
image:End_of_proof.gif

W dowodzie korzystaliśmy kolejno z: definicji funkcji parującej, ciągłości funkcji f i g, definicji obrazu, równości (dir'), faktu, że zbiór \{(r,r)\mid r\in G\} jest skierowany i współkońcowy w zbiorze skierowanym G\times G (a więc ma to samo supremum), prostej własności zbiorów, definicji funkcji parującej i definicji obrazu.

Zanim przejdziemy do dyskusji przestrzeni funkcyjnej potrzebny nam będzie następujący lemat:


Lemat 13.2

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.


Twierdzenie 13.3 [Eksponent dcpo]

Niech D,E będą dcpo. Wówczas:
  • Zbiór funkcji ciągłych [D, E] wraz z relacją
f\sqsubseteq g\iff \forall x\in D\  f(x)\sqsubseteq  g(x)

jest dcpo.

  • Funkcja ewaluacji ev\colon [D, E]\times D\to E definiowana jako:
ev(f, x) = f(x)
dla każdej f\in [D, E] oraz x\in D, jest funkcją ciągłą.

Dowód

Ponieważ relacja \sqsubseteq w zbiorze funkcji jest zdefiniowana poprzez odwołanie do częściowego porządku w E, jest również częściowym porządkiem.

Dla dowodu (1) załóżmy, że F jest skierowanym podzbiorem funkcji ciągłych z D do E. Pokażemy, że funkcja g\colon D\to E zdefiniowana jako:

\forall x\in D\  g(x) = \bigvee{}^\downarrow_{f\in  F} f(x)

jest funkcją ciągłą (jest oczywiste, że g jest supremum F). Niech A\subseteq^{\uparrow}  D będzie skierowany. Mamy:

\aligned   g(\bigvee{}^\downarrow A) & = & \bigvee{}^\downarrow_{f\in F} f(\bigvee{}^\downarrow A)\\                & = & \bigvee{}^\downarrow_{f\in F}\bigvee{}^\downarrow_{a\in A} f(a)\\                & = & \bigvee{}^\downarrow_{a\in A}\bigvee{}^\downarrow_{f\in F} f(a)\\                & = & \bigvee{}^\downarrow_{a\in A} g(a)\\                & = & \bigvee{}^\downarrow g[A]. \endaligned
Dla dowodu (2), zauważmy, że ewaluacja jest ciągła ze względu na pierwszy argument: dla G\subseteqdir [D\to E] i x\in D mamy ev(\bigvee{}^\downarrow G,  x) = (\bigvee{}^\downarrow G)(x) =  \bigvee{}^\downarrow_{g\in G} g(x)=  \bigvee{}^\downarrow_{g\in G} ev(g,x). Ciągłości ze względu na drugi argument dowodzi się równie łatwo: dla A\subseteqdir D oraz f\in [D\to E] mamy ev(f, \bigvee{}^\downarrow A) =  f(\bigvee{}^\downarrow A) = \bigvee{}^\downarrow_{a\in A} f(a) =  \bigvee{}^\downarrow_{a\in A} ev(f,a). A zatem z Lematu 13.2 wynika, że ewaluacja jest funkcją ciągłą. image:End_of_proof.gif

Oczywiście elementem najmniejszym każdego eksponentu jest funkcja stała o wartości \bot.

Pozostaje nam wykazać, że produkt, jaki zaproponowaliśmy w Twierdzeniu 13.1 jest produktem kategoryjnym (granicą), podobnie - powinniśmy przekonać się, że przestrzeń funkcyjna, opisana pośrednio w Twierdzeniu 13.3, jest eksponentem. Ale obydwa dowody są analogiczne, jak w \mathbf{Set}, więc tutaj już kończymy dowód kartezjańskiej zamkniętości \mathbf{Dcpo} i \mathbf{Dcpo}_{\bot}.

Dziedziny bc-zupełne

Wiemy już, że zarówno produkt, jak i przestrzeń funkcyjna istnieją w kategoriach \mathbf{Dcpo} i \mathbf{Dcpo}_{\bot}. W szczególności oznacza to, że jeśli D i E są dziedzinami bc-zupełnymi, to produkt i przestrzeń funkcji są dcpo. Czy są one jednak bc-zupełne? Na to dość trudne pytanie odpowiemy poniżej. Pierwszy z dowodów nie nastręcza trudności, patrz Zadanie 13.4:


Twierdzenie 13.4 [Produkt dziedzin bc-zupełnych]

Niech D, E będą dziedzinami bc-zupełnymi. Wówczas produkt D\times E jest dziedziną bc-zupełną.


Tenże produkt jest oczywiście produktem kategoryjnym (dowód taki sam, jak dla \mathbf{Set}).

Niech D, E będą posetami ciągłymi i załóżmy, że E posiada element najmniejszy \bot. Niech a\in D i b\in E. Zdefiniujmy funkcję oznaczaną (a\searrow b)\colon D\to E poprzez:

(a\searrow b)(x) = \begin{cases}     b, &  a\ll x,\\     \bot, & \text{w przeciwnym przypadku}.   \end{cases}

Funkcje tej postaci nazywamy funkcjami prostymi. Dowód poniższego lematu znajduje się w Zadaniu 13.5.


Lemat 13.5 [Funkcje proste]

Funkcje proste są ciągłe.

Aby pokazać, że jeśli D, E są dziedzinami bc-zupełnymi, to [D, E] jest dziedziną bc-zupełną, musimy najpierw udowodnić kilka pomocniczych własności.


{{lemat|13.6|mod13:lemma:tech1| Jeśli f\in [D, E] oraz y\ll f(x) dla pewnych elementów x\in D i y\in E, to mamy (x\searrow y)\ll f w [D, E].

Dowód

Niech G \subseteq^{\uparrowarrow} [D,  E] będzie podzbiorem skierowanym takim, że \bigvee{}^{\uparrowarrow} G\sqsupseteq f. Z założenia wynika, że y\sqsubseteq g(x) dla pewnego g\in G. Niech z\in D będzie dowolnym elementem. Jeśli x\ll z, to (x\searrow y) (z) = y\sqsubseteq  g(x)\sqsubseteq g(z). W przeciwnym wypadku (x\searrow y)(z)=\bot\sqsubseteq g(z). A zatem (x\searrow y)\sqsubseteq g, co należało pokazać. image:End_of_proof.gif


{{lemat|13.7|mod13:lemma:tech2| Jeśli D i E są posetami bc-zupełnymi i E jest dcpo, to [D,E] jest posetem bc-zupełnym.

Dowód

Pokażemy, że każde dwie funkcje z [D, E] wspólnie ograniczone z góry posiadają supremum. Załóżmy, że g,h\sqsubseteq f. To znaczy, że dla każdego z\in D mamy g(z),h(z)\sqsubseteq f(z). Skoro E jest bc-zupełny, g(z)\vee h(z) istnieje dla każdego z\in D. Zdefiniujmy więc funkcję g\vee h\colon D\to E w następujący sposób:
\forall z\in D\  (g\vee h)(z) = g(z)\vee h(z).
Funkcja ta jest ciągła i jest oczywiste, że jest ona supremum funkcji g i h. Z dowolności wyboru funkcji f,g,h wynika teza lematu. image:End_of_proof.gif

Dowód ciągłości przestrzeni funkcyjnej będzie polegał na tym, że pokażemy, iż funkcje będące skończonymi supremami funkcji prostych tworzą bazę.


Twierdzenie 13.8 [Eksponent dla dziedzin bc-zupełnych]

Niech D, E będą dziedzinami bc-zupełnymi. Wówczas [D, E] jest dziedziną bc-zupełną. Jest to eksponent w kategorii dziedzin bc-zupełnych.

Dowód

Niech f\colon D\to E będzie dowolną funkcją ciągłą. Niech x\in D i y\in E. Rozważmy zbiór:
A_f = \{(x\searrow y)\mid y\ll  f(x)\}.

(Zauważmy, że zbiór A nie jest w ogólności skierowany.) Pokażemy najpierw, że zachodzi:

f = \bigvee A_f.

Z Lematu 13.6 wynika, że funkcja f jest ograniczeniem górnym A_f, bo jeśli (x\searrow y)\in A_f, to y\ll f(x), a zatem (x\searrow y)\ll f, co implikuje (x\searrow y)\sqsubseteq f. Niech g\in [D\to E] będzie dowolnym innym ograniczeniem zbioru A_f. Załóżmy, że z\in D. Aby wykazać, że f(z)\sqsubseteq g(z), wystarczy pokazać, iż:

\forall w\in E\  (w\ll f(z)\Rightarrow w\sqsubseteq  g(z)).

Niech w\in E będzie dowolnym elementem takim, że w\ll f(z). Skoro \uup w jest zbiorem otwartym i \bigvee{}^\downarrow f[\ddn z] = f(z)\in \uup  w, to musi istnieć v\ll z taki, że w\ll  f(v). Wówczas (v\searrow w)\in A_f oraz w=(v \searrow w)(z) \sqsubseteq g(z). Wnioskujemy więc, że f\sqsubseteq g. Z dowolności funkcji g wnioskujemy, że f jest najmniejszym ograniczeniem górnym zbioru A_f, co dowodzi równości (*).

Niech B_f będzie zbiorem wszystkich skończonych supremów elementów z A_f, to znaczy supremów skończonych funkcji prostych aproksymujących f. Zauważmy, że zbiór B_f jest poprawnie określony, co wynika z Lematu 13.7. Co więcej, każda funkcja z B_f aproksymuje funkcję f (przypomnijmy, że zdanie k,l\ll  r\Rightarrow k\vee l\ll r, kiedykolwiek k\vee  l istnieje, jest prawdziwe w dowolnym posecie ciągłym!). A zatem B_f\subseteq \ddn f, co daje w szczególności B_f\cap \ddn f = B_f. Zauważmy w końcu, że B_f jest zbiorem skierowanym, a więc supremum B_f istnieje, gdyż [D,E] jest dcpo, co wynika z Twierdzenia 13.3. Skoro zaś A_f\subseteq B_f, to f=\bigvee  A_f\sqsubseteq \bigvee{}^\downarrow (B_f\cap \ddn f) =  \bigvee{}^\downarrow B_f\sqsubseteq f. A zatem, f=  \bigvee{}^\downarrow (B_f\cap \ddn f). To znaczy, że rodzina:

\beta = \bigcup \{B_f\mid f\in [D,E]\}
jest bazą dla [D,E], a więc poset [D,E] jest ciągły. A zatem [D\to E] jest dziedziną bc-zupełną. image:End_of_proof.gif