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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania

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.


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. , albo rekursywna, np.:

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ę ; 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

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 opisującą wszystkie sytuacje, gdy wyrażenie redukuje się do wartości (wartości to wyrażenia, które nie mogą być już uproszczone). Na przykład, jeśli jest wyrażeniem typu boolowskiego, to opisuje sytuację, gdy przyjmuje wartość .

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

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

     (*)

dla wszystkich kontekstów i wszystkich wartości . (w tej chwili wystarczy wiedzieć, że o kontekstach można myśleć jako o testach jakim poddajemy programy , ). 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 i kontekstów. Dlatego wprowadza się również trzeci styl semantyki, zwany semantyką denotacyjną.

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

Obiekt jest nazywany również znaczeniem, semantyką, obiektem semantycznym i jest elementem pewnego zbioru 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:

  • - zbiór wyrażeń boolowskich (oznaczanych metazmienną ),
  • - zbiór prymitywnych komend (oznaczanych metazmienną ),
  • - zbiór zdań (oznaczanych metazmienną ) dany przez następującą gramatykę:

OBIEKTY SEMANTYCZNE (DZIEDZINY):

  • - zbiór wartości logicznych (oznaczanych metazmienną ),
  • - zbiór stanów programu (oznaczanych metazmienną ),
  • - zbiór komend (oznaczanych metazmienną ).


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 .

  • jest zadana z góry,
  • jest zadana z góry,
  • jest zdefiniowana za pomocą dwóch poprzednich funkcji zgodnie z wymogiem składalności, jak następuje:
  • ,
  • ,
  • , gdzie funkcja jest dana jako:

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:

Oczekujemy, że semantyka pętli będzie taka sama jak semantyka frazy:

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

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

W szczególnym przypadku, jeśli i , to:

czyli może być dowolną funkcją! To przeczy jednak naszej intuicji, gdyż oczekiwalibyśmy, że w tym wypadku funkcja powinna być po prostu niezdefiniowana. Innymi słowy, oczekujemy, że funkcje takie jak 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 jest równoważna funkcji totalnej , gdzie jest sumą prostą zbioru i elementu nienależącego do . Zdanie jest interpretowane jako stwierdzenie, że funkcja przyjmuje dla argumentu wartość niezdefiniowaną (znak 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 oznaczający wartość niezdefiniowaną. Interpretacja elementu sugeruje również, że dowolna funkcja pomiędzy dziedzinami powinna spełniać .

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 . Definiując częściowy porządek na poprzez:

widzimy, że warunek jest równoważny stwierdzeniu, że funkcja jest monotoniczna. Porządek na dziedzinie oznaczamy i definiujemy analogicznie. Podobnie dla innych dziedzin. Tak naprawdę każdy zbiór może być zmieniony na poset (gdzie ) poprzez:

     (eq:flat)

Konsekwentnie, funkcja omawiana powyżej typu i jest zdefiniowana jako:

Ł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ść

pokazuje, że:

     (fix)

dla pewnej funkcji zależnej od semantyki i . Konkretnie:

gdzie jest funkcją identycznościową na . Równość (fix) oznacza, że znaczenie pętli jest niczym innym, tylko punktem stałym funkcji typu . 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 liczb całkowitych ujemnych z porządkiem naturalnym, poset 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 (dcpo z funkcjami ciągłymi), - dcpo z elementami najmniejszymi plus funkcje ciągłe oraz (-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 ().

Twierdzenie 13.1 [Produkt dcpo]

Niech będą dcpo. Mamy:
  • Zbiór z porządkiem po współrzędnych

jest dcpo.

  • Jeśli i posiadają elementy najmniejsze, to ma element najmniejszy .
  • Projekcje i dane odpowiednio przez , są funkcjami ciągłymi.
  • Jeśli jest dowolnym dcpo, a funkcje oraz są ciągłe, to funkcja definiowana jako:

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 będzie zbiorem skierowanym. Z definicji porządku na produkcie wynika, że projekcje , są zbiorami skierowanymi. Pokażemy, że:

Niech bowiem dla pewnego . Wówczas z definicji porządku na produkcie mamy, że oraz , co daje oraz . A zatem, . To dowodzi, że supremum istnieje i jest równe , co należało pokazać.

Zauważmy, że równość (dir) implikuje, że dla zbiorów skierowanych i mamy:

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

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

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

End of proof.gif

W dowodzie korzystaliśmy kolejno z: definicji funkcji parującej, ciągłości funkcji i , definicji obrazu, równości (dir'), faktu, że zbiór jest skierowany i współkońcowy w zbiorze skierowanym (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 będą dcpo oraz będzie funkcją dwóch argumentów. Funkcja 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 będą dcpo. Wówczas:
  • Zbiór funkcji ciągłych wraz z relacją

jest dcpo.

  • Funkcja ewaluacji definiowana jako:
dla każdej oraz , jest funkcją ciągłą.

Dowód

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

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

jest funkcją ciągłą (jest oczywiste, że jest supremum ). Niech będzie skierowany. Mamy:

Dla dowodu (2), zauważmy, że ewaluacja jest ciągła ze względu na pierwszy argument: dla i mamy Ciągłości ze względu na drugi argument dowodzi się równie łatwo: dla oraz mamy A zatem z Lematu 13.2 wynika, że ewaluacja jest funkcją ciągłą. End of proof.gif

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

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 , więc tutaj już kończymy dowód kartezjańskiej zamkniętości i .

Dziedziny bc-zupełne

Wiemy już, że zarówno produkt, jak i przestrzeń funkcyjna istnieją w kategoriach i . W szczególności oznacza to, że jeśli i 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 , będą dziedzinami bc-zupełnymi. Wówczas produkt jest dziedziną bc-zupełną.


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

Niech , będą posetami ciągłymi i załóżmy, że posiada element najmniejszy . Niech i . Zdefiniujmy funkcję oznaczaną poprzez:

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 , są dziedzinami bc-zupełnymi, to jest dziedziną bc-zupełną, musimy najpierw udowodnić kilka pomocniczych własności.


{{lemat|13.6|mod13:lemma:tech1| Jeśli oraz dla pewnych elementów i , to mamy w .

Dowód

Niech będzie podzbiorem skierowanym takim, że . Z założenia wynika, że dla pewnego . Niech będzie dowolnym elementem. Jeśli , to . W przeciwnym wypadku . A zatem , co należało pokazać. End of proof.gif


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

Dowód

Pokażemy, że każde dwie funkcje z wspólnie ograniczone z góry posiadają supremum. Załóżmy, że . To znaczy, że dla każdego mamy . Skoro jest bc-zupełny, istnieje dla każdego . Zdefiniujmy więc funkcję w następujący sposób:
Funkcja ta jest ciągła i jest oczywiste, że jest ona supremum funkcji i . Z dowolności wyboru funkcji wynika teza lematu. 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 , będą dziedzinami bc-zupełnymi. Wówczas jest dziedziną bc-zupełną. Jest to eksponent w kategorii dziedzin bc-zupełnych.

Dowód

Niech będzie dowolną funkcją ciągłą. Niech i . Rozważmy zbiór:

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

Z Lematu 13.6 wynika, że funkcja jest ograniczeniem górnym , bo jeśli , to , a zatem , co implikuje . Niech będzie dowolnym innym ograniczeniem zbioru . Załóżmy, że . Aby wykazać, że , wystarczy pokazać, iż:

Niech będzie dowolnym elementem takim, że . Skoro jest zbiorem otwartym i , to musi istnieć taki, że . Wówczas oraz . Wnioskujemy więc, że . Z dowolności funkcji wnioskujemy, że jest najmniejszym ograniczeniem górnym zbioru , co dowodzi równości (*).

Niech będzie zbiorem wszystkich skończonych supremów elementów z , to znaczy supremów skończonych funkcji prostych aproksymujących . Zauważmy, że zbiór jest poprawnie określony, co wynika z Lematu 13.7. Co więcej, każda funkcja z aproksymuje funkcję (przypomnijmy, że zdanie , kiedykolwiek istnieje, jest prawdziwe w dowolnym posecie ciągłym!). A zatem , co daje w szczególności . Zauważmy w końcu, że jest zbiorem skierowanym, a więc supremum istnieje, gdyż jest dcpo, co wynika z Twierdzenia 13.3. Skoro zaś , to . A zatem, . To znaczy, że rodzina:

jest bazą dla , a więc poset jest ciągły. A zatem jest dziedziną bc-zupełną. End of proof.gif