SW wykład 3 - Slajd15

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

Zaczniemy od definicji równoważności instrukcji indukowanej przez semantykę operacyjną.

Rozważmy dwie instrukcje i dowolny stan. Wymaganie, by semantyka operacyjna dla konfiguracji zawierającej odpowiednio każdą z tych instrukcji i rozważany stan generowała te same obliczenia, okazuje się zbyt mocne w praktyce: tylko nieliczne pary instrukcji byłyby względem takiej definicji równoważne. Problemem jest zbyt mocne wymaganie tożsamości obliczeń. Przyjmiemy nieco luźniejszą definicję, wymagającą jedynie by generowane obliczenia były w pewnym sensie równoważne. Podana na slajdzie formalna definicja bipodobieństwa konfiguracji określa w istocie równoważność rozpoczynających się od takich konfiguracji obliczeń. Jest to jedna z wersji ważnego pojęcia bisymulacji procesów.

Łatwo teraz pokazać, że tak zdefiniowana równoważność instrukcji względem semantyki operacyjnej implikuje ich naturalną równoważność zdefiniowaną wcześniej względem semantyki naturalnej. Okazuje się przy tym, że te dwie równoważności są tożsame dla dotychczas rozważanego języka instrukcji.