SW wykład 8 - Slajd1
Częściowe porządki zupełne Przykłady Funkcje ciągłe Intuicje Intuicje, c.d. Przestrzeń funkcji częściowych Twierdzenie o punkcie stałym Techniki dowodowe Semantyka while
Przypomnijmy, że w ramach wykładu 4 (pierwszy z wykładów o semantyce denotacyjnej) analizowaliśmy dość starannie stałopunktową definicję semantyki instrukcji pętli. Pokazaliśmy, że zapisana w naturalny sposób klauzula semantyczna dla pętli jest równaniem stałopunktowym, które ma najmniejsze rozwiązanie, będące najmniejszym punktem stałym odpowiedniego operatora na funkcjach częściowych ze stanów w stany (czyli wówczas dziedzinie semantycznej dla instrukcji). Uzasadnialiśmy też, że ten właśnie najmniejszy punkt stały to rzeczywiście oczekiwane (i zgodne z semantyką operacyjną) znaczenie instrukcji pętli. W kolejnych wykładach jeszcze kilkakroć mieliśmy do czynienia z równaniami stałopunktowymi (lub układami równań stałopunktowych) --- zapewnialiśmy wówczas, że ich rozwiązywanie nie jest problemem, bo rzeczywiście, wszystkie układy równań, z którymi mieliśmy do czynienia, mają takie oczekiwane, "najmniejsze" rozwiązania.
W tym i w kolejnym wykładzie postaramy się to uzasadnić.
W każdym z rozważanych wyżej przypadków klauzul prowadzących do równań stałopunktowych, oczywiste jest wypisanie odpowiedniego operatora na dziedzinie znaczeń dla konstrukcji, które rozważamy, tak by punkty stałe tego operatora były potencjalnymi kandydatami na znaczenie danej konstrukcji. Zatem, najważniejsze pytanie, które pozwoli na uogólnienie analizy przeprowadzonej dla semantyki pętli, to pytanie o własności dziedziny funkcji częściowych ze stanów w stany i własności wyznaczonego klauzulą dla instrukcji pętli operatora, które zapewniły istnienie odpowiedniego, najmniejszego punktu stałego tego operatora.
Okazuje się, że odpowiedzi dostarcza teoria porządków, i można ją znaleźć już w pracach z połowy XX wieku (Kleene'ego, Tarskiego, i innych).
Przypomnijmy, że relacja (częściowego) porządku to każda binarna relacja na danym zbiorze, która jest zwrotna, przechodnia i antysymetryczna (ta ostatnia własność oznacza, że jeśli jest w relacji z i jest w relacji z , to ). Mając zbiór z relacją porządku i jego dowolny podzbiór, mówimy, że element jest najmniejszy w tym podzbiorze, gdy jest w tym podzbiorze i jest w relacji porządku z każdym elementem tego podzbioru. Element jest ograniczeniem górnym tego podzbioru, gdy każdy element tego podzbioru jest z nim w relacji porządku. I w końcu, element jest kresem górnym tego podzbioru, gdy jest najmniejszy w zbiorze jego górnych ograniczeń.
Zbiorem łańcuchowo zupełnym (cpo --- z angielskiego complete partial order) nazywamy zbiór z relacją częściowego porządku, z elementem najmniejszym w całym tym zbiorze, i taki, że każdy przeliczalny łańcuch w tym zbiorze ma kres górny (łańcuch to każdy podzbiór zawierający porównywalne ze sobą elementy: dla każdych elementów łańcucha, i , jest w relacji porządku z lub jest w relacji porządku z ).
Zauważmy, że podane na slajdzie wymaganie wydaje się nieco słabsze: wymagamy tam istnienia kresów górnych tylko dla przeliczalnych łańcuchów elementów, z których każdy jest w relacji porządku z następnym. Nie każdy przeliczalny łańcuch jest tej postaci (warto podać kontrprzykład) ale jeśli wszystkie łańcuchy tej postaci mają kres górny, to wszystkie łańcuchy przeliczalne mają kres górny. Okazuje się (zachęcamy do przeprowadzenia dowodu!), że wówczas także każdy przeliczalny zbiór skierowany ma kres górny --- podzbiór zbioru z relacją porządku jest skierowany, gdy każde dwa jego elementy mają w tym podzbiorze ograniczenie górne.
Uwaga: jednak podane przez nas wymaganie istnienia kresów górnych przeliczalnych łańcuchów (lub równoważnie: przeliczalnych zbiorów skierowanych) jest istotnie słabsze niż wymaganie istnienia kresów górnych wszystkich łańcuchów (lub równoważnie --- a ta równoważność już trywialna nie jest --- wszystkich zbiorów skierowanych). Przypomniwszy sobie wiadomości z teorii mnogości, łatwo podać przykład zbioru uporządkowanego, gdzie każdy łańcuch przeliczalny ma kres górny, ale istnieją nieprzeliczalne łańcuchy, które kresów górnych nie mają.
Jeszcze uwaga terminologiczno-notacyjna: najmniejszy element zbiorów skierowanych jest na ogól oznaczany tak, jak na slajdzie, a nazywany "denkiem" lub "pinezką", a czasem jeszcze elementem "nieokreślonym". Warto też zauważyć, że zgodnie z definicją, każdy element zbioru uporządkowanego jest ograniczeniem górnym zbioru pustego, a element najmniejszy w tym zbiorze uporządkowanym jest więc w nim kresem górnym zbioru pustego.
