SW wykład 9 - Slajd10

<<powrót do strony wykładu

Dziedziny podstawowe Suma i produkt Suma spłaszczona i produkt spłaszczony Przestrzeń funkcji ciągłych Izomorfizm dziedzin Konstruowanie funkcji ciągłych Złożenie funkcji i indeksowanie Inne konstrukcje Operator punktu stałego Równania stałopunktowe Równania dziedzinowe Rekurencyjne równania dziedzinowe Rekurencyjne równania dziedzinowe Problemy Dziedziny refleksywne Rozwiązanie naiwne dziedziny Scotta

Skoro zgodnie z argumentacją na poprzednich slajdach, wszystkie definiowane przez nas funkcje (też funkcje wyższego rzędu) są funkcjami ciągłymi na zbiorach łańcuchowo zupełnych, to każde równanie stałopunktowe, które może się pojawić w naszych definicjach semantyki języków programowania, ma najmniejsze rozwiązanie --- i to właśnie najmniejsze rozwiązanie przyjmujemy za definiowane znaczenie.

Oczywiście, zależności pomiędzy definiowanymi znaczeniami są niekiedy z pozoru zawikłane bardziej, niż w ramach jednego równania stałopunktowego. Mamy wówczas do czynienia z układem równań stałopunktowych. Każdy taki układ można zapisać w podanej na slajdzie postaci. Z kolei łatwo widać, że odpowiada on jednemu równaniu stałopunktowemu w odpowiednim produkcie zbiorów łańcuchowo zupełnych. Najmniejsze rozwiązanie tego równania to wektor elementów stanowiących najmniejsze rozwiązanie rozważanego układu równań stałopunktowych. Zatem możliwość jednoznacznego rozwiązywania dowolnych równań stałopunktowych pozwala nam też na dowolne posługiwanie się układami takich równań.