SW wykład 3 - Slajd13

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

Wskazana równoważność semantyki operacyjnej i naturalnej podkreśla tylko intuicyjną rolę relacji wejścia/wyjścia dla każdej instrukcji języka TINY. Formalnie możemy tę relację zdefiniować przez warunek, że zachodzi ona między dwoma stanami, jeśli konfiguracja zawierająca daną instrukcję i pierwszy z tych stanów prowadzi do drugiego z nich jako stanu końcowego w semantyce naturalnej (albo równoważnie: istnieje skończone obliczenie w semantyce operacyjnej, które prowadzi od konfiguracji zawierającej daną instrukcję i pierwszy z tych stanów do drugiego z nich jako konfiguracji końcowej).

Ponieważ TINY jest językiem deterministycznym, co pokazaliśmy formalnie na gruncie obu jego podanych powyżej semantyk, tak określona relacja wejścia/wyjścia jest dla każdej instrukcji funkcją --- ale na ogół funkcją częściową, określoną tylko dla tych stanów, dla których z konfiguracji budowanej jak wyżej prowadzi obliczenie do jakiegoś stanu końcowego.

W ten sposób określiliśmy jeszcze jedną semantykę dla instrukcji języka TINY, w stylu podobnym do pomocniczej semantyki dla wyrażeń podanej w poprzednim module. Jest to mianowicie funkcja, która instrukcjom przypisuje ich znaczenia, będące częściowymi funkcjami ze zbioru stanów w zbiór stanów. Więcej o tak określanych, denotacyjnych semantykach w kolejnych modułach tych zajęć.