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

← poprzednia edycja następna edycja →

WizualnieWikikod

Wersja z 16:14, 7 sie 2006

Zawartość

Tematem tych zajęć jest semantyka operacyjna wyrażeń (małe kroki).

Zadania z rozwiązaniami

Ćwiczenie 1

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.

{{rozwiazanie||roz1|

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 są 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, tranzycje postaci

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

oznaczające 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 (nie ma tzw. efektów ubocznych), więc to samo $s$ figuruje po lewej i prawej stronie strzałki.

Po drugie, tranzycje postaci $e, s ⟹ n$

będą 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: Tak naprawdę to druga postać tranzycji nie jest niezbędna, gdyż moglibyśmy umówić się, że konfiguracje końcowe to $𝐍 𝐮 𝐦 \times 𝐒 𝐭 𝐚 𝐭 𝐞$ . (koniec uwagi)

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

$n, s ⟹ n$

Zauważmy, że $n$ po prawej stronie to wyrażenie składające się ze stałej, podczas gdy $n$ po prawej stronie reprezentuje liczbę będącą wartością wyrażenia.

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łę:

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

Reguły tej postaci będziem zapisywac tak:

[[ \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 $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$

}}

Ćwiczenie 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 = 0 𝐢 𝐧 𝐥 𝐞 𝐭 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. Tym razem jednak uwzględnimy 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ć symbolem $\emptyset$ . 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}$

W szczególności, dla $y \neq x$ , $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) 𝐢 𝐧 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 𝐢 𝐧 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). Przedyskutujmy kilka wariantów.

Wariant 1

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ść pojawia 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 .$

Rozwiązanie to jest odrobinę nieeleganckie, gdyż prawie identyczne reguły musimy napisać dwukrotnie. Widać to np. w poniższych regułach, scalających 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]$

$n^{'} 𝐭 𝐡 𝐞 𝐧 x : = ⊥, s ⟹ n^{'}, s^{'} o ile s (x) jest określone i s^{'} = s ∖ {(x, s (x))}$

Wariant 2

Zanim przejdziemy do kolejnego wariantu, zastanówmy się czy istnieje inny sposób rozwiązania trudności związanej z $n = ⊥$ , który pozwalałby uniknąć wprowadzania dodatkowej konstrukcji $e 𝐭 𝐡 𝐞 𝐧 x : = ⊥$ . Pomysł może polegać na rozszerzeniu zbioru $𝐍 𝐮 𝐦$ o dodatkowy element $⊥$ :

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

Wtedy nie musimy pisać dwóch bardzo podobnych wariantów reguł. 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. Pewnym mankamentem jest to, że teraz $n = ⊥$ może pojawiać sie w wyrażeniach podobnie jak stałe. Tym niemniej nie musimy adaptować reguł dla stałych tak, aby radziły one sobie z $n = ⊥$ , ponieważ wyrażenia zawierające $⊥$ możemy również uważać za roszerzenie składni.

Jeśli jednak dopuścimy symbol $⊥$ w wyrażeniach, to możemy elegancko wybrnąć z sytuacji, rozszerzając operacje arytmetyczne na zbiór $𝐍 𝐮 𝐦 \cup {⊥}$ tak, aby zachowywały one nieokreśloność:

$n + ⊥ = ⊥ + n = ⊥$

Trzeba jednak w takim razie zadbać o to, aby wyrażenie $𝐥 𝐞 𝐭 x = e_{1} i n e_{2}$ obliczało się normalnie tylko wtedy, gdy wartość wyrażenia $e_{1}$ jest różna od $⊥$ .

Wariant 3

Zrewidujmy teraz podstawowe założenia, które dotychczas poczyniliśmy. Jednym z nich było przyjęcie ogólnej postaci tranzycji:

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

pozwalającej na zmianę stanu podczas obliczania wyrażenia. Czy faktycznie był to dobry pomysł? Czy moglibyśmy poradzić sobie przy pomocy tranzycji postaci

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

Spróbujmy! Oto nowa wersja jednej z reguł dla $𝐥 𝐞 𝐭 x = e_{1} 𝐢 𝐧 e_{2}$ dotycząca kroku wewnątrz $e_{1}$ :

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

Dotychczas nie ma problemu: podwyrażenie $e_{1}$ jest prawidłowo obliczane w stanie $s$ . Trudność pojawi się, gdy zakończymy obliczanie $e_{1}$ i przejdziemy do $e_{2}$ . Oto możliwa reguła:

$\frac{e, s [x \mapsto n] ⟹ e^{'}, s [x \mapsto n]}{𝐥 𝐞 𝐭 x = n 𝐢 𝐧 e, s ⟹ 𝐥 𝐞 𝐭 x = n 𝐢 𝐧 e^{'}, s} .$

Okazuje się, że wszystko jest w porządku. Wyrażenie $e$ obliczamy w prawidłowym stanie, tzn. z wartością $n$ przypisaną zmiennej $x$ . Mały krok w $e$ daje przyczynek do małego kroku w całym wyrażeniu, a przy tym stan pozostaje niezmieniony. Przy tym wogóle nie potrzebujemy przywracać poprzedniej wartości zmiennej $x$ , ponieważ $x$ zyskuje nową wartość tylko na potrzeby obliczania podwyrażenia $e$ ! Można na to również spojrzeć inaczej: informacja o nowej wartości $n$ dla zmiennej $x$ nie jest jawnie dodawana do stanu $s$ , ale jest przechowywana w składni wyrażenia $𝐥 𝐞 𝐭 x = n 𝐢 𝐧 \dots$ jako deklaracja $x = n$ . Na końcu musimy oczywiście pozbyć się tej deklaracji za pomocą następującej tranzycji:

$𝐥 𝐞 𝐭 x = n 𝐢 𝐧 n^{'}, s ⟹ n^{'}, s$

Podsumujmy. Okazuje się, że rozwiązanie nie było wcale łatwe, nawet dla tak prościutkiego języka. W przyszłości przekonamy się, że łatwiej jest poradzić sobie z zagadnieniem wiązania identyfikatorów w semantyce naturalnej (duże kroki). W wariancie 1 i 2 wprowadziliśmy do języka dodatkowe elementy, tak, by łatwiej było pisać reguły. W przyszłości będziemy czasem stosować takie podejście. Niekiedy jednak rozszerzanie języka będzie zabronione.

Zadania domowe

Zadanie 1

Zapisz wariant 2 semantyki z poprzedniego zadania.

Zadanie 2

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 3

Rozważ rozszerzenie języka wyrażeń 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. Rozważ różne strategie obliczania wyrażeń boolowskich, oraz podejście leniwe. Na przykład w strategii lewostronnej dla $b_{1} \land b_{2}$ , gdy $b_{1}$ zostało obliczone do $𝐭 𝐫 𝐮 𝐞$ , nie ma wogóle potrzeby obliczania $b_{2}$ .

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

Wersja z 16:14, 7 sie 2006

Spis treści

Zawartość

Zadania z rozwiązaniami

Przykłady

Wariant 1

Wariant 2

Wariant 3

Zadania domowe

Zadanie 1

Zadanie 2

Zadanie 3

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia

@@ Linia 9: / Linia 9: @@
-==== Zadanie 1 (przygotowawcze) ====
+{{cwiczenie|1|cw1|
 Rozważmy bardzo prosty język wyrażeń, którego składnia opisana jest
@@ Linia 30: / Linia 31: @@
 </math>
-Wynikiem wyrażenienia warunkowego <math> \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
+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
+<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>.
+przypadku wynikiem jest wartość wyrażenia <math>e_3</math>.
 Zaproponuj semantykę operacyjną (małe kroki) dla tego języka.
+}}
-==== Rozwiązanie ====
+{{rozwiazanie||roz1|
 Zacznijmy od ustalenia notacji i dziedzin syntaktycznych.
-Niech <math> \mathbf{Num} </math> oznacza zbiór stałych liczbowych,
+Niech <math>\mathbf{Num}</math> oznacza zbiór stałych liczbowych,
-<math> n \in \mathbf{Num} = \{ 0, 1, \ldots \} </math>.
+<math>n \in \mathbf{Num} = \{ 0, 1, \ldots \}</math>.
-Podobnie, niech <math> \mathbf{Var} </math> oznacza zbiór identyfikatorów, które
+Podobnie, niech <math>\mathbf{Var}</math> oznacza zbiór identyfikatorów, które
-mogą być nazwami zmiennych; <math> x \in \mathbf{Var} </math>.
+mogą być nazwami zmiennych; <math>x \in \mathbf{Var}</math>.
-Wreszcie, niech <math> \mathbf{Exp} </math> oznacza zbiór wyrażeń;
+Wreszcie, niech <math>\mathbf{Exp}</math> oznacza zbiór wyrażeń;
-<math> e \in \mathbf{Exp} </math>.
+<math>e \in \mathbf{Exp}</math>.
 Dla ułatwienia zapisywania reguł zakładamy, ze stałe
-liczbowe są wyrażeniami, czyli <math> \mathbf{Num} \subseteq \mathbf{Exp} </math>.
+liczbowe są 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>.
+z <math>\mathbf{Var}</math> do <math>\mathbf{Num}</math>.
-Oznaczmy przez <math> \mathbf{State} </math> zbiór wszystkich takich funkcji;
+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>.
+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.
@@ Linia 66: / Linia 67: @@
 </math>
-oznaczające mały krok w trakcie obliczania wyrażenia <math> e </math>
+oznaczające 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
+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
+<math>e'</math>. Stan nie ulega zmiania podczas obliczania wyrażenia
 (nie ma tzw. ''efektów ubocznych''),
-więc to samo <math> s </math> figuruje po lewej i prawej stronie strzałki.
+więc to samo <math>s</math> figuruje po lewej i prawej stronie strzałki.
 Po drugie, tranzycje postaci
@@ Linia 77: / Linia 78: @@
 </math>
-będą oznaczaczać, że wyrażenie <math> e </math> jest już policzone,
+będą oznaczaczać, że wyrażenie <math>e</math> jest już policzone,
-a jego wartością jest <math> n </math>.
+a jego wartością jest <math>n</math>.
 Zatem przyjmijmy, że zbiór konfiguracji to
@@ Linia 86: / Linia 87: @@
 </math>
-a konfiguracje końcowe to <math> \mathbf{Num} </math>.
+a konfiguracje końcowe to <math>\mathbf{Num}</math>.
 '''Uwaga:''' Tak naprawdę to druga postać tranzycji nie jest
 niezbędna, gdyż moglibyśmy umówić się, że konfiguracje końcowe
-to <math> \mathbf{Num} \times \mathbf{State} </math>.
+to <math>\mathbf{Num} \times \mathbf{State}</math>.
 '''(koniec uwagi)'''
@@ Linia 114: / Linia 115: @@
 </math>
-Zauważmy, że <math> n </math> po prawej stronie to wyrażenie składające się
+Zauważmy, że <math>n</math> po prawej stronie to wyrażenie składające się
-ze stałej, podczas gdy <math> n </math> po prawej stronie reprezentuje liczbę
+ze stałej, podczas gdy <math>n</math> po prawej stronie reprezentuje liczbę
 będącą wartością wyrażenia.
@@ Linia 124: / Linia 125: @@
 </math>
-Teraz zajmiemy się dodawaniem <math> e_1 + e_2 </math>. Ponieważ semantyka jest w stylu małych
+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?
+<math>e_1</math> czy drugi?
 Jeśli wybierzemy lewy (strategia ''lewostronna''), otrzymamy regułę:
@@ Linia 142: / Linia 143: @@
 </math>
-Czyli mały krok w <math> e_1 </math> stanowi też mały krok w <math> 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>:
+Po zakończeniu obliczania <math>e_1</math> przechodzimy do <math>e_2</math>:
 <math>
@@ Linia 158: / Linia 159: @@
 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>.
+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
+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>.
+dobrze pisać np. <math>{\mathrm{add}}(e_1, e_2)</math>.
-Inna możliwą strategią obliczania <math> e_1 + e_2 </math> jest strategia
+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:
@@ Linia 176: / Linia 177: @@
 </math>
-Ponadto, jeśli przyjmiemy regułę pierwszą (dla <math> e_1 </math>), trzecią
+Ponadto, jeśli przyjmiemy regułę pierwszą (dla <math>e_1</math>), trzecią
-i czwartą (dla <math> e_2 </math>), otrzymamy strategię
+i czwartą (dla <math>e_2</math>), otrzymamy strategię
-''równoległą'', polegającą na obliczaniu jednocześnie <math> e_1 </math> i
+''równoległą'', polegającą na obliczaniu jednocześnie <math>e_1</math> i
-<math> e_2 </math>:
+<math>e_2</math>:
 <math>
@@ Linia 204: / Linia 205: @@
 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ść
+<math>e_1</math> i <math>e_2</math> nie wpływa w tym przypadku na końcową wartość
 całego wyrażenia.
@@ Linia 223: / Linia 224: @@
+}}
-==== Zadanie 2 ====
+{{cwiczenie|2|cw2|
 Rozszerzmy język wyrażeń z poprzedniego zadania o jedną konstrukcję
@@ Linia 235: / Linia 237: @@
 </math>
-Wyrażenie <math> \mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2 </math> zawiera w sobie deklarację
+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
+<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>
+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:
+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
+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>.
+<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
+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>;
+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.
@@ Linia 250: / Linia 252: @@
 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
+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''
+odwołania do <math>x</math> wewnątrz <math>e</math> odnoszą się do ''najbliższej''
-deklaracji zmiennej <math> x </math>.
+deklaracji zmiennej <math>x</math>.
 Zakładamy, że na początku wartości wszystkich zmiennych są
@@ Linia 278: / Linia 280: @@
 \quad \quad \mapsto \quad \quad \mbox{wynik} = 4
 </math>
+}}
-==== Rozwiązanie ====
+{{rozwiazanie||roz2|
@@ Linia 288: / Linia 290: @@
 Tym razem jednak
 uwzględnimy 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>.
+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:
+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ć symbolem <math> \emptyset </math>.
+pusta funkcja częściowa, który będziemy oznaczać symbolem <math>\emptyset</math>.
-Wartość wyrażenia <math> e </math> w stanie początkowym wynosi <math> n </math>
+Wartość wyrażenia <math>e</math> w stanie początkowym wynosi <math>n</math>
 o ile zachodzi:
@@ Linia 309: / Linia 311: @@
 </math>
-Tranzycja ta oznacza mały krok w trakcie obliczania wyrażenia <math> e </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
+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>.
+<math>e'</math> a nowym stanem jest <math>s'</math>.
 Stan może się teraz zmienić na skutek deklaracji zmiennych.
@@ Linia 322: / Linia 324: @@
 Następnie dodajemy reguły dla wyrażenia
-<math> \mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2 </math>.
+<math>\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2</math>.
-Gdy <math> e_1 </math> jest już obliczne, wyatarczy reguła:
+Gdy <math>e_1</math> jest już obliczne, wyatarczy reguła:
 <math>
@@ Linia 329: / Linia 331: @@
 </math>
-Notacja <math> s[x \mapsto n] </math> oznacza stan <math> s </math>, który zmodyfikowano
+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>,
+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,
+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
@@ Linia 344: / Linia 346: @@
 W szczególności,
-dla <math> y \neq x </math>, <math> s[x \mapsto n](y) </math> jest określone wtedy i tylko
+dla <math>y \neq x</math>, <math>s[x \mapsto n](y)</math> jest określone wtedy i tylko
-wtedy, gdy <math> s(y) </math> jest określone.
+wtedy, gdy <math>s(y)</math> jest określone.
-Natomiast aby obliczyc <math> e_1 </math> potrzebujemy reguły:
+Natomiast aby obliczyc <math>e_1</math> potrzebujemy reguły:
 <math>
@@ Linia 354: / Linia 356: @@
 </math>
-Zwróćmy uwagę, że stan <math> s' </math> może być różny od <math> 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
+np. dlatego, że wewnątrz <math>e_1</math> znajduje się podwyrażenie
-<math> \mathbf{let}\, y = \ldots </math>.
+<math>\mathbf{let}\, y = \ldots</math>.
 '''Pytanie:''' czy taka semantyka jest poprawna?
@@ Linia 368: / Linia 370: @@
 Według naszych intencji to wyrażenie nie ma wartości, gdyż ostatnie
-odwołanie do <math> z </math> jest błędne.
+odwołanie do <math>z</math> jest błędne.
 Natomiast według powyższych reguł mamy
@@ Linia 380: / Linia 382: @@
 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>
+<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).
 Przedyskutujmy kilka wariantów.
@@ Linia 403: / Linia 405: @@
 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.
+<math>e_2</math> a następnie na przypisaniu zmiennej <math>x</math> danej wartości.
 Rozszerzmy zatem składnię następujaco:
@@ Linia 412: / Linia 414: @@
 </math>
-Zauważmy, że wyrażenie <math> e \,\mathbf{then}\, x:= n </math> jest w pewnym sensie dualne
+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
+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
+między nimi to kolejność obliczenia <math>e</math> i przypisania wartości
-na zmienną <math> x </math>.
+na zmienną <math>x</math>.
 Oto nowa reguła
@@ Linia 423: / Linia 425: @@
 </math>
-Pewna trudność pojawia się w sytuacji, gdy <math> s(x) </math> jest
+Pewna trudność pojawia się w sytuacji, gdy <math>s(x)</math> jest
-nieokreślone, czyli gdy zmienna <math> x </math> jest niezainicjowana -- reguła
+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>:
+konstrukcji <math>e \,\mathbf{then}\, x := n</math>:
 <math>
@@ Linia 436: / Linia 438: @@
 </math>
-gdzie symbol <math> \bot </math> oznacza brak wartości.
+gdzie symbol <math>\bot</math> oznacza brak wartości.
 Dodajemy również regułę:
@@ Linia 446: / Linia 448: @@
 Rozwiązanie to jest odrobinę nieeleganckie, gdyż prawie identyczne reguły
 musimy napisać dwukrotnie.
-Widać to np. w poniższych regułach, ''scalających'' semantykę dla <math> e \,\mathbf{then}\, x := n </math>
+Widać to np. w poniższych regułach, ''scalających'' semantykę dla <math>e \,\mathbf{then}\, x := n</math>
 z semantyką pozostałych wyrażeń:
@@ Linia 467: / Linia 469: @@
 Zanim przejdziemy do kolejnego wariantu, zastanówmy się czy
-istnieje inny sposób rozwiązania trudności związanej z <math> n =
+istnieje inny sposób rozwiązania trudności związanej z <math>n =
-\bot </math>, który pozwalałby uniknąć wprowadzania dodatkowej konstrukcji
+\bot</math>, który pozwalałby uniknąć wprowadzania dodatkowej konstrukcji
-<math> e \,\mathbf{then}\, x := \bot </math>.
+<math>e \,\mathbf{then}\, x := \bot</math>.
 Pomysł może polegać na rozszerzeniu
-zbioru <math> \mathbf{Num} </math> o dodatkowy element <math> \bot </math>:
+zbioru <math>\mathbf{Num}</math> o dodatkowy element <math>\bot</math>:
 <math>
@@ Linia 479: / Linia 481: @@
 Wtedy nie musimy pisać dwóch bardzo podobnych wariantów reguł.
 Dodatkowo, w tym rozwiązaniu warto poczynić umowę, że
-<math> s(x) = \bot </math> reprezentuje brak wartości zmiennej <math> x </math>.
+<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>
+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
+przyjmującymi wartość różną od <math>\bot</math> tylko dla skończenie
 wielu elementów.
 Pewnym mankamentem jest to, że teraz
-<math> n = \bot </math> może pojawiać sie w wyrażeniach podobnie jak stałe.
+<math>n = \bot</math> może pojawiać sie w wyrażeniach podobnie jak stałe.
 Tym niemniej nie musimy adaptować reguł dla stałych tak, aby radziły
-one sobie z <math> n = \bot </math>, ponieważ wyrażenia zawierające
+one sobie z <math>n = \bot</math>, ponieważ wyrażenia zawierające
-<math> \bot </math> możemy również uważać za roszerzenie składni.
+<math>\bot</math> możemy również uważać za roszerzenie składni.
-Jeśli jednak dopuścimy symbol <math> \bot </math> w wyrażeniach, to możemy
+Jeśli jednak dopuścimy symbol <math>\bot</math> w wyrażeniach, to możemy
 elegancko wybrnąć z sytuacji, rozszerzając operacje arytmetyczne
-na zbiór <math> \mathbf{Num} \cup \{ \bot \} </math> tak, aby zachowywały one
+na zbiór <math>\mathbf{Num} \cup \{ \bot \}</math> tak, aby zachowywały one
 nieokreśloność:
@@ Linia 498: / Linia 500: @@
 </math>
-Trzeba jednak w takim razie zadbać o to, aby wyrażenie <math> \mathbf{let}\, x = e_1
+Trzeba jednak w takim razie zadbać o to, aby wyrażenie <math>\mathbf{let}\, x = e_1
-in e_2 </math> obliczało się normalnie tylko wtedy, gdy wartość
+in e_2</math> obliczało się normalnie tylko wtedy, gdy wartość
-wyrażenia <math> e_1 </math> jest różna od <math> \bot </math>.
+wyrażenia <math>e_1</math> jest różna od <math>\bot</math>.
@@ Linia 520: / Linia 522: @@
 </math>
-Spróbujmy! Oto nowa wersja jednej z reguł dla <math> \mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2 </math>
+Spróbujmy! Oto nowa wersja jednej z reguł dla <math>\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2</math>
-dotycząca kroku wewnątrz <math> e_1 </math>:
+dotycząca kroku wewnątrz <math>e_1</math>:
 <math>
@@ Linia 528: / Linia 530: @@
 </math>
-Dotychczas nie ma problemu: podwyrażenie <math> e_1 </math> jest
+Dotychczas nie ma problemu: podwyrażenie <math>e_1</math> jest
-prawidłowo obliczane w stanie <math> s </math>. Trudność pojawi się, gdy
+prawidłowo obliczane w stanie <math>s</math>. Trudność pojawi się, gdy
-zakończymy obliczanie <math> e_1 </math> i przejdziemy do <math> e_2 </math>.
+zakończymy obliczanie <math>e_1</math> i przejdziemy do <math>e_2</math>.
 Oto możliwa reguła:
@@ Linia 538: / Linia 540: @@
 </math>
-Okazuje się, że wszystko jest w porządku. Wyrażenie <math> e </math>
+Okazuje się, że wszystko jest w porządku. Wyrażenie <math>e</math>
-obliczamy w prawidłowym stanie, tzn. z wartością <math> n </math>
+obliczamy w prawidłowym stanie, tzn. z wartością <math>n</math>
-przypisaną zmiennej <math> x </math>.
+przypisaną zmiennej <math>x</math>.
-Mały krok w <math> e </math> daje przyczynek do małego kroku w całym
+Mały krok w <math>e</math> daje przyczynek do małego kroku w całym
 wyrażeniu, a przy tym stan pozostaje niezmieniony.
 Przy tym wogóle nie potrzebujemy przywracać poprzedniej wartości
-zmiennej <math> x </math>, ponieważ <math> x </math> zyskuje nową wartość
+zmiennej <math>x</math>, ponieważ <math>x</math> zyskuje nową wartość
-''tylko'' na potrzeby obliczania podwyrażenia <math> e </math>!
+''tylko'' na potrzeby obliczania podwyrażenia <math>e</math>!
 Można na to również spojrzeć inaczej: informacja o nowej wartości
-<math> n </math>  dla zmiennej <math> x </math> nie jest jawnie dodawana do stanu
+<math>n</math>  dla zmiennej <math>x</math> nie jest jawnie dodawana do stanu
-<math> s </math>, ale jest przechowywana w składni wyrażenia
+<math>s</math>, ale jest przechowywana w składni wyrażenia
-<math> \mathbf{let}\, x = n \,\mathbf{in}\, \ldots </math> jako deklaracja <math> x = n </math>.
+<math>\mathbf{let}\, x = n \,\mathbf{in}\, \ldots</math> jako deklaracja <math>x = n</math>.
 Na końcu musimy oczywiście pozbyć się tej deklaracji za pomocą
 następującej tranzycji:
@@ Linia 567: / Linia 569: @@
+}}
 == Zadania domowe ==
@@ Linia 585: / Linia 588: @@
 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ł
+wyrażenia <math>e</math> w stanie <math>s</math> jest niemożliwe bo wystąpił
 błąd, to
@@ Linia 626: / Linia 629: @@
 Zaproponuj semantykę małych kroków dla tego języka.
 Rozważ różne strategie obliczania wyrażeń boolowskich, oraz podejście leniwe.
-Na przykład w strategii lewostronnej dla <math> b_1 \land b_2 </math>,
+Na przykład w strategii lewostronnej dla <math>b_1 \land b_2</math>,
-gdy <math> b_1 </math> zostało obliczone do <math> \mathbf{true} </math>, nie ma wogóle potrzeby
+gdy <math>b_1</math> zostało obliczone do <math>\mathbf{true}</math>, nie ma wogóle potrzeby
-obliczania <math> b_2 </math>.
+obliczania <math>b_2</math>.