SW wykład 3 - Slajd3

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

Oczywiście, implikacje opisane regułami na poprzednim slajdzie nie wyznaczają definiowanej tu relacji przejścia jednoznacznie: istnieje wiele relacji, które te implikacje spełniają (włącznie z zupełnie trywialną i wielce "niedeterministyczną" relacją wiążącą każdą konfigurację z każdym stanem jako jej konfiguracją końcową).

Jak zatem tę definicję należy rozumieć?

Zapewne najprostsze jest rozumienie "teoriomnogościowe": definiujemy tu najmniejszą relację między konfiguracjami i stanami, która spełnia zapisane jako reguły implikacje (w tym oczywiście implikacje "bez poprzedników").

Łatwo pokazać, że wykorzystywana tu postać reguł (nieformalnie: tylko "pozytywne" warunki wykorzystujące definiowaną relację w przesłankach i w konkluzjach reguł) zapewnia istnienie (i oczywiście jedyność) takiej najmniejszej relacji.

I ta właśnie najmniejsza relacja spełniająca podane implikacje to definiowana relacja przejścia od konfiguracji do odpowiadających im stanów końcowych.