SW wykład 3 - Slajd7

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

Przez (łatwą) indukcję po strukturze drzewa dowodu można teraz pokazać na przykład, że semantyka naturalna instrukcji języka TINY zachowała jego determinizm: każda konfiguracja prowadzi do co najwyżej jednego stanu końcowego.

Na marginesie warto zauważyć, że próba "oczywistego" dowodu tego faktu przez indukcję strukturalną po strukturze zawartej w konfiguracjach instrukcji nie powiedzie się: pojawi się problem dla przypadku instrukcji pętli. Semantyka naturalna pętli nie jest bowiem "kompozycyjna": stan końcowy, do którego prowadzi konfiguracja zawierająca pętlę, może zależeć od stanów końcowych, do których prowadzą nie tylko konfiguracje zawierające bezpośrednie składowe danej pętli, ale też konfiguracja zawierająca tę pętlę jako całość. Więcej o problemach takich "rekurencyjnych" definicji w dalszych modułach tych zajęć dotyczących semantyki denotacyjnej.