SW wykład 8 - Slajd6
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
I w końcu, jako ostatni i najbardziej bezpośrednio związany z tymi zajęciami przykład, przypomnijmy "obliczeniowe" motywacje wprowadzenie zbiorów łancuchowo zupełnych, rozważając raz jeszcze zbiór łańcuchowo zupełny funkcji częściowych pomiędzy dwoma ustalonymi zbiorami.
Porządek na tych funkcjach określamy przez inkluzję ich grafów (jako relacji). Zwróćmy uwagę, że przy przedstawionej wyżej "informacyjnej" intuicji, daną funkcję częściową należy rozumieć jako informację o pewnej, aproksymowanej przez nią funkcji --- albo jako własność pewnego zbioru funkcji. Jeśli dana funkcja jest określona na jakimś argumencie, to jest to jednoznaczna, pozytywna informacji, która mówi, że aproksymowane przez nią funkcje też są na tym argumencie określone i dają wskazany wynik. Jeśli jednak funkcja na jakimś argumencie nie ma określonej wartości, to należy to rozumieć jako stwierdzenie: "nie wiem, jaka jest wartość funkcji dla tego argumentu". Oznacza to, że podając dalsze informacje (na przykład, kontynuując proces obliczeń funkcji, którą aproksymujemy) wartość tę możemy jeszcze uzyskać. Jednocześnie, możemy nie być w stanie się upewnić, że z pewnością tego wyniku nie uzyskamy (bo to może wymagać nieskończonego obliczenia i spojrzenia na takie nieskończone obliczenia jako na całość --- niejako, po "pozaskończonym zakończeniu" tego nieskończonego obliczenia).
Mając skierowany, a zatem niesprzeczny zbiór takich informacji, zadanych jako funkcje częściowe, jego kresem górnym jest jego suma --- która też jest funkcją częściową.
Najciekawsze teraz pojęcia dotyczą operatorów z jednego zbioru funkcji częściowych z tak zadanym porządkiem w drugi. Operator taki jest monotoniczny, gdy bardziej określonej funkcji przypisuje nie mniej określoną funkcję. Ponieważ teraz każdą funkcję częściową (o przeliczalnej dziedzinie) możemy aproksymować przez zbiór skończonych funkcji częściowych, którego kresem jest dana funkcja, to operator taki jest ciągły, gdy jego wynik dla danej funkcji na każdym z argumentów zależy co najwyżej od skończonej liczby aplikacji tej funkcji do jej argumentów. Zatem, bardzo nieformalnie, typowe operatory, które ciągłe nie są, wymagać będą wartości swoich funkcyjnych argumentów na nieskończonym zbiorze --- na przykład testowanie, czy dana funkcja na liczbach naturalnych jest stała --- lub określać będą wynik w zależności od nieokreśloności swoich funkcyjnych argumentów --- na przykład testowanie, czy dana funkcja jest całkowita.
