Semantyka i weryfikacja programów/Ćwiczenia 1: Różnice pomiędzy wersjami

← poprzednia edycja następna edycja →

WizualnieWikikod

Wersja z 17:17, 26 lip 2006

Ćwiczenia 1: semantyka operacyjna wyrażeń (małe kroki)

Zadania z rozwiązaniami

Zadanie 1 (przygotowawcze)

Rozważmy bardzo prosty język wyrażeń, którego składnia opisana jest następującą gramatyką:

$n : : = 0 | 1 | \dots$

$x : : = \dots (i d e n t y f i k a t o r y) \dots$

$e : : = n | x | e_{1} + e_{2} | 𝐢 𝐟 e_{1} 𝐭 𝐡 𝐞 𝐧 e_{2} 𝐞 𝐥 𝐬 𝐞 e_{3}$

Wynikiem wyrażenienia warunkowego $𝐢 𝐟 e_{1} 𝐭 𝐡 𝐞 𝐧 e_{2} 𝐞 𝐥 𝐬 𝐞 e_{3}$ jest wartość wyrażenia $e_{2}$ , o ile wyrażenie $e_{1}$ oblicza się do wartości różnej od zera; w przeciwnym przypadku wynikiem jest wartość wyrażenia $e_{3}$ .

Zaproponuj semantykę operacyjną (małe kroki) dla tego języka.

Rozwiązanie

Zacznijmy od ustalenia notacji i dziedzin syntaktycznych. Niech $𝐍 𝐮 𝐦$ oznacza zbiór stałych liczbowych, $n \in 𝐍 𝐮 𝐦 = {0, 1, \dots}$ . Podobnie, niech $𝐕 𝐚 𝐫$ oznacza zbiór identyfikatorów, które mogą być nazwami zmiennych; $x \in 𝐕 𝐚 𝐫$ . Wreszcie, niech $𝐄 𝐱 𝐩$ oznacza zbiór wyrażeń; $e \in 𝐄 𝐱 𝐩$ . Dla ułatwienia zapisywania reguł zakładamy, ze stałe liczbowe sa wyrażeniami, czyli $𝐍 𝐮 𝐦 \subseteq 𝐄 𝐱 𝐩$ .

Będziemy potrzebować zbioru stanów, opisujących wartości przypisane zmiennym. Najprostszym rozwiązaniem jest przyjąc, że stan to funkcja z $𝐕 𝐚 𝐫$ do $𝐍 𝐮 𝐦$ . Oznaczmy przez $𝐒 𝐭 𝐚 𝐭 𝐞$ zbiór wszystkich takich funkcji; stany oznaczac będziemy przez $s, s_{1}, s^{'}, \dots \in 𝐒 𝐭 𝐚 𝐭 𝐞$ .

W naszej semantyce będziemy potrzebowac tranzycji dwóch postaci. Po pierwsze, tranzycja

$e, s ⟹ e^{'}, s$

oznaczająca mały krok w trakcie obliczania wyrażenia $e$ w stanie $s$ , w wyniku którego $e$ wyewoluowało do $e^{'}$ . Stan nie ulega zmiania podczas obliczania wyrażenia, więc to samo $s$ figuruje po lewej i prawej stronie strzałki.

Po drugie, tranzycja $e, s ⟹ n$

będzie oznaczaczać, że wyrażenie $e$ jest już policzone, a jego wartością jest $n$ .

Zatem przyjmijmy, że zbiór konfiguracji to

$(𝐄 𝐱 𝐩 \times 𝐒 𝐭 𝐚 𝐭 𝐞) \cup 𝐍 𝐮 𝐦$

a konfiguracje końcowe to $𝐍 𝐮 𝐦$ .

Uwaga: Tranzycje pierwszej postaci mogłyby również wyglądać następująco: $e, s ⟹ e^{'} .$ Wtedy zbiorem konfiguracji byłby zbiór $(𝐄 𝐱 𝐩 \times 𝐒 𝐭 𝐚 𝐭 𝐞) \cup 𝐄 𝐱 𝐩$ a konfiguracje końcowe pozostałyby bez zmian. (koniec uwagi)

Najprostsze są tranzycje prowadzące do konfiguracji końcowej:

$n, s ⟹ n$

Zmienna oblicza się do swojej wartości w bieżącym stanie:

$x, s ⟹ n, s o ile s (x) = n .$

Teraz zajmiemy się dodawaniem $e_{1} + e_{2}$ . Ponieważ semantyka jest w stylu małych kroków, musimy zdecydować się czy najpierw obliczyć pierwszy (lewy) składnik $e_{1}$ czy drugi? Jeśli wybierzemy lewy (strategia lewostronna), otrzymamy regułę:

$\frac{e_{1}, s ⟹ e'_{1}, s}{e_{1} + e_{2}, s ⟹ e'_{1} + e_{2}, s} .$

Czyli mały krok w $e_{1}$ stanowi też mały krok w $e_{1} + e_{2}$ . Po zakończeniu obliczania $e_{1}$ przechodzimy do $e_{2}$ :

$\frac{e_{2}, s ⟹ e'_{2}, s}{n + e_{2}, s ⟹ n + e'_{2}, s} .$

A na końcu dodajemy:

$n_{1} + n_{2}, s ⟹ n, s o ile n = n_{1} + n_{2} .$

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 $𝐍 𝐮 𝐦$ . 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 $e_{1} + e_{2}$ moglibyśmy równie dobrze pisać np. $a d d (e_{1}, e_{2})$ .

Inna możliwą strategią obliczania $e_{1} + e_{2}$ jest strategia prawostronna, którą otrzymujemy zastępując pierwsze dwie z trzech powyższych reguł przez:

$\frac{e_{2}, s ⟹ e'_{2}, s}{e_{1} + e_{2}, s ⟹ e_{1} + e'_{2}} \frac{e_{1}, s ⟹ e'_{1}, s}{e_{1} + n, s ⟹ e'_{1} + n, s} .$

Ponadto, jeśli przyjmiemy regułę pierwszą (dla $e_{1}$ ), trzecią i czwartą (dla $e_{2}$ ), otrzymamy strategię równoległą, polegającą na obliczaniu jednocześnie $e_{1}$ i $e_{2}$ :

$\frac{e_{1}, s ⟹ e'_{1}, s}{e_{1} + e_{2}, s ⟹ e'_{1} + e_{2}, s} \frac{e_{2}, s ⟹ e'_{2}, s}{e_{1} + e_{2}, s ⟹ e_{1} + e'_{2}} n_{1} + n_{2}, s ⟹ n, s o ile n = n_{1} + n_{2} .$

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ż możemy mieć do wyboru dwie różne tranzycje

$e_{1} + e_{2}, s ⟹ e'_{1} + e_{2}, s e_{1} + e_{2}, s ⟹ e_{1} + e'_{2}, s .$

Zauważmy natomiast, że kolejność przeplatania się małych kroków obliczających $e_{1}$ i $e_{2}$ nie wpływa w tym przypadku na końcową wartość całego wyrażenia.

Na koniec reguły dla wyrażenia warunkowego.

$\frac{e_{1}, s ⟹ e'_{1}, s}{𝐢 𝐟 e_{1} 𝐭 𝐡 𝐞 𝐧 e_{2} 𝐞 𝐥 𝐬 𝐞 e_{3}, s ⟹ 𝐢 𝐟 e'_{1} 𝐭 𝐡 𝐞 𝐧 e_{2} 𝐞 𝐥 𝐬 𝐞 e_{3}, s}$

$𝐢 𝐟 n 𝐭 𝐡 𝐞 𝐧 e_{2} 𝐞 𝐥 𝐬 𝐞 e_{3}, s ⟹ e_{2}, s o ile n \neq 0$

$𝐢 𝐟 n 𝐭 𝐡 𝐞 𝐧 e_{2} 𝐞 𝐥 𝐬 𝐞 e_{3}, s ⟹ e_{3}, s o ile n = 0$

Zadanie 2

Rozszerzmy język wyrażeń z poprzedniego zadania o jedną konstrukcję

$e : : = \dots | 𝐥 𝐞 𝐭 x = e_{1} 𝐢 𝐧 e_{2}$

Wyrażenie $𝐥 𝐞 𝐭 x = e_{1} 𝐢 𝐧 e_{2}$ zawiera w sobie deklarację $x = e_{1}$ , która stanowi mechanizm wiązania identyfikatorów w naszym języku. Deklaracja $x = e_{1}$ wprowadza nową zmienną $x$ oraz przypisuje jej wartość. Wartość wyrażenia $𝐥 𝐞 𝐭 x = e_{1} 𝐢 𝐧 e_{2}$ obliczamy następująco: najpierw oblicza się wartość $e_{1}$ , podstawia ją na zmienna $x$ , a następnie oblicza wyrażenie $e_{2}$ . Zakresem zmiennej $x$ jest wyrażenie $e_{2}$ , czyli wewnątrz $e_{2}$ można odwoływać się (wielokrotnie) do zmiennej $x$ ; Ogólniej, odwołania do zmiennej w wyrażeniu odnoszą się do najbliższej (najbardziej zagnieżdzonej) deklaracji tej zmiennej. Taki mechanizm wiązania identyfikatorów nazywamy wiązaniem statycznym. Przyjmujemy zwykłe reguły przesłaniania zmiennych. Np., jeśli w $e_{2}$ występuje podwyrażenie $𝐥 𝐞 𝐭 x = \dots 𝐢 𝐧 e$ to odwołania do $x$ wewnątrz $e$ odnoszą się do najbliższej deklaracji zmiennej $x$ .

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

$𝐥 𝐞 𝐭 x = z + z 𝐢 𝐧 𝐥 𝐞 𝐭 y = 7 𝐢 𝐧 𝐥 𝐞 𝐭 x = y + 3 𝐢 𝐧 x + x + y \mapsto wynik = 24$ $𝐥 𝐞 𝐭 y = 5 𝐢 𝐧 𝐥 𝐞 𝐭 x = (𝐥 𝐞 𝐭 y = 3 𝐢 𝐧 y + y) 𝐢 𝐧 x + y \mapsto wynik = 11$ Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathbf{let}\, z = 5 \,\mathbf{in}\, x+z \quad \quad \mapsto \quad \quad \mbox{brak wyniku; odwołanie do niezainicjowanej zmiennej}\, x } $𝐥 𝐞 𝐭 x = 1 𝐢 𝐧 𝐥 𝐞 𝐭 x = x + x 𝐢 𝐧 x + x \mapsto wynik = 4$

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 $𝐕 𝐚 𝐫$ do $𝐍 𝐮 𝐦$ . Oznaczmy symbolem $𝐒 𝐭 𝐚 𝐭 𝐞$ zbiór wszystkich takich funkcji: $𝐒 𝐭 𝐚 𝐭 𝐞 = 𝐕 𝐚 𝐫 \to_{f i n} 𝐍 𝐮 𝐦$ . Naturalnym stanem początkowym jest stan pusty, tzn. pusta funkcja częściowa, który będziemy oznaczać $\emptyset$ . A wartość wyrażenia $e$ w stanie początkowym wynosi $n$ o ile zachodzi:

$e, \emptyset ⟹^{*} n .$

Będziemy potrzebowac tranzycji dwóch postaci, podobnie jak poprzednio, ale pierwsza postać będzie trochę ogólniejsza:

$e, s ⟹ e^{'}, s^{'} .$

Tranzycja ta oznacza mały krok w trakcie obliczania wyrażenia $e$ w stanie $s$ , w wyniku którego $e$ wyewoluowało do $e^{'}$ a nowym stanem jest $s^{'}$ . Stan może się teraz zmienić na skutek deklaracji zmiennych.

Spróbujmy rozszerzyc semantykę z poprzedniego zadania. Ponieważ stan jest funkcją częściową, musimy zmienić niektóre reguły, np.

$x, s ⟹ n, s o ile s (x) jest określone i s (x) = n$

Następnie dodajemy reguły dla wyrażenia $𝐥 𝐞 𝐭 x = e_{1} 𝐢 𝐧 e_{2}$ . Gdy $e_{1}$ jest już obliczne, wyatarczy reguła:

$𝐥 𝐞 𝐭 x = n 𝐢 𝐧 e_{2}, s ⟹ e_{2}, s [x \mapsto n] .$

Notacja $s [x \mapsto n]$ oznacza stan $s$ , który zmodyfikowano przypisując zmiennej $x$ wartość $n$ , niezależnie od tego, czy $s (x)$ było określone, czy nie, i pozostawiając niezmienione wartości dla pozostałych zmiennych. Formanie

$s [x \mapsto n] (y) = {\begin{cases} n & y = x \\ s (y) & y \neq x \end{cases}$

Dla $y \neq x$ zachodzi $s [x \mapsto n] (y) = s (y)$ (w szczególności, $s [x \mapsto n] (y)$ jest określone wtedy i tylko wtedy, gdy $s (y)$ jest określone).

Natomiast aby obliczyc $e_{1}$ potrzebujemy reguły:

$\frac{e_{1}, s ⟹ e'_{1}, s^{'}}{𝐥 𝐞 𝐭 x = e_{1} 𝐢 𝐧 e_{2}, s ⟹ 𝐥 𝐞 𝐭 x = e'_{1} 𝐢 𝐧 e_{2}, s^{'}}$

Zwróćmy uwagę, że stan $s^{'}$ może być różny od $s$ , np. dlatego, że wewnątrz $e_{1}$ znajduje się podwyrażenie $𝐥 𝐞 𝐭 y = \dots$ .

Pytanie: czy taka semantyka jest poprawna?

Niestety nie, gdyż nie uwzględniamy ograniczonego zasięgu zmiennej. Rzućmy okiem na przykład:

$𝐥 𝐞 𝐭 x = (𝐥 𝐞 𝐭 z = 4 𝐢 𝐧 z + z + z) i n z$

Według naszych intencji to wyrażenie nie ma wartości, gdyż ostatnie odwołanie do $z$ jest błędne. Natomiast według powyższych reguł mamy

$𝐥 𝐞 𝐭 x = (𝐥 𝐞 𝐭 z = 4 i n z + z + z) 𝐢 𝐧 z, \emptyset ⟹ 𝐥 𝐞 𝐭 x = z + z + z 𝐢 𝐧 z, \emptyset [z \mapsto 4] ⟹ \dots ⟹ 𝐥 𝐞 𝐭 x = 12 𝐢 𝐧 z, \emptyset [z \mapsto 4] ⟹ 12, \emptyset [z \mapsto 4] ⟹ 12!$

Nasz błąd polega na tym, że po zakończeniu obliczania podwyrażenia $𝐥 𝐞 𝐭 z = 4 𝐢 𝐧 z + z + z$ zapominamy przywrócić zmiennej $z$ poprzednią wartość (a właściwie brak wartości w przykładzie powyżej).

Wygodne i eleganckie rozwiązanie tego problemu jest możliwe, jeśli rozszerzymy składnię naszego języka. Intuicyjnie, reguła

$𝐥 𝐞 𝐭 x = n 𝐢 𝐧 e_{2}, s ⟹ e_{2}, s [x \mapsto n] .$

powinna zostać zastąpiona przez

$𝐥 𝐞 𝐭 x = n 𝐢 𝐧 e_{2}, s ⟹ e_{2} 𝐭 𝐡 𝐞 𝐧,,przywróć wartość zmiennej x'', s [x \mapsto n] .$

czyli potrzebujemy konstrukcji składniowej, która polega na obliczeniu wyrażenia $e_{2}$ a następnie na przypisaniu zmiennej $x$ danej wartości. Rozszerzmy zatem składnię następujaco:

$e : : = \dots | e 𝐭 𝐡 𝐞 𝐧 x : = n .$

Zauważmy, że wyrażenie $e 𝐭 𝐡 𝐞 𝐧 x : = n$ jest w pewnym sensie dualne do $𝐥 𝐞 𝐭 x = n 𝐢 𝐧 e$ , gdyż jedyna (choc niewątpliwie istotna) różnica między nimi to kolejność obliczenia $e$ i przypisania wartości na zmienną $x$ . Oto nowa reguła

$𝐥 𝐞 𝐭 x = n 𝐢 𝐧 e_{2}, s ⟹ e_{2} 𝐭 𝐡 𝐞 𝐧 x : = n^{'}, s [x \mapsto n] o ile s (x) = n^{'} .$

Pewna trudność pojawiają się w sytuacji, gdy $s (x)$ jest nieokreślone, czyli gdy zmienna $x$ jest niezainicjowana -- reguła powyższa nie obejmuje wogóle takiej sytuacji. Najprostszym sposobem rozwiązania tej trudności jest rozszerzenie konstrukcji $e 𝐭 𝐡 𝐞 𝐧 x : = n$ :

$e : : = \dots | e 𝐭 𝐡 𝐞 𝐧 x : = n | e 𝐭 𝐡 𝐞 𝐧 x : = ⊥$

gdzie symbol $⊥$ oznacza brak wartości. Dodajemy również regułę:

$𝐥 𝐞 𝐭 x = n 𝐢 𝐧 e_{2}, s ⟹ e_{2} 𝐭 𝐡 𝐞 𝐧 x : = ⊥, s [x \mapsto n] o ile s (x) jest nieokreślone .$

Uwaga: Inny sposób rozwiązania omawianej trudności polega na rozszerzeniu zbioru $𝐍 𝐮 𝐦$ o dodatkowy element $⊥$ :

$n : : = ⊥ | 0 | 1 | \dots$

Wtedy nie musimy dodawać osobnego wariantu ostatniej reguły, ale za to $n = ⊥$ może sie pojawić w wyrażeniach. Dodatkowo, w tym rozwiązaniu warto poczynić umowę, że $s (x) = ⊥$ reprezentuje brak wartości zmiennej $x$ . Wtedy stany są funkcjami całkowitymi z $𝐕 𝐚 𝐫$ w $𝐍 𝐮 𝐦$ przyjmującymi wartość różną od $⊥$ tylko dla skończenie wielu elementów. (koniec uwagi)

Na zakończenie scalamy semantykę dla $e 𝐭 𝐡 𝐞 𝐧 x : = n$ z semantyką pozostałych wyrażeń:

$\frac{e, s ⟹ e^{'}, s^{'}}{e 𝐭 𝐡 𝐞 𝐧 x : = n, s ⟹ e^{'} 𝐭 𝐡 𝐞 𝐧 x : = n, s^{'}}$

$n^{'} 𝐭 𝐡 𝐞 𝐧 x : = n, s ⟹ n^{'}, s [x \mapsto n]$

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). Spójrzmy na przykład:

$𝐥 𝐞 𝐭 x = 7 𝐢 𝐧 𝐥 𝐞 𝐭 y = y + y 𝐢 𝐧 x + x$

Według semantyki z poprzedniego zadania wyrażnie to nie ma wartości, bo w deklaracji $y = y + y$ jest odwołanie do niezainicjowanej zmiennej. Natomiast w semantyce leniwej wyrażenie to obliczy się do wartości $14$ , gdyż wyrażenie $y + y$ nie będzie wogóle obliczane. Będzie tak dlatego, że w wyrażeniu $x + x$ nie ma odwołań do zmiennej $y$ .

Rozwiązanie

Semantyka będzie bardzo podobna do tej z poprzedniego zadania. Zasadnicza różnica dotyczy informacji przechowywanej w stanie. Dotychczas $s (x) \in 𝐍 𝐮 𝐦$ , gdyż podwyrażenie $e$ w $𝐥 𝐞 𝐭 x = e 𝐢 𝐧 \dots$ obliczało sie natychmiast. Jeśli chcemy opóżnic obliczenie tego podwyrażenia, to w $s (x)$ powinniśmy zapamiętać całe (nieobliczone) wyrażenie $e$ wraz ze stanem bieżącym. Czyli

$𝐒 𝐭 𝐚 𝐭 𝐞 = 𝐕 𝐚 𝐫 \to 𝐄 𝐱 𝐩 \times 𝐒 𝐭 𝐚 𝐭 𝐞 .$

Odpowiednia reguła dla wyrażenia $𝐥 𝐞 𝐭$ to

$𝐥 𝐞 𝐭 x = e_{1} 𝐢 𝐧 e_{2}, s ⟹ e_{2}, s [x \mapsto (e_{1}, s)] .$

Uważnego czytelnika zapewne zaniepokoił fakt, że $𝐒 𝐭 𝐚 𝐭 𝐞$ stoi zarówno po lewej jak i po prawej stronie równania $𝐒 𝐭 𝐚 𝐭 𝐞 = 𝐕 𝐚 𝐫 \to 𝐄 𝐱 𝐩 \times 𝐒 𝐭 𝐚 𝐭 𝐞 .$ Również zapis $s [x \mapsto (e_{1}, s)]$ może wzbudzić niepokój, gdyż sugeruje on, iż $s (x)$ zawiera, jako jeden z elementów pary, obiekt tego samego typu co $s$ . Formalnego rozwiązania tego typu dylematów dostarcza teoria dziedzin. Natomiast na użytek semantyki operacyjnej wystarczy, jeśli uznamy, iż równanie $𝐒 𝐭 𝐚 𝐭 𝐞 = 𝐕 𝐚 𝐫 \to 𝐄 𝐱 𝐩 \times 𝐒 𝐭 𝐚 𝐭 𝐞$ stanowi skrótowy zapis następującej definicji. Zdefiniujmy ${𝐒 𝐭 𝐚 𝐭 𝐞}_{0}, {𝐒 𝐭 𝐚 𝐭 𝐞}_{1}, \dots$ następująco:

${𝐒 𝐭 𝐚 𝐭 𝐞}_{0} = {\emptyset}$

${𝐒 𝐭 𝐚 𝐭 𝐞}_{n + 1} = 𝐕 𝐚 𝐫 \to_{f i n} 𝐄 𝐱 𝐩 \times {𝐒 𝐭 𝐚 𝐭 𝐞}_{n}$

....

Zadania domowe

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 $e$ w stanie $s$ jest niemożliwe bo wystąpił błąd, to

$e, s ⟹^{*} B l a d$

Zadanie 5

Rozważ rozszerzenie języka z zadania 2 o wyrażenia boolowskie:

$n : : = 0 | 1 | \dots$

$x : : = \dots (i d e n t y f i k a t o r y) \dots$

$b : : = 𝐭 𝐫 𝐮 𝐞 | 𝐭 𝐫 𝐮 𝐞 | e_{1} \leq e_{2} | \neg b | b_{1} \land b_{2}$

$e : : = n | x | e_{1} + e_{2} | 𝐢 𝐟 b 𝐭 𝐡 𝐞 𝐧 e_{2} 𝐞 𝐥 𝐬 𝐞 e_{3} | 𝐥 𝐞 𝐭 x = e_{1} 𝐢 𝐧 e_{2}$

Zaproponuj semantykę małych kroków dla tego języka.

Semantyka i weryfikacja programów/Ćwiczenia 1: Różnice pomiędzy wersjami

Wersja z 17:17, 26 lip 2006

Spis treści

Ćwiczenia 1: semantyka operacyjna wyrażeń (małe kroki)

Zadania z rozwiązaniami

Zadanie 1 (przygotowawcze)

Rozwiązanie

Zadanie 2

Przykłady

Rozwiązanie

Zadanie 3

Rozwiązanie

Zadania domowe

Zadanie 4

Zadanie 5

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia

@@ Linia 1: / Linia 1: @@
+== Ćwiczenia 1: semantyka operacyjna wyrażeń (małe kroki) ==
+=== Zadania z rozwiązaniami ===
+==== Zadanie 1 (przygotowawcze) ====
+Rozważmy bardzo 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 </math> czy drugi?
+Jeśli wybierzemy lewy (strategia ''lewostronna''), otrzymamy regułę:
+<math>
+\frac{e_1, s \,\Longrightarrow\, e'_1, s}
+     {e_1 + e_2, s \,\Longrightarrow\, e'_1 + e_2, s}.
+</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 regułę pierwszą (dla <math> e_1 </math>), trzecią
+i czwartą (dla <math> e_2 </math>), otrzymamy strategię
+''równoległą'', polegającą na obliczaniu jednocześnie <math> e_1 </math> i
+<math> e_2 </math>:
+<math>
+\frac{e_1, s \,\Longrightarrow\, e'_1, s}
+     {e_1 + e_2, s \,\Longrightarrow\, e'_1 + e_2, s}
+\quad \quad \quad
+\frac{e_2, s \,\Longrightarrow\, e'_2, s}
+     {e_1 + e_2, s \,\Longrightarrow\, e_1 + e'_2}
+\quad \quad \quad
+n_1 + n_2, s \,\Longrightarrow\, n, s \quad \mbox{ o ile } n = n_1 + n_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ż możemy mieć do wyboru dwie różne 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 mechanizm wiązania
+identyfikatorów w naszym języku.
+Deklaracja <math> x = e_1 </math> wprowadza nową zmienną <math> x </math>
+oraz przypisuje jej wartość.
+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>, czyli
+wewnątrz <math> e_2 </math> można odwoływać się (wielokrotnie) do zmiennej <math> x </math>;
+Ogólniej, odwołania do zmiennej w wyrażeniu odnoszą się do ''najbliższej''
+(najbardziej zagnieżdzonej) deklaracji tej zmiennej.
+Taki mechanizm wiązania identyfikatorów nazywamy ''wiązaniem
+statycznym''.
+Przyjmujemy zwykłe reguły przesłaniania zmiennych.
+Np., 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''
+deklaracji zmiennej <math> x </math>.
+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 \mapsto \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 \mapsto \quad \quad \mbox{wynik} = 11
+</math>
+<math>
+\mathbf{let}\, z = 5 \,\mathbf{in}\, x+z
+\quad \quad \mapsto \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+x
+\quad \quad \mapsto \quad \quad \mbox{wynik} = 4
+</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 symbolem <math> \mathbf{State} </math> zbiór wszystkich takich funkcji:
+<math>
+\mathbf{State} = \mathbf{Var} \to_{\mathrm{fin}} \mathbf{Num}
+</math>.
+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 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> a nowym stanem jest <math> s' </math>.
+Stan może się teraz zmienić na skutek deklaracji zmiennych.
+Spróbujmy rozszerzyc semantykę z poprzedniego zadania.
+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>
+Następnie dodajemy reguły dla wyrażenia
+<math> \mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2 </math>.
+Gdy <math> e_1 </math> jest już obliczne, wyatarczy reguła:
+<math>
+\mathbf{let}\, x = n \,\mathbf{in}\, e_2, s \,\Longrightarrow\, e_2, s[x \mapsto n].
+</math>
+Notacja <math> s[x \mapsto n] </math> oznacza stan <math> s </math>, który zmodyfikowano
+przypisując zmiennej <math> x </math> wartość <math> n </math>,
+niezależnie od tego, czy <math> s(x) </math> było określone, czy nie,
+i pozostawiając niezmienione wartości dla pozostałych zmiennych.
+Formanie
+<math>
+s[x \mapsto n](y) =
+\begin{cases}
+n    & y = x \\
+s(y) & y \neq x
+\end{cases}
+</math>
+Dla <math> y \neq x </math> zachodzi <math> s[x \mapsto n](y) = s(y) </math>
+(w szczególności, <math> s[x \mapsto n](y) </math> jest określone wtedy i tylko
+wtedy, gdy <math> s(y) </math> jest określone).
+Natomiast aby obliczyc <math> e_1 </math> potrzebujemy reguły:
+<math>
+\frac{e_1, s \,\Longrightarrow\, e'_1, s'}
+{\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2, s \,\Longrightarrow\, \mathbf{let}\, x = e'_1 \,\mathbf{in}\, e_2, s'}
+</math>
+Zwróćmy uwagę, że stan <math> s' </math> może być różny od <math> s </math>,
+np. dlatego, że wewnątrz <math> e_1 </math> znajduje się podwyrażenie
+<math> \mathbf{let}\, y = \ldots </math>.
+'''Pytanie:''' czy taka semantyka jest poprawna?
+Niestety nie, gdyż nie uwzględniamy ograniczonego zasięgu zmiennej.
+Rzućmy okiem na przykład:
+<math>
+\mathbf{let}\, x = (\mathbf{let}\, z = 4 \,\mathbf{in}\, z+z+z) in z
+</math>
+Według naszych intencji to wyrażenie nie ma wartości, gdyż ostatnie
+odwołanie do <math> z </math> jest błędne.
+Natomiast według powyższych reguł mamy
+<math>
+\mathbf{let}\, x = (\mathbf{let}\, z = 4 in z+z+z) \,\mathbf{in}\, z, \emptyset \,\Longrightarrow\,
+\mathbf{let}\, x = z+z+z \,\mathbf{in}\, z, \emptyset[z \mapsto 4] \,\Longrightarrow\, \quad \ldots \quad \,\Longrightarrow\,
+\mathbf{let}\, x = 12 \,\mathbf{in}\, z, \emptyset[z \mapsto 4] \,\Longrightarrow\,
+, \emptyset[z \mapsto 4] \,\Longrightarrow\,
+!
+</math>
+Nasz błąd polega na tym, że po zakończeniu obliczania podwyrażenia
+<math> \mathbf{let}\, z = 4 \,\mathbf{in}\, z+z+z </math> ''zapominamy'' przywrócić zmiennej <math> z </math>
+poprzednią wartość (a właściwie brak wartości w przykładzie powyżej).
+Wygodne i eleganckie rozwiązanie tego problemu jest możliwe, jeśli
+rozszerzymy składnię naszego języka.
+Intuicyjnie, reguła
+<math>
+\mathbf{let}\, x = n \,\mathbf{in}\, e_2, s \,\Longrightarrow\, e_2, s[x \mapsto n].
+</math>
+powinna zostać zastąpiona przez
+<math>
+\mathbf{let}\, x = n \,\mathbf{in}\, e_2, s \,\Longrightarrow\, e_2 \,\mathbf{then}\, \mbox{,,przywróć wartość zmiennej x''}, s[x \mapsto n].
+</math>
+czyli potrzebujemy konstrukcji składniowej, która polega na obliczeniu
+wyrażenia
+<math> e_2 </math> a następnie na przypisaniu zmiennej <math> x </math> danej wartości.
+Rozszerzmy zatem składnię następujaco:
+<math>
+e \,  ::=  \,\,
+        \ldots   \,\,|\,\,
+        e \,\mathbf{then}\, x := n.
+</math>
+Zauważmy, że wyrażenie <math> e \,\mathbf{then}\, x:= n </math> jest w pewnym sensie dualne
+do <math> \mathbf{let}\, x = n \,\mathbf{in}\, e </math>, gdyż jedyna (choc niewątpliwie istotna) różnica
+między nimi to kolejność obliczenia <math> e </math> i przypisania wartości
+na zmienną <math> x </math>.
+Oto nowa reguła
+<math>
+\mathbf{let}\, x = n \,\mathbf{in}\, e_2, s \,\Longrightarrow\, e_2 \,\mathbf{then}\, x := n', s[x \mapsto n] \quad
+\mbox{ o ile } s(x) = n'.
+</math>
+Pewna trudność pojawiają się w sytuacji, gdy <math> s(x) </math> jest
+nieokreślone, czyli gdy zmienna <math> x </math> jest niezainicjowana -- reguła
+powyższa nie obejmuje wogóle takiej sytuacji.
+Najprostszym sposobem rozwiązania tej trudności jest rozszerzenie
+konstrukcji <math> e \,\mathbf{then}\, x := n </math>:
+<math>
+e \,  ::=  \,\,
+        \ldots   \,\,|\,\,
+        e \,\mathbf{then}\, x := n  \,\,|\,\,
+        e \,\mathbf{then}\, x := \bot
+</math>
+gdzie symbol <math> \bot </math> oznacza brak wartości.
+Dodajemy również regułę:
+<math>
+\mathbf{let}\, x = n \,\mathbf{in}\, e_2, s \,\Longrightarrow\, e_2 \,\mathbf{then}\, x := \bot, s[x \mapsto n] \quad
+\mbox{ o ile } s(x) \, \mbox{ jest nieokreślone}.
+</math>
+'''Uwaga:'''
+Inny sposób rozwiązania omawianej trudności polega na rozszerzeniu
+zbioru <math> \mathbf{Num} </math> o dodatkowy element <math> \bot </math>:
+<math>
+n \, ::= \,\, \bot \,\,|\,\, 0 \,\,|\,\, 1 \,\,|\,\, \ldots
+</math>
+Wtedy nie musimy dodawać osobnego wariantu ostatniej reguły, ale
+za to <math> n = \bot </math> może sie pojawić w wyrażeniach.
+Dodatkowo, w tym rozwiązaniu warto poczynić umowę, że
+<math> s(x) = \bot </math> reprezentuje brak wartości zmiennej <math> x </math>.
+Wtedy stany są funkcjami całkowitymi z <math> \mathbf{Var} </math> w <math> \mathbf{Num} </math>
+przyjmującymi wartość różną od <math> \bot </math> tylko dla skończenie
+wielu elementów.
+'''(koniec uwagi)'''
+Na zakończenie ''scalamy'' semantykę dla <math> e \,\mathbf{then}\, x := n </math>
+z semantyką pozostałych wyrażeń:
+<math>
+\frac{e, s \,\Longrightarrow\, e', s'}
+{e \,\mathbf{then}\, x := n, s \,\Longrightarrow\, e' \,\mathbf{then}\, x:= n, s'}
+</math>
+<math>
+n' \,\mathbf{then}\, x := n, s \,\Longrightarrow\, n', s[x \mapsto 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). Spójrzmy 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>, gdyż 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 ====
+Semantyka będzie bardzo podobna do tej z poprzedniego zadania.
+Zasadnicza różnica dotyczy informacji przechowywanej w stanie.
+Dotychczas <math> s(x) \in \mathbf{Num} </math>, gdyż podwyrażenie <math> e </math> w
+<math> \mathbf{let}\, x = e \,\mathbf{in}\, \ldots </math> obliczało sie natychmiast.
+Jeśli chcemy opóżnic obliczenie tego podwyrażenia, to w
+<math> s(x) </math> powinniśmy zapamiętać całe (nieobliczone) wyrażenie <math> e </math>
+wraz ze stanem bieżącym.
+Czyli
+<math>
+\mathbf{State} \, = \, \mathbf{Var} \to \mathbf{Exp} \times \mathbf{State}.
+</math>
+Odpowiednia reguła dla wyrażenia <math> \mathbf{let}\, </math> to
+<math>
+\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2, s \,\Longrightarrow\, e_2, s[x \mapsto (e_1, s)].
+</math>
+Uważnego czytelnika zapewne zaniepokoił fakt, że <math> \mathbf{State} </math>
+stoi zarówno po lewej jak i po prawej stronie równania
+<math>
+\mathbf{State} \, = \, \mathbf{Var} \to \mathbf{Exp} \times \mathbf{State}.
+</math>
+Również zapis <math> s[x \mapsto (e_1, s)] </math> może wzbudzić niepokój,
+gdyż sugeruje on, iż <math> s(x) </math> zawiera, jako jeden z elementów pary,
+obiekt ''tego samego typu'' co <math> s </math>.
+Formalnego rozwiązania tego typu dylematów dostarcza teoria dziedzin.
+Natomiast na użytek semantyki operacyjnej wystarczy, jeśli
+uznamy, iż równanie
+<math>
+\mathbf{State} \, = \, \mathbf{Var} \to \mathbf{Exp} \times \mathbf{State}
+</math>
+stanowi skrótowy zapis następującej definicji.
+Zdefiniujmy <math> \mathbf{State}_0, \mathbf{State}_1, \ldots </math> następująco:
+<math>
+\mathbf{State}_{0} = \{ \emptyset \}
+</math>
+<math>
+\mathbf{State}_{n+1} = \mathbf{Var} \to_{\mathrm{fin}} \mathbf{Exp} \times \mathbf{State}_{n}
+</math>
+....
+=== Zadania domowe ===
+==== 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>
+==== Zadanie 5 ====
+Rozważ rozszerzenie języka z zadania 2 o wyrażenia boolowskie:
+<math>
+n \, ::= \,\, 0 \,\,|\,\, 1 \,\,|\,\, \ldots
+</math>
+<math>
+x \, ::= \,\, \ldots \, (identyfikatory) \, \ldots
+</math>
+<math>
+b \, ::= \,\,
+        \mathbf{true}   \,\,|\,\,
+        \mathbf{true}  \,\,|\,\,
+        e_1 \leq e_2  \,\,|\,\,
+        \neg b  \,\,|\,\,
+        b_1  \land  b_2
+</math>
+<math>
+e \,  ::=  \,\,
+        n   \,\,|\,\,
+        x   \,\,|\,\,
+        e_1 + e_2   \,\,|\,\,
+        \mathbf{if}\, b \,\mathbf{then}\, e_2 \,\mathbf{else}\, e_3  \,\,|\,\,
+        \mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2
+</math>
+Zaproponuj semantykę małych kroków dla tego języka.