Jaka jest podstawowa różnica między semantyką operacyjną małego i dużego kroku?
Trudno mi zrozumieć, co to jest i motywację do posiadania tych dwóch.
semantics
operational-semantics
small-step-semantics
Simon Morgan
źródło
źródło
x = 0; while ( true ) { x = x + 1; }
?Odpowiedzi:
Semantyka małych kroków definiuje metodę oceny wyrażeń po jednym kroku obliczeniowym na raz. Formalnie rzecz biorąc, semantyka w małym stopniu dla języka wyrażeń jest relacją zwaną relacją redukcji . Semantyka w małych krokach opisuje szczegółowo to, co dzieje się z wyrażeniem. Jest w stanie podać dokładny opis nawet nie kończących się programów, z nieskończonym łańcuchem . Program kończący to taki, że kończy się wartością taką, że . \ newcommand {\ llbracket} {[\! [} \ newcommand {\ rrbracket} {] \!]}E →:E×E e0→e1→e2→… e0→e1→⋯→v v ∀e′∈E,v↛e′
Na drugim końcu spektrum jest semantyka denotacyjna . Semantyka denotacyjna przypisuje „znaczenie” każdemu wyrażeniu. Jest to funkcja od wyrażeń do denotacji: ( to domena). Przestrzeń oznaczeń może być całkowicie niezwiązana z przestrzenią syntaktyczną, na przykład może być wyrażeniami, które są obliczane na liczbę, a może być zbiorem liczb takich jak lub .D E D N R[[⋅]]:E→D D E D N R
Semantyka z dużymi krokami jest jakby w środku. A semantyka dużym krokiem na język ekspresji i zestaw wartości jest relacją . Odnosi wyrażenie do jego wartości (być może wielu wartości, jeśli język jest niedeterministyczny). Często do wyrażeń nie kończących używana jest specjalna wartość .V ⇓ : E × V ⊥E V ⇓:E×V ⊥
Dlaczego więc mamy te trzy pojęcia? Wszystkie te pojęcia mogą się nawzajem modelować, ale model ten powoduje pewien stopień złożoności.
Mówiąc operacyjnie, semantyka małych kroków odpowiada spojrzeniu na każdą operację wykonaną przez tłumacza języka. Semantyka dużych kroków patrzy tylko na wynikową wartość. Semantyka denotacyjna analizuje matematyczną interpretację, która może, ale nie musi mieć nic wspólnego z tym, co dzieje się na komputerze.
Semantyka małych kroków jest najbardziej oczywista. W sposób wyraźny dostarcza użytecznych informacji o nie kończących się programach. Mówiąc bardziej ogólnie, zapewnia szczegółowe informacje na temat zachowania programu.
Semantyka denotacyjna przekształca konstrukty składniowe w dowolne obiekty matematyczne; może wyrażać wszystko, co chcą naukowcy (możesz zdefiniować oznaczenie wyrażenia jako wszystkie możliwe łańcuchy redukcyjne z niego), ale kosztem dodania poziomu złożoności. Jest używany, gdy chcemy wyodrębnić niektóre szczegóły, takie jak dokładna ocena wyrażenia.
Semantyka składająca się z wielu kroków znajduje się pośrodku: wyodrębnia szczegóły oceny, ale zachowuje składniowy charakter wyniku. Zwykle koncepcja jest stosowana, gdy istnieje podstawowa semantyka małego kroku, jako sposób zwięzłego wyrażenia „ ”jako„ ”. W takich konstrukcjach, choć pojęcia są bardzo różne (jedna pozwala mówić o poszczególnych krokach obliczeniowych i programach nie kończących się, druga nie), definicje będą wyglądać bardzo podobnie, ponieważ w tym przypadku reguły definiujące semantyka dużych kroków ma zasadniczo postać „jeśli i… oraz i e ⇓ e n e 1 → ∗ e 2 e n → ∗ v v e 1 ⇓ v∃(e1,…,en),e→e1→…en and ∄e′,en→e′ e⇓en e1→∗e2 en→∗v v jest wartością wtedy ”.e1⇓v
źródło
3
w((2+1)+1)⇓3
Zgaduję „denotational” jest jakiś koniec wszystkim wartość, ale w tym, co instancja będzie „dużym krokiem” niekoniecznie map bezpośrednio na to? Czy różnica ma coś wspólnego z kontekstem, na przykład w(a + 1)
zależności od środowiska, które zawieraa
?3