SW wykład 4 - Slajd17

<<powrót do strony wykładu

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

Pozostał nam jeszcze dowód, że obliczenie instrukcji pętli w pewnym stanie początkowym prowadzi do stanu końcowego, wtedy i tylko wtedy, gdy jedna z iteracji związanego z pętlą operatora na funkcji pustej dla tego stanu daje w wyniku tenże stan końcowy.

Zacznijmy od implikacji, która mówi, że jeśli dla pewnego stanu początkowego obliczenie instrukcji pętli prowadzi do stanu końcowego, to któraś z iteracji związanego z tą pętlą operatora na funkcji pustej dla tego stanu początkowego jako argumentu daje wynik, który jest stanem końcowym tego obliczenia. Korzystać będziemy z założenia, że jeśli dla pewnego stanu początkowego obliczenie ciała pętli prowadzi do stanu końcowego, to znaczenie ciała pętli jest funkcją, która dla tego stanu początkowego daje w wyniku stan końcowy tego obliczenia.

Dowód przebiega przez indukcję względem długości obliczenia pętli. Zauważmy, że obliczenie puste nie może spełniać przesłanki implikacji. Możemy więc przyjąć, że interesujące nas obliczenie ma dodatnią długość. Rozważamy dwa przypadki.

Po pierwsze, przypuśćmy, że wartością warunku pętli w stanie początkowym jest fałsz. Wtedy obliczenie pętli ma długość jeden i stanem końcowym jest po prostu stan początkowy. Ale wówczas także pierwsza iteracja operatora na tymże stanie początkowym jest określona i daje w wyniku ten sam stan --- co kończy dowód w tym przypadku.

Rozważmy przypadek przeciwny, gdy wartością warunku pętli w stanie początkowym jest prawda. Wówczas pierwszy krok obliczenia prowadzi do konfiguracji, w której w tym samym stanie początkowym mamy wykonać najpierw ciało pętli, a następnie znów całą pętlę. Z faktu o obliczeniach dla sekwencyjnego złożenia instrukcji (patrz slajd 23 wykładu o semantyce operacyjnej) wynika, że prowadzące od tej konfiguracji do stanu końcowego obliczenie można "rozbić" na dwa krótsze obliczenia: obliczenie ciała pętli w stanie początkowym prowadzące do pewnego stanu pośredniego oraz obliczenie całej pętli w tym stanie pośrednim, prowadzące do wskazanego wcześniej stanu końcowego. A przy tym obliczenia te (w szczególności drugie z nich) są krótsze niż rozważane od początku obliczenie pętli w stanie początkowym. Z założenia, to pierwsze obliczenie pokazuje, że znaczenie ciała pętli dla stanu początkowego daje w wyniku wskazany stan pośredni. Z kolei, na mocy założenia indukcyjnego, drugie z tych obliczeń pokazuje, że dla tego stanu pośredniego pewna iteracja operatora na funkcji pustej daje w wyniku stan końcowy. Teraz już łatwo sprawdzić, że dla naszego stanu początkowego następna iteracja operatora na funkcji pustej da jako wynik stan końcowy całego obliczenia.

Kończy to dowód tej implikacji.