SW wykład 4 - Slajd12
Semantyka denotacyjna Dziedziny składniowe i semantyczne Funkcje semantyczne Kompozycjonalność Tiny. Semantyka denotacyjna Tiny. Semantyka denotacyjna, c.d. Pojęcia pomocnicze Pojęcia pomocnicze, c.d. |Tiny. Semantyka denotacyjna, c.d. Tiny. Semantyka denotacyjna, c.d. Problem z while Konstrukcje stałopunktowe Konstrukcje stałopunktowe, c.d. Konstrukcje stałopunktowe, c.d. Przykład Przykład, c.d. Dowód Dowód Zgodność semantyki denotacyjnej
Klauzula określająca znaczenie pętli jest więc równaniem stałopunktowym (w dziedzinie semantycznej dla instrukcji, czyli w dziedzinie funkcji częściowych ze stanów w stany).
Równania stałopunktowe sprawiają jednak przynajmniej dwa podstawowe problemy.
Po pierwsze, nie każdy operator ma jakikolwiek punkt stały. Przykładowy operator na slajdzie, który dowolnej funkcji częściowej przyporządkowuje funkcję z pewnością od niej różną (bo dla dowolnego stanu, jeśli wartość funkcji będącej argumentem jest nieokreślona, to wartość wyniku operatora na tym stanie jest określona, a w przeciwnym przypadku wartość ta też jest określona, ale różna od wartości argumentu na tym stanie), oczywiście nie ma żadnego punktu stałego. Musimy więc jakoś zapewnić, że z takimi operatorami nie będziemy mieli do czynienia i precyzyjnie opisać własność rozważanych operatorów, która zapewni istnienie dla nich (przynajmniej jednego) punktu stałego.
Po drugie zaś, istnieją operatory, które mają wiele punktów stałych. Najprostszy przykład to operator identycznościowy, dla którego każda funkcja ze stanów w stany jest punktem stałym. Inny przykład na slajdzie to operator, którego jednym z punktów stałych jest funkcja zawsze nieokreślona, a drugim funkcja, która modyfikuje dowolny stan przez przypisanie wskazanej zmiennej zera. Który z punktów stałych danego operatora powinniśmy jakoś wskazać jako definiowaną równaniem stałopunktowym wartość? Poszukamy jednolitej metody wskazania "właściwego" punktu stałego dla praktycznie nas interesującej (na potrzeby semantyki denotacyjnej) klasy operatorów.
