Różnica między semantyką operacyjną małego i dużego kroku

28

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.

Simon Morgan
źródło
1
Artykuł w Wikipedii na temat semantyki operacyjnej wygląda obiecująco ... dopóki nie uświadomimy sobie, że suma informacji w sekcji „Semantyka dużych kroków” to „Ta sekcja wymaga rozszerzenia. (Luty 2011 r.)”.
David Richerby,
1
Jakie jest twoje źródło nauki? Co zawiera w tej sprawie? Co myślisz? Wskazówka: o czym jest semantyka wielkiego kroku x = 0; while ( true ) { x = x + 1; }?
Raphael
@Raphael Czytam Understanding Computation . Myślę, że podejście małostopniowe polega na zredukowaniu wyrażenia do podwyrażeń, dopóki nie będzie można go dalej zredukować, a następnie ocenienie. Wydaje się, że dużym krokiem jest ocena rzeczy od razu, ale tak naprawdę nie mam żadnej interesującej różnicy między tymi dwiema metodami, ponieważ obie wydają się dotyczyć drążenia konstrukcji wyższego poziomu.
Simon Morgan
Wielkim krokiem jest drążenie w dół od konstruktów wyższego poziomu poprzez ocenę podkonstruktów, a drobny krok poprzez redukcję większego konstruktu, ponownie, do jego podkonstruktów.
Simon Morgan,

Odpowiedzi:

32

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×Ee0e1e2e0e1v veE,ve

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[[]]:EDDEDNR

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 EV⇓: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.

  • Biorąc pod uwagę małą krok semantyka można zdefiniować odpowiednie semantyki dużym krokiem, który odnosi się każdy wyraz jego wartość (lub wartości, jeżeli redukcja nie jest deterministyczny): wtw istnieje łańcuch i nie mogą dalej zmniejszać. Zauważ, że generalnie nie można zrekonstruować semantyki małego kroku z semantyki dużego kroku. Na przykład wszystkie wyrażenia nie kończące się są nierozróżnialne w ramach semantyki dużego kroku.e v e e 1v vevee1vv
  • Biorąc pod uwagę semantykę dużym krokiem , można powiedzieć, że jest to semantyka małych krok na . To nie jest szczególnie przydatne.⇓:E×VEV
  • Biorąc pod uwagę semantykę , możesz zdefiniować odpowiednią semantykę denotacyjną, w której denotacja wyrażenia jest zbiorem łańcuchów redukcyjnych rozpoczynających się od niego. Jest to zgodne z formalną definicją, ale nie jest szczególnie przydatne, ponieważ dodaje zestaw teoretycznego narzutu do obiektów, które łatwiej jest zrozumieć, patrząc bezpośrednio na składnię.
  • Biorąc pod uwagę semantykę denotacyjną , możesz zdefiniować semantykę małych kroków, dodając wszystkie możliwe denotacje jako wartości w języku. Wymaga to tworzenia wartości, które nie są częścią składni, którą programista może napisać, co oznacza, że ​​niektóre interesujące wyniki muszą zawierać stwierdzenie „dla wszystkich programów, które programista może napisać”, a nie „dla wszystkich programów”. Ten też nie jest więc bardzo przydatny.[[]]
  • Biorąc pod uwagę semantykę dużego kroku , możesz zdefiniować odpowiadającą semantykę denotacyjną, w której domeną jest zbiór zestawów wartości: . Jeśli semantyka dużego kroku jest deterministyczna (każde wyrażenie zmniejsza się do jednej wartości), możesz zdefiniować prostszą semantykę denotacyjną, w której domeną jest zbiór wartości.[[[e]]={vev}
  • I odwrotnie, biorąc pod uwagę semantykę denotacyjną , można zdefiniować semantykę dużego kroku . Znowu ten jest trochę bezcelowy.E [[[]]E[[]]

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 1v(e1,,en),ee1en and e,eneeene1e2envvjest wartością wtedy ”.e1v

Gilles „SO- przestań być zły”
źródło
Uczę się tego, ale mam problem z tym, co powiedziałeś w swojej odpowiedzi, które chciałbym wyjaśnić. Powiedziałeś: „Semantyka dużych kroków jest w pewnym sensie w środku”. Czy jednak mały krok nie byłby faktycznie modelem „środkowym”? Rozważ wyrażenia: A: ((5 + 7) + 3) B: ((5 + 5) + 5) C: ((1 + 2) + 1) D: ((2 + 1) + 1) Denotacyjny sklasyfikowałby nawet C i D o różnych wartościach (możliwe, że „C” i „D”), a duży krok klasyfikuje je zarówno jako „4”, a zarówno A, jak i B jako „15”. Jednak mały krok daje ” + 3) „i” (10 + 5) ”dla A i B oraz„ (3 + 1) ”dla C i D.
Timothy Swan
@TimothySwan Zakładając, że chcesz zdefiniować zwykłą ocenę arytmetyczną, semantyka denotacyjna nie rozróżniałaby C i D.Sermantyka w małych krokach definiowałaby łańcuch redukcji, taki jak . Semantyka dużego kroku byłaby bardzo podobna do semantyki denotacyjnej: vs . w semantyce dużym krokiem jest jeden w składni języka natomiast w denotational semantyki jest jednym z metateorii, ale różnica nie jest widoczna lub ważne w tym prostym przykładzie. ( ( 2 + 1 ) + 1 ) 3 [((2+1)+1)3+14((2+1)+1)34 4[[((2+1)+1)]]=444
Gilles „SO- przestań być zły”
Kiedy więc powiedziałeś: „semantyka denotacyjna przypisuje„ znaczenie ”każdemu wyrażeniu”. nie chodziło Ci o jednoznaczną identyfikację samych wyrażeń, ale o jakieś znaczenie niezależne od oceny? Czy możesz podać prosty przykład, który wyraźnie pokazuje różnicę między semantyką dużego kroku a denotacją? Także, proszę wyjaśnić 3w ((2+1)+1)⇓3Zgaduję „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 zawiera a?
Timothy Swan
@TimothySwan Dopóki nie ma efektów ubocznych, brak determinizmu i żadnych funkcji, semantyka denotacyjna wyrażenia jest wartością, którą ocenia. Niedeterminizm to dobry sposób na zilustrowanie różnicy między krokiem wielkodostępnym a denotacyjnym: denotacja wyrażenia byłaby zbiorem wartości, które może on mieć: , podczas gdy semantyka dużego kroku miałaby wiele dopuszczalnych osądów: i i ... To była literówka. r a n d ( 1 .. n ) 1 r a n d ( 1 .. n ) 2[[rand(1..n)]]={1,2,,n}rand(1..n)1rand(1..n)23
Gilles „SO- przestań być zły”