SW wykład 8 - Slajd8
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
Podamy jeszcze dwa proste fakty, które pozwolą nam na dowodzenie własności najmniejszych punktów stałych funkcji ciągłych, o których istnieniu przekonaliśmy sie właśnie powyżej.
Po pierwsze, jeśli znajdziemy element taki, że wynik funkcji na nim jest elementem w relacji porządku z nim samym (element taki czasem określa się jako "pre-punkt stały" funkcji), to najmniejszy punkt stały jest z nim w relacji porządku. Prosty dowód pomijamy (można sprawdzić, że na przykład przenosi się tu dowód faktu, że kres górny łańcucha iteracji funkcji na elemencie najmniejszym jest w relacji z każdym punktem stałym funkcji).
Drugi fakt jest nieco bardziej skomplikowany do sformułowania, ale też i bardziej przydatny w praktyce.
Własność elementów zbioru łańcuchowo zupełnego nazwiemy dopuszczalną, jeśli spełnia ją element najmniejszy tego zbioru i jest ona zamknięta na kresy górne przeliczalnych łańcuchów w tym zbiorze.
Teraz: dla każdej funkcji ciągłej z tego zbioru z niego samego, każda dopuszczalna własność zamknięta ze względu na aplikacje tej funkcji, zachodzi dla jej najmniejszego punktu stałego.
Przykładowy dowód: element najmniejszy spełnia tę własność z założenia o jej dopuszczalności. Przez indukcję można więc pokazać, że kolejne iteracje tej funkcji na elemencie najmniejszym też tę własność spełniają (bo jest ona zamknięta ze względu na aplikacje funkcji). Zatem, znów z dopuszczalności tej własności, najmniejszy punkt stały tej funkcji z tym zbiorze, jako kres górny łańcucha tych iteracji, spełnia tę własność.
