|
|
| Linia 1: |
Linia 1: |
|
| |
|
| == Ćwiczenia 1: semantyka operacyjna wyrażeń (małe kroki) ==
| |
|
| |
|
| |
| ==== Zadanie 1 (przygotowawcze) ====
| |
| Rozważmy prosty język wyrażeń, którego składnia opisana jest
| |
| następującą gramatyką:
| |
|
| |
| <math>
| |
| n \, ::= \,\, 0 \,\,|\,\, 1 \,\,|\,\, \ldots
| |
| </math>
| |
|
| |
| <math>
| |
| x \, ::= \,\, \ldots \, (identyfikatory) \, \ldots
| |
| </math>
| |
|
| |
| <math>
| |
| e \, ::= \,\,
| |
| n \,\,|\,\,
| |
| x \,\,|\,\,
| |
| e_1 + e_2 \,\,|\,\,
| |
| \mathbf{if}\, e_1 \,\mathbf{then}\, e_2 \,\mathbf{else}\, e_3
| |
| </math>
| |
|
| |
| Wynikiem wyrażenienia warunkowego <math> \mathbf{if}\, e_1 \,\mathbf{then}\, e_2 \,\mathbf{else}\, e_3 </math>
| |
| jest wartość wyrażenia <math> e_2 </math>, o ile wyrażenie
| |
| <math> e_1 </math> oblicza się do wartości różnej od zera; w przeciwnym
| |
| przypadku wynikiem jest wartość wyrażenia <math> e_3 </math>.
| |
|
| |
| Zaproponuj semantykę operacyjną (małe kroki) dla tego języka.
| |
|
| |
|
| |
| ==== Rozwiązanie ====
| |
|
| |
| Zacznijmy od ustalenia notacji i dziedzin syntaktycznych.
| |
| Niech <math> \mathbf{Num} </math> oznacza zbiór stałych liczbowych,
| |
| <math> n \in \mathbf{Num} = \{ 0, 1, \ldots \} </math>.
| |
| Podobnie, niech <math> \mathbf{Var} </math> oznacza zbiór identyfikatorów, które
| |
| mogą być nazwami zmiennych; <math> x \in \mathbf{Var} </math>.
| |
| Wreszcie, niech <math> \mathbf{Exp} </math> oznacza zbiór wyrażeń;
| |
| <math> e \in \mathbf{Exp} </math>.
| |
| Dla ułatwienia zapisywania reguł zakładamy, ze stałe
| |
| liczbowe sa wyrażeniami, czyli <math> \mathbf{Num} \subseteq \mathbf{Exp} </math>.
| |
|
| |
| Będziemy potrzebować zbioru ''stanów'', opisujących wartości
| |
| przypisane zmiennym.
| |
| Najprostszym rozwiązaniem jest przyjąc, że stan to funkcja
| |
| z <math> \mathbf{Var} </math> do <math> \mathbf{Num} </math>.
| |
| Oznaczmy przez <math> \mathbf{State} </math> zbiór wszystkich takich funkcji;
| |
| stany oznaczac będziemy przez <math> s, s_1, s', \ldots \in \mathbf{State} </math>.
| |
|
| |
| W naszej semantyce będziemy potrzebowac tranzycji dwóch postaci.
| |
| Po pierwsze, tranzycja
| |
|
| |
| <math>
| |
| e, s \,\Longrightarrow\, e', s
| |
| </math>
| |
|
| |
| oznaczająca mały krok w trakcie obliczania wyrażenia <math> e </math>
| |
| w stanie <math> s </math>, w wyniku którego <math> e </math> wyewoluowało do
| |
| <math> e' </math>. Stan nie ulega zmiania podczas obliczania wyrażenia,
| |
| więc to samo <math> s </math> figuruje po lewej i prawej stronie strzałki.
| |
|
| |
| Po drugie, tranzycja
| |
| <math>
| |
| e, s \,\Longrightarrow\, n
| |
| </math>
| |
|
| |
| będzie oznaczaczać, że wyrażenie <math> e </math> jest już policzone,
| |
| a jego wartością jest <math> n </math>.
| |
|
| |
| Zatem przyjmijmy, że zbiór konfiguracji to
| |
|
| |
| <math>
| |
| ( \mathbf{Exp} \times \mathbf{State} ) \, \cup \, \mathbf{Num}
| |
| </math>
| |
|
| |
| a konfiguracje końcowe to <math> \mathbf{Num} </math>.
| |
|
| |
| '''Uwaga:''' tranzycje pierwszej postaci mogłyby również wyglądać
| |
| następująco:
| |
| <math>
| |
| e, s \,\Longrightarrow\, e';
| |
| </math>
| |
| wtedy zbiorem konfiguracji byłby zbiór
| |
| <math>
| |
| ( \mathbf{Exp} \times \mathbf{State} ) \, \cup \, \mathbf{Exp}
| |
| </math>
| |
| a konfiguracje końcowe pozostałyby bez zmian
| |
| '''(koniec uwagi)'''.
| |
|
| |
|
| |
| Najprostsze są tranzycje prowadzące do konfiguracji końcowej:
| |
|
| |
| <math>
| |
| n, s \,\Longrightarrow\, n
| |
| </math>
| |
|
| |
| Zmienna oblicza się do swojej wartości w bieżącym stanie:
| |
| <math>
| |
| x, s \,\Longrightarrow\, n, s \quad \mbox{ o ile } s(x) = n
| |
| </math>
| |
|
| |
| Teraz zajmiemy się dodawaniem <math> e_1 + e_2 </math>. Ponieważ semantyka jest w stylu małych
| |
| kroków, musimy zdecydować się czy najpierw obliczyć pierwszy (lewy) składnik
| |
| <math> e_1 ] czy drugi?
| |
| Jeśli wybierzemy lewy, otrzymamy regułę:
| |
|
| |
| <math>
| |
| \frac{e_1, s \,\Longrightarrow\, e'_1, s}
| |
| {e_1 + e_2, s \,\Longrightarrow\, e'_1 + e_2}.
| |
| </math>
| |
|
| |
| Czyli mały krok w <math> e_1 </math> stanowi też mały krok w <math> e_1 + e_2 </math>.
| |
| Po zakończeniu obliczania <math> e_1 </math> przechodzimy do <math> e_2 </math>:
| |
|
| |
| <math>
| |
| \frac{e_2, s \,\Longrightarrow\, e'_2, s}
| |
| {n + e_2, s \,\Longrightarrow\, n + e'_2, s}.
| |
| </math>
| |
|
| |
| A na końcu dodajemy:
| |
|
| |
| <math>
| |
| n_1 + n_2, s \,\Longrightarrow\, n, s \quad \mbox{ o ile } n = n_1 + n_2.
| |
| </math>
| |
|
| |
| Zauważmy tutaj pewną subtelność, dotyczącą dwóch wystąpień
| |
| symbolu ''+'': pierwsze wystąpienie oznacza jedną z konstrukcji składniowych
| |
| języka, a drugie oznacza operację dodawania w zbiorze <math> \mathbf{Num} </math>.
| |
| Pozwalamy sobie na taką kolizję oznaczeń, gdyż nie powinna ona
| |
| prowadzić do niejednoznaczności. Pamiętajmy, że składnia języka jest
| |
| składnią abstrajkcyjną, więc zamiast <math> e_1 + e_2 </math> moglibyśmy równie
| |
| dobrze pisać np. <math> {\mathrm{add}}(e_1, e_2) </math>.
| |
|
| |
| Inna możliwą strategią obliczania <math> e_1 + e_2 </math> jest strategia
| |
| ''prawostronna'', którą otrzymujemy zastępując pierwsze dwie z trzech
| |
| powyższych reguł przez:
| |
|
| |
| <math>
| |
| \frac{e_2, s \,\Longrightarrow\, e'_2, s}
| |
| {e_1 + e_2, s \,\Longrightarrow\, e_1 + e'_2}
| |
| \quad \quad \quad
| |
| \frac{e_1, s \,\Longrightarrow\, e'_1, s}
| |
| {e_1 + n, s \,\Longrightarrow\, e'_1 + n, s}.
| |
| </math>
| |
|
| |
| Ponadto, jeśli przyjmiemy wszystkie pięc reguł, otrzymamy strategię
| |
| ''równoległą'', polegającą na obliczaniu jednocześnie <math> e_1 </math> i
| |
| <math> e_2 </math>. Bardziej precyzyjnie mówiąc, małe kroki obliczające
| |
| obydwa podwyrażenia przeplatają się, i to w dowolny sposób.
| |
| Ta dowolność prowadzi do ''niedeterminizmu'', czyli do sytuacji, gdy
| |
| kolejna (następna) konfiguracja nie jest wyznaczona jednoznacznie.
| |
| Jest tak, gdyż jednocześnie możemy mieć dwie tranzycje
| |
|
| |
| <math>
| |
| e_1 + e_2, s \,\Longrightarrow\, e'_1 + e_2, s
| |
| \quad \quad \quad
| |
| e_1 + e_2, s \,\Longrightarrow\, e_1 + e'_2, s.
| |
| </math>
| |
|
| |
| Zauważmy natomiast, że kolejność przeplatania się małych kroków obliczających
| |
| <math> e_1 </math> i <math> e_2 </math> nie wpływa w tym przypadku na końcową wartość
| |
| całego wyrażenia.
| |
|
| |
| Na koniec reguły dla wyrażenia warunkowego.
| |
|
| |
| <math>
| |
| \frac{e_1, s \,\Longrightarrow\, e'_1, s}
| |
| {\mathbf{if}\, e_1 \,\mathbf{then}\, e_2 \,\mathbf{else}\, e_3, s \,\Longrightarrow\, \mathbf{if}\, e'_1 \,\mathbf{then}\, e_2 \,\mathbf{else}\, e_3, s}
| |
| </math>
| |
|
| |
| <math>
| |
| \mathbf{if}\, n \,\mathbf{then}\, e_2 \,\mathbf{else}\, e_3, s \,\Longrightarrow\, e_2, s \quad \mbox{ o ile } n \neq 0
| |
| </math>
| |
|
| |
| <math>
| |
| \mathbf{if}\, n \,\mathbf{then}\, e_2 \,\mathbf{else}\, e_3, s \,\Longrightarrow\, e_3, s \quad \mbox{ o ile } n = 0
| |
| </math>
| |
|
| |
|
| |
| ==== Zadanie 2 ====
| |
|
| |
| Rozszerzmy język wyrażeń z poprzedniego zadania o jedną konstrukcję
| |
| <math>
| |
| e \, ::= \,\,
| |
| \ldots \,\,|\,\,
| |
| \mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2
| |
| </math>
| |
|
| |
| Wyrażenie <math> \mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2 </math> zawiera w sobie deklarację
| |
| <math> x = e_1 </math>, która stanowi jedyny mechannizm wiązania
| |
| identyfikatorów w naszym języku.
| |
| Wartość wyrażenia <math> \mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2 </math> obliczamy następująco:
| |
| najpierw oblicza się wartość <math> e_1 </math>, podstawia ją na zmienna
| |
| <math> x </math>, a następnie oblicza wyrażenie <math> e_2 </math>.
| |
| Zakresem zmiennej <math> x </math> jest wyrażenie <math> e_2 </math>, ale jeśli w
| |
| <math> e_2 </math> występuje podwyrażenie <math> \mathbf{let}\, x = \ldots \,\mathbf{in}\, e </math> to
| |
| odwołania do <math> x </math> wewnątrz <math> e </math> odnoszą się do ''najbliższej''
| |
| (najbardziej zagnieżdzonej) deklaracji zmiennej <math> x </math>.
| |
| Taki mechanizm wiązania identyfikatorów nazywamy ''wiązaniem
| |
| statycznym''.
| |
|
| |
| Zakładamy, że na początku wartości wszystkich zmiennych są
| |
| ''nieokreślone'', czyli zmienne są niezainicjowane, a odwołanie do
| |
| niezainicjowanej zmiennej jest uważane za niepoprawne.
| |
|
| |
|
| |
| ==== Przykłady ====
| |
|
| |
| <math>
| |
| \mathbf{let}\, x = z+z \,\mathbf{in}\, \mathbf{let}\, y = 7 \,\mathbf{in}\, \mathbf{let}\, x = y+3 \,\mathbf{in}\, x+x+y
| |
| \quad \quad \mbox{wynik} = 24
| |
| </math>
| |
| <math>
| |
| \mathbf{let}\, y = 5 \,\mathbf{in}\, \mathbf{let}\, x = (\, \mathbf{let}\, y = 3 \,\mathbf{in}\, y+y \,) \,\mathbf{in}\, x+y
| |
| \quad \quad \mbox{wynik} = 11
| |
| </math>
| |
| <math>
| |
| \mathbf{let}\, z = 5 \,\mathbf{in}\, x+z
| |
| \quad \quad \mbox{brak wyniku; odwołanie do niezainicjowanej
| |
| zmiennej}\, x
| |
| </math>
| |
| <math>
| |
| \mathbf{let}\, x = 1 \,\mathbf{in}\, \mathbf{let}\, x = x+x \,\mathbf{in}\, x
| |
| \quad \quad \mbox{wynik} = 2
| |
| </math>
| |
|
| |
|
| |
| ==== Rozwiązanie ====
| |
|
| |
| Podobnie jak poprzednio,
| |
| stan powinien opisywać wartości przypisane zmiennym, ale powinniśmy też
| |
| uwzględnić niezainicjowane zmienne, czyli zmienne bez żadnej wartości.
| |
| Przyjmijmy zatem, że stan to skończona funkcja częściowa z <math> \mathbf{Var} </math> do <math> \mathbf{Num} </math>.
| |
| Oznaczmy przez <math> \mathbf{State} </math> zbiór wszystkich takich funkcji.
| |
| Naturalnym stanem początkowym jest stan ''pusty'', tzn.
| |
| pusta funkcja częściowa, który będziemy oznaczać <math> \emptyset </math>.
| |
| A wartość wyrażenia <math> e </math> w stanie początkowym wynosi <math> n </math>
| |
| o ile zachodzi:
| |
|
| |
| <math>
| |
| e, \emptyset \,\Longrightarrow^{*}\, n.
| |
| </math>
| |
|
| |
| Będziemy potrzebowac tranzycji dwóch postaci, podobnie jak poprzednio,
| |
| ale pierwsza postać będzie trochę ogólniejsza:
| |
|
| |
| <math>
| |
| e, s \,\Longrightarrow\, e', s'.
| |
| </math>
| |
|
| |
| Tranzycja ta oznacza mały krok w trankcie obliczania wyrażenia <math> e </math>
| |
| w stanie <math> s </math>, w wyniku którego <math> e </math> wyewoluowało do
| |
| <math> e' </math> a nowym stanem jest <math> s' </math>.
| |
| Stan może się teraz zmienić na skutek deklaracji zmiennych.
| |
|
| |
| Ponieważ stan jest funkcją częściową, musimy zmienić niektóre reguły, np.
| |
|
| |
| <math>
| |
| x, s \,\Longrightarrow\, n, s \quad \mbox{ o ile } s(x) \mbox{ jest określone i } s(x) = n
| |
| </math>
| |
|
| |
|
| |
| ==== Zadanie 3 ====
| |
|
| |
| Zmodyfikuj semantykę z poprzedniego zadania tak, aby uzyskać
| |
| ''leniwą'' ewaluację wyrażeń, zgodnie z dyrektywą: nie obliczaj
| |
| wyrażenia o ile jego wynik nie jest potrzebny
| |
| (albo: obliczaj wartość wyrażenia dopiero wtedy, gdy jego wynik jest
| |
| naprawdę potrzebny). Spojrzmy na przykład:
| |
|
| |
| <math>
| |
| \mathbf{let}\, x = 7 \,\mathbf{in}\, \mathbf{let}\, y = y+y \,\mathbf{in}\, x+x
| |
| </math>
| |
|
| |
| Według semantyki z poprzedniego zadania wyrażnie to nie ma wartości,
| |
| bo w deklaracji <math> y = y+y </math> jest odwołanie do niezainicjowanej
| |
| zmiennej.
| |
| Natomiast w semantyce leniwej wyrażenie to obliczy się do wartości
| |
| <math> 14 </math>, ponieważ wyrażenie <math> y+y </math> nie będzie wogóle obliczane.
| |
| Będzie tak dlatego, że w wyrażeniu <math> x+x </math> nie ma odwołań do
| |
| zmiennej <math> y </math>.
| |
|
| |
|
| |
| ==== Rozwiązanie ====
| |
|
| |
|
| |
| ==== Zadanie 4 ====
| |
|
| |
| Dotychczas wystąpienie błędu podczas obliczania wyrażenia,
| |
| np. odwołanie do niezainicjowanej zmiennej, powodowało, że
| |
| wyrażenie nie posiadało wartości (nie było ciągu tranzycji
| |
| prowadzących do konfiguracji końcowej). Zmodyfikuj którąś z semantyk
| |
| z poprzednich zadań tak, aby błąd był komunikowany
| |
| jako jedna z konfiguracji końcowych. To znaczy: jeśli obliczenie
| |
| wyrażenia <math> e </math> w stanie <math> s </math> jest niemożliwe bo wystąpił
| |
| błąd, to
| |
|
| |
| <math>
| |
| e, s \,\Longrightarrow^{*}\, Blad
| |
| </math>
| |
