SW wykład 3 - Slajd10

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

Spróbujmy teraz porównać dwie wprowadzone semantyki dla instrukcji języka TINY: semantykę operacyjną (małych kroków) i semantykę naturalna (wielkich kroków).

Zgodnie z nieformalną sugestią przy wprowadzaniu semantyki naturalnej powyżej, w pewnym sensie są one w istocie takie same: w semantyce naturalnej dana konfiguracja prowadzi do pewnej konfiguracji końcowej wtedy i tylko wtedy, gdy w semantyce operacyjnej obliczenie rozpoczynające się w tej konfiguracji kończy się w tejże konfiguracji końcowej.

Uwaga: nie jest to już teraz tylko intuicja; jest to w pełni ścisłe stwierdzenie, dla którego poniżej przeprowadzimy formalny dowód.