SW wykład 3 - Slajd17

<<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ść

Wprowadzenie tych dodatkowych konstrukcji językowych podkreśla różnicę między semantyką operacyjną i naturalną. W szczególności, równoważność instrukcji względem semantyki operacyjnej nadal implikuje ich równoważność względem semantyki naturalnej --- ale implikacja przeciwna już na ogół nie zachodzi. Równoważność względem semantyki naturalnej utożsamia bowiem instrukcje różniące się jedynie dodatkowymi ścieżkami obliczeń, prowadzącymi do zakleszczenia --- a zdefiniowana wyżej bisymulacyjna równoważność względem semantyki operacyjnej na ogół instrukcje takie pozwala od siebie odróżnić. Podobnie: ta druga równoważność rozróżnia instrukcje różniące się od siebie "miejscem" niedeterministycznego wyboru, podczas gdy semantyka naturalna i definiowana przez nią równoważność takie różnice pomija.