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

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.

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$$\rightarrow : E \times E$$e_0 \to e_1 \to e_2 \to \dots$$e_0 \to e_1 \to \dots \to v$ $v$$\forall e' \in E, v \not\rightarrow e'$$\newcommand{\llbracket}{[\![} \newcommand{\rrbracket}{]\!]}$

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 $\llbracket \cdot \rrbracket : E \to D$$D$$E$$D$$\mathbb{N}$$\mathbb{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$$\Downarrow : E \times V$$\bot$

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 1 → ⋯ → v $\to$$e \Downarrow v$$e \to e_1 \to \dots \to v$$v$
• 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.$\Downarrow : E \times V$$E \cup V$
• 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ę.$\to$
• 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.$\llbracket \cdot \rrbracket$
• 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.$\Downarrow$$\llbracket e \rrbracket = \{v \mid e \Downarrow v\}$
• I odwrotnie, biorąc pod uwagę semantykę denotacyjną , można zdefiniować semantykę dużego kroku . Znowu ten jest trochę bezcelowy.E ⇓ $\llbracket \cdot \rrbracket$$E \Downarrow \llbracket \cdot \rrbracket$

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 ⇓ $\exists (e_1, \dots, e_n), e \to e_1 \to \dots e_n \text{ and } \not\exists e', e_n \to e'$$e \Downarrow e_n$$e_1 \to^* e_2$$e_n \to^* v$$v$jest wartością wtedy ”.$e_1 \Downarrow v$