SW wykład 3 - Slajd12

<<powrót do strony wykładu

Semantyka naturalna Semantyka naturalna Tiny Sens definicji Sens definicji, c.d. Dowody Indukcja po strukturze Własności Równoważność semantyczna Kongruencje Semantyka operacyjna a naturalna Semantyka operacyjna a naturalna, c.d. Semantyka operacyjna a naturalna, c.d. Semantyka "denotacyjna" Semantyka operacyjna a naturalna, c.d. Równoważność operacyjna Niedeterminizm Kilka równoważności Równoległość

Teraz implikacja przeciwna: jeśli w semantyce operacyjnej istnieje obliczenie prowadzące od pewnej konfiguracji do stanu końcowego, to w semantyce naturalnej mamy przejście od tej konfiguracji do tegoż stanu końcowego. Dowód przebiega przez indukcję względem długości obliczenia, o którym mowa w założeniu implikacji.

Zauważmy, że obliczenie to nie może być puste. Dowód prowadzimy teraz przez przypadki względem pierwszego kroku obliczenia, w zależności od postaci instrukcji zawartej w początkowej konfiguracji. Dowody dla kilku przykładowych przypadków przedstawiamy powyżej na slajdzie. Pozostałe przypadki pomijamy, zachęcając do odtworzenia dla nich dowodów, analogicznych do podanych tutaj dla wybranych typowych przypadków.