SW wykład 4 - Slajd14
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
Nieformalnie, obliczenia dla instrukcji pętli można powiązać z iterowaniem przez kolejne aplikacje określonego w klauzuli semantycznej dla tej pętli operatora na dziedzinie semantycznej dla instrukcji, rozpoczynając od zawsze nieokreślonej funkcji pustej. Iteracje te formalnie definiujemy w dość oczywisty sposób: iteracja zerowa to zawsze funkcja (częściowa, ze stanów w stany) o nieokreślonej wartości dla wszystkich argumentów, czyli funkcja pusta. Kolejna iteracja to po prostu aplikacja operatora do iteracji poprzedniej. Zatem, iteracja pierwsza określi funkcję, która da wynik dla tych stanów, dla których warunek pętli nie jest spełniony i ciało pętli nie musi być wykonywane ani razu. Iteracja druga dodatkowo da wynik dla stanów, dla których wykonanie pętli wymaga wykonania jej ciała dokładnie raz. Iteracja trzecia dołoży do tego wyniki dla stanów, w których wykonanie pętli wymaga wykonania jej ciała dwa razy. I tak dalej...
Stąd wniosek (oczywiście przy założeniu, że znaczenie ciała pętli jest w oczekiwany sposób związane z jego semantyką operacyjną), że obliczenie ciała pętli w pewnym stanie prowadzi do stanu końcowego, wtedy i tylko wtedy, gdy jedna (a wtedy też wszystkie kolejne) z iteracji związanego z pętlą operatora na funkcji pustej dla tego stanu daje w wyniku tenże stan końcowy. Formalny dowód tej własności poniżej.
Inny wniosek z tej własności pozwala na określenie poszukiwanego punktu stałego tego operatora właśnie jako sumy (teoriomnogościowej) jego kolejnych iteracji na funkcji pustej. Formalne uzasadnienie, że jest to rzeczywiście punkt stały tego operatora i co więcej, jest to jego najmniejszy punkt stały (względem inkluzji funkcji częściowych jako zbiorów par "argument-wynik") podamy na jednym z kolejnych wykładów tych zajęć (patrz wykład o punktach stałych w porządkach zupełnych).
Dla potrzeb zrozumienia i definiowania semantyki denotacyjnej języka TINY i rozważanych dalej jego rozszerzeń na razie wystarczą powyższe intuicyjne rozważania o semantyce instrukcji pętli, uzupełnione formalną analizą odpowiadającej tej konstrukcji językowej klauzuli semantycznej zadanej równaniem stałopunktowym. Przenoszą się one także na bardziej złożone sytuacje, gdzie będziemy mieli do czynienia z podobnymi stałopunktowymi definicjami znaczeń dla innych ("iteracyjnych" lub "rekurencyjnych") konstrukcji językowych.
