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

← poprzednia edycja

WizualnieWikikod

Aktualna wersja na dzień 21:29, 11 wrz 2023

Zawartość

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

Semantyka operacyjna wyrażeń

Ć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.

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, że 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ąć, że stan to funkcja z $𝐕 𝐚 𝐫$ do $𝐍 𝐮 𝐦$ . Oznaczmy przez $𝐒 𝐭 𝐚 𝐭 𝐞$ zbiór wszystkich takich funkcji; stany oznaczać 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 zmianie 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ę, druga postać tranzycji nie jest niezbędna, gdyż moglibyśmy umówić się, że konfiguracje końcowe to $𝐍 𝐮 𝐦 \times 𝐒 𝐭 𝐚 𝐭 𝐞$ .

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

$n, s ⟹, n$

Symbol $n$ po lewej stronie to wyrażenie składające się ze stałej liczbowej, 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ędziemy zapisywać tak:

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

Zwróćmy tutaj uwagę na 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ą abstrakcyjną, więc zamiast $e_{1} + e_{2}$ moglibyśmy równie dobrze pisać np. $a d d (e_{1}, e_{2})$ , a wtedy reguła wyglądałaby tak:

$a d d (n_{1}, n_{2}), s ⟹, n, s o ile n = n_{1} + n_{2}$

Inną 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ą za zmienną $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 (statyczne) reguły przesłaniania zmiennych, np. jeśli w $e_{2}$ występuje podwyrażenie $𝐥 𝐞 𝐭 x = e 𝐢 𝐧 e^{'}$ , to deklaracja $x = e$ "przesłania" deklarację $x = e_{1}$ w wyrażeniu $e^{'}$ .

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.

{{przyklad|||

$𝐥 𝐞 𝐭 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$

$𝐥 𝐞 𝐭 z = 5 𝐢 𝐧 x + z \mapsto 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 nieco 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 rozszerzyć 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ż obliczone, wystarczy 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. Formalnie

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

Wyrażenie $e 𝐭 𝐡 𝐞 𝐧 x : = n$ jest w pewnym sensie dualne do $𝐥 𝐞 𝐭 x = n 𝐢 𝐧 e$ , gdyż jedyna (choć 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ć się 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} 𝐢 𝐧 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

Ćwiczenie 1

Zapisz wariant 2 semantyki z poprzedniego zadania.

Ćwiczenie 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$

Ćwiczenie 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 $𝐟 𝐚 𝐥 𝐬 𝐞$ , w podejściu leniwym nie ma wogóle potrzeby obliczania $b_{2}$ .

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

Aktualna wersja na dzień 21:29, 11 wrz 2023

Zawartość

Semantyka operacyjna wyrażeń

Zadania domowe

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia

@@ Linia 1: / Linia 1: @@
+== Zawartość ==
+Tematem tych zajęć jest semantyka operacyjna wyrażeń (małe kroki).
-== Zawarto¶æ ==
-Tematem tych zajêæ jest semantyka operacyjna wyra¿eñ (ma³e kroki).
+== Semantyka operacyjna wyrażeń ==
-== Semantyka operacyjna wyra¿eñ ==
 {{cwiczenie|1|cw1|
-Rozwa¿my bardzo prosty jêzyk wyra¿eñ, którego sk³adnia opisana jest
+Rozważmy bardzo prosty język wyrażeń, którego składnia opisana jest następującą gramatyką:
-nastêpuj±c± gramatyk±:
 <math>
@@ Linia 30: / Linia 27: @@
 </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 <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>.
-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.
+Zaproponuj semantykę operacyjną (małe kroki) dla tego języka.
 }}
+<div class="mw-collapsible mw-made=collapsible mw-collapsed">
-{{rozwiazanie||roz1|
+<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie</span>
+<div class="mw-collapsible-content" style="display:none">
-<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
 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 mogą być nazwami zmiennych; <math>x \in \mathbf{Var}</math>.
-Podobnie, niech <math>\mathbf{Var}</math> oznacza zbiór identyfikatorów, które
+Wreszcie, niech <math>\mathbf{Exp}</math> oznacza zbiór wyrażeń; <math>e \in \mathbf{Exp}</math>.
-mog± byæ nazwami zmiennych; <math>x \in \mathbf{Var}</math>.
+Dla ułatwienia zapisywania reguł zakładamy, że stałe  liczbowe są wyrażeniami, czyli <math>\mathbf{Num} \subseteq \mathbf{Exp}</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 s± wyra¿eniami, czyli <math>\mathbf{Num} \subseteq \mathbf{Exp}</math>.
-Bêdziemy potrzebowaæ zbioru ''stanów'', opisuj±cych warto¶ci
+Będziemy potrzebować zbioru "stanów", opisujących wartości przypisane zmiennym.
-przypisane zmiennym.
+Najprostszym rozwiązaniem jest przyjąć, że stan to funkcja z <math>\mathbf{Var}</math> do <math>\mathbf{Num}</math>.
-Najprostszym rozwi±zaniem jest przyj±c, ¿e stan to funkcja
+Oznaczmy przez <math>\mathbf{State}</math> zbiór wszystkich takich funkcji; stany oznaczać będziemy przez <math>s, s_1, s', \ldots \in \mathbf{State}</math>.
-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.
+W naszej semantyce będziemy potrzebowac tranzycji dwóch postaci.
 Po pierwsze, tranzycje postaci
 <math>
-e, s \,\Longrightarrow\, e', s
+e, s \,\Longrightarrow, e', s
 </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 <math>e'</math>.
-w stanie <math>s</math>, w wyniku którego <math>e</math> wyewoluowa³o do
+Stan nie ulega zmianie 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.
-<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.
 Po drugie, tranzycje postaci
 <math>
-e, s \,\Longrightarrow\, n
+e, s \,\Longrightarrow, n
 </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
+Zatem przyjmijmy, że zbiór konfiguracji to
 <math>
@@ Linia 87: / Linia 70: @@
 </math>
-a konfiguracje koñcowe to <math>\mathbf{Num}</math>.
+a konfiguracje końcowe to <math>\mathbf{Num}</math>.
 {{
 uwaga||uwaga1|
-Tak naprawdê to druga postaæ tranzycji nie jest
+Tak naprawdę, 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>.
-niezbêdna, gdy¿ mogliby¶my umówiæ siê, ¿e konfiguracje koñcowe
-to <math>\mathbf{Num} \times \mathbf{State}</math>.
 }}
-Najprostsze s± tranzycje prowadz±ce do konfiguracji koñcowej:
+Najprostsze są tranzycje prowadzące do konfiguracji końcowej:
 <math>
-n, s \,\Longrightarrow\, n
+n, s \,\Longrightarrow, n
 </math>
-Symbol <math>n</math> po lewej stronie to wyra¿enie sk³adaj±ce siê
+Symbol <math>n</math> po lewej stronie to wyrażenie składające się ze stałej liczbowej, podczas gdy <math>n</math> po prawej stronie reprezentuje liczbę będącą wartością wyrażenia.
-ze sta³ej liczbowej, podczas gdy <math>n</math> po prawej stronie reprezentuje liczbê
-bêd±c± warto¶ci± wyra¿enia.
-Zmienna oblicza siê do swojej warto¶ci w bie¿±cym stanie:
+Zmienna oblicza się do swojej wartości w bieżącym stanie:
 <math>
-x, s \,\Longrightarrow\, n, s \quad \mbox{ o ile } s(x) = n.
+x, s \,\Longrightarrow, n, s \quad \mbox{ o ile } s(x) = n</math>
-</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?
-kroków, musimy zdecydowaæ siê czy najpierw obliczyæ pierwszy (lewy) sk³adnik
+Jeśli wybierzemy lewy (strategia "lewostronna"), otrzymamy regułę:
-<math>e_1</math> czy drugi?
-Je¶li wybierzemy lewy (strategia ''lewostronna''), otrzymamy regu³ê:
 <math>
-e_1 + e_2, s \,\Longrightarrow\, e'_1 + e_2, s
+e_1 + e_2, s \,\Longrightarrow, e'_1 + e_2, s
 \quad \mbox{ o ile } \quad
-e_1, s \,\Longrightarrow\, e'_1, s.
+e_1, s \,\Longrightarrow, e'_1, s</math>
-</math>
-Regu³y tej postaci bêdziemy zapisywaæ tak:
+Reguły tej postaci będziemy zapisywać tak:
 <math>
-\frac{e_1, s \,\Longrightarrow\, e'_1, s}
+\frac{e_1, s \,\Longrightarrow, e'_1, s}
-      {e_1 + e_2, s \,\Longrightarrow\, e'_1 + e_2, 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>.
+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>
-\frac{e_2, s \,\Longrightarrow\, e'_2, s}
+\frac{e_2, s \,\Longrightarrow, e'_2, s}
-{n + e_2, s \,\Longrightarrow\, n + e'_2, s}.
+{n + e_2, s \,\Longrightarrow, n + e'_2, s}</math>
-</math>
-A na koñcu dodajemy:
+A na końcu dodajemy:
 <math>
-n_1 + n_2, s \,\Longrightarrow\, n, s \quad \mbox{ o ile } n = n_1 + n_2.
+n_1 + n_2, s \,\Longrightarrow, n, s \quad \mbox{ o ile } n = n_1 + n_2</math>
-</math>
-Zwróæmy tutaj uwagê na pewn± subtelno¶æ, dotycz±c± dwóch wyst±pieñ
+Zwróćmy tutaj uwagę na pewną subtelność, dotyczącą dwóch wystąpień symbolu <math>+</math>: pierwsze wystąpienie oznacza jedną z konstrukcji składniowych języka, a drugie oznacza operację dodawania w zbiorze <math>\mathbf{Num}</math>.
-symbolu <math>+</math>: pierwsze wyst±pienie oznacza jedn± z konstrukcji sk³adniowych
+Pozwalamy sobie na taką kolizję oznaczeń, gdyż nie powinna ona prowadzić do niejednoznaczności. Pamiętajmy, że składnia języka jest składnią abstrakcyjną, więc zamiast <math>e_1 + e_2</math> moglibyśmy równie dobrze pisać np. <math>{\mathrm{add}}(e_1, e_2)</math>, a wtedy reguła wyglądałaby tak:
-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± abstrakcyjn±, wiêc zamiast <math>e_1 + e_2</math> mogliby¶my równie
-dobrze pisaæ np. <math>{\mathrm{add}}(e_1, e_2)</math> a wtedy regu³a
-wygl±da³aby tak:
 <math>
-\mathrm{add}(n_1, n_2), s \,\Longrightarrow\, n, s \quad \mbox{ o ile } n = n_1 + n_2.
+\mathrm{add}(n_1, n_2), s \,\Longrightarrow, n, s \quad \mbox{ o ile } n = n_1 + n_2</math>
-</math>
-Inn± mo¿liw± strategi± obliczania <math>e_1 + e_2</math> jest strategia
+Inną 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:
-''prawostronna'', któr± otrzymujemy zastêpuj±c pierwsze dwie z trzech
-powy¿szych regu³ przez:
 <math>
-\frac{e_2, s \,\Longrightarrow\, e'_2, s}
+\frac{e_2, s \,\Longrightarrow, e'_2, s}
-      {e_1 + e_2, s \,\Longrightarrow\, e_1 + e'_2}
+      {e_1 + e_2, s \,\Longrightarrow, e_1 + e'_2}
 \quad \quad
-\frac{e_1, s \,\Longrightarrow\, e'_1, s}
+\frac{e_1, s \,\Longrightarrow, e'_1, s}
-      {e_1 + n, s \,\Longrightarrow\, e'_1 + n, s}.
+      {e_1 + n, s \,\Longrightarrow, e'_1 + n, s}</math>
-</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ę "równoległą", polegającą na obliczaniu jednocześnie <math>e_1</math> i <math>e_2</math>:
-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}
+\frac{e_1, s \,\Longrightarrow, e'_1, s}
-      {e_1 + e_2, s \,\Longrightarrow\, e'_1 + e_2, s}
+      {e_1 + e_2, s \,\Longrightarrow, e'_1 + e_2, s}
 \quad \quad
-\frac{e_2, s \,\Longrightarrow\, e'_2, s}
+\frac{e_2, s \,\Longrightarrow, e'_2, s}
-      {e_1 + e_2, s \,\Longrightarrow\, e_1 + e'_2}
+      {e_1 + e_2, s \,\Longrightarrow, e_1 + e'_2}
 \quad \quad
-n_1 + n_2, s \,\Longrightarrow\, n, s \quad \mbox{ o ile } n = n_1 + n_2.
+n_1 + n_2, s \,\Longrightarrow, n, s \quad \mbox{ o ile } n = n_1 + n_2</math>
-</math>
-Bardziej precyzyjnie mówi±c, ma³e kroki obliczaj±ce
+Bardziej precyzyjnie mówiąc, małe kroki obliczające obydwa podwyrażenia przeplatają się, i to w dowolny sposób.
-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.
-Ta dowolno¶æ prowadzi do ''niedeterminizmu'', czyli do sytuacji, gdy
+Jest tak, gdyż możemy mieć do wyboru dwie różne tranzycje
-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
+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.
+e_1 + e_2, s \,\Longrightarrow, e_1 + e'_2, s</math>
-</math>
-Zauwa¿my natomiast, ¿e kolejno¶æ przeplatania siê ma³ych kroków obliczaj±cych
+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.
-<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.
+Na koniec reguły dla wyrażenia warunkowego.
 <math>
-\frac{e_1, s \,\Longrightarrow\, e'_1, s}
+\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}
+      {\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
+\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
+\mathbf{if}\, n \,\mathbf{then}\, e_2 \,\mathbf{else}\, e_3, s \,\Longrightarrow, e_3, s \quad \mbox{ o ile } n = 0
 </math>
 </div></div>
-}}
 {{cwiczenie|2|cw2|
+}}
-Rozszerzmy jêzyk wyra¿eñ z poprzedniego zadania o jedn± konstrukcjê
+Rozszerzmy język wyrażeń z poprzedniego zadania o jedną konstrukcję
 <math>
@@ Linia 229: / Linia 184: @@
 </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 identyfikatorów w naszym języku.
-<math>x = e_1</math>, która stanowi mechanizm wi±zania
+Deklaracja <math>x = e_1</math> wprowadza nową zmienną <math>x</math> oraz przypisuje jej wartość.
-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ą <font color=red>za</font> zmienną <math>x</math>, a następnie oblicza wyrażenie <math>e_2</math>.
-Deklaracja <math>x = e_1</math> wprowadza now± zmienn± <math>x</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>;
-oraz przypisuje jej warto¶æ.
+Ogólniej, odwołania do zmiennej w wyrażeniu odnoszą się do "najbliższej" (najbardziej zagnieżdzonej) deklaracji tej zmiennej.
-Warto¶æ wyra¿enia <math>\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2</math> obliczamy nastêpuj±co:
+Taki mechanizm wiązania identyfikatorów nazywamy ''wiązaniem statycznym''.
-najpierw oblicza siê warto¶æ <math>e_1</math>, podstawia j± na zmienna
+Przyjmujemy zwykłe (statyczne) reguły przesłaniania zmiennych, np. jeśli w <math>e_2</math> występuje podwyrażenie <math>\mathbf{let}\, x = e \,\mathbf{in}\, e'</math>, to
-<math>x</math>, a nastêpnie oblicza wyra¿enie <math>e_2</math>.
+deklaracja <math>x = e</math> "przesłania" deklarację <math>x = e_1</math> w wyrażeniu <math>e'</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>;
+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.
-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 (statyczne) regu³y przes³aniania zmiennych, np.
-je¶li w <math>e_2</math> wystêpuje podwyra¿enie <math>\mathbf{let}\, x = e \,\mathbf{in}\, e'</math> to
-deklaracja <math>x = e</math> ''przes³ania'' deklaracjê <math>x = e_1</math>
-w wyra¿eniu <math>e'</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.
-}}
@@ Linia 267: / Linia 210: @@
 <math>
-\mathbf{let}\, z = 5 \,\mathbf{in}\, x+z
+\mathbf{let}\, z = 5 \,\mathbf{in}\, x+z \quad \quad \mapsto \quad \quad \mbox{ brak wyniku, odwołanie do niezainicjowanej zmiennej } x
-\quad \quad \mapsto \quad \quad \mbox{brak wyniku; odwo³anie do niezainicjowanej
-zmiennej}\, x
 </math>
@@ Linia 276: / Linia 217: @@
 \quad \quad \mapsto \quad \quad \mbox{wynik} = 4
 </math>
-}}
+<div class="mw-collapsible mw-made=collapsible mw-collapsed">
+<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie</span>
+<div class="mw-collapsible-content" style="display:none">
-{{rozwiazanie||roz2|
+Podobnie jak poprzednio, stan powinien opisywać wartości przypisane zmiennym.
+Tym razem jednak uwzględnimy niezainicjowane zmienne, czyli zmienne bez żadnej wartości.
-<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
+Przyjmijmy zatem, że stan to skończona funkcja częściowa z <math>\mathbf{Var}</math> do <math>\mathbf{Num}</math>.
-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 <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.
+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>, o ile zachodzi:
-Warto¶æ wyra¿enia <math>e</math> w stanie pocz±tkowym wynosi <math>n</math>
-o ile zachodzi:
 <math>
-e, \emptyset \,\Longrightarrow^{*}\, n.
+e, \emptyset \,\Longrightarrow^{*}\, n</math>
-</math>
-Bêdziemy potrzebowac tranzycji dwóch postaci, podobnie jak poprzednio,
+Będziemy potrzebowac tranzycji dwóch postaci, podobnie jak poprzednio, ale pierwsza postać będzie nieco ogólniejsza:
-ale pierwsza postaæ bêdzie trochê ogólniejsza:
 <math>
-e, s \,\Longrightarrow\, e', s'.
+e, s \,\Longrightarrow, e', s'</math>
-</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 <math>e'</math>, a nowym stanem jest <math>s'</math>.
-w stanie <math>s</math>, w wyniku którego <math>e</math> wyewoluowa³o do
+Stan może się teraz zmienić na skutek deklaracji zmiennych.
-<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.
+Spróbujmy rozszerzyć semantykę z poprzedniego zadania.
-Poniewa¿ stan jest funkcj± czê¶ciow±, musimy zmieniæ niektóre regu³y, np.
+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
+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
+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ż obliczone, wystarczy reguła:
-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].
+\mathbf{let}\, x = n \,\mathbf{in}\, e_2, s \,\Longrightarrow, e_2, s[x \mapsto n]</math>
-</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>, 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.
-przypisuj±c zmiennej <math>x</math> warto¶æ <math>n</math>,
+Formalnie
-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>
@@ Linia 342: / Linia 267: @@
 </math>
-W szczególno¶ci,
+W szczególności 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.
-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.
-Natomiast aby obliczyc <math>e_1</math> potrzebujemy regu³y:
+Natomiast aby obliczyc <math>e_1</math>, potrzebujemy reguły:
 <math>
-\frac{e_1, s \,\Longrightarrow\, e'_1, s'}
+\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'}
+{\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>,
+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>.
-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.
+Niestety nie, gdyż nie uwzględniamy ograniczonego zasięgu zmiennej.
-Rzuæmy okiem na przyk³ad:
+Rzućmy okiem na przykład:
 <math>
@@ Linia 366: / Linia 287: @@
 </math>
-Wed³ug naszych intencji to wyra¿enie nie ma warto¶ci, gdy¿ ostatnie
+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
-Natomiast wed³ug powy¿szych regu³ mamy
 <math>
-\mathbf{let}\, x = (\mathbf{let}\, z = 4 \,\mathbf{in}\, z+z+z) \,\mathbf{in}\, z, \emptyset \,\Longrightarrow\,
+\mathbf{let}\, x = (\mathbf{let}\, z = 4 \,\mathbf{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 = 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\,
+\mathbf{let}\, x = 12 \,\mathbf{in}\, z, \emptyset[z \mapsto 4] \,\Longrightarrow,
-, \emptyset[z \mapsto 4] \,\Longrightarrow\,
+, \emptyset[z \mapsto 4] \,\Longrightarrow,
 !
 </math>
-Nasz b³±d polega na tym, ¿e po zakoñczeniu obliczania podwyra¿enia
+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).
-<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.
 <br>
@@ Linia 388: / Linia 305: @@
 <br>
-Wygodne i eleganckie rozwi±zanie tego problemu jest mo¿liwe, je¶li
+Wygodne i eleganckie rozwiązanie tego problemu jest możliwe, jeśli rozszerzymy składnię naszego języka.
-rozszerzymy sk³adniê naszego jêzyka.
+Intuicyjnie, reguła
-Intuicyjnie, regu³a
 <math>
-\mathbf{let}\, x = n \,\mathbf{in}\, e_2, s \,\Longrightarrow\, e_2, s[x \mapsto n].
+\mathbf{let}\, x = n \,\mathbf{in}\, e_2, s \,\Longrightarrow, e_2, s[x \mapsto n]</math>
-</math>
-powinna zostaæ zast±piona przez
+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].
+\mathbf{let}\, x = n \,\mathbf{in}\, e_2, s \,\Longrightarrow\, e_2 \,\mathbf{then}\, \mbox{przywróć wartość zmiennej x}, s[x \mapsto n]</math>
-</math>
-czyli potrzebujemy konstrukcji sk³adniowej, która polega na obliczeniu
+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.
-wyra¿enia
+Rozszerzmy zatem składnię następujaco:
-<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.
+         e \,\mathbf{then}\, x := n</math>
-</math>
-Wyra¿enie <math>e \,\mathbf{then}\, x:= n</math> jest w pewnym sensie dualne
+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 (choć niewątpliwie istotna) różnica między nimi to kolejność obliczenia <math>e</math> i przypisania wartości na zmienną <math>x</math>.
-do <math>\mathbf{let}\, x = n \,\mathbf{in}\, e</math>, gdy¿ jedyna (choc niew±tpliwie istotna) ró¿nica
+Oto nowa reguła
-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
+\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'.
+\mbox{ o ile } s(x) = n'</math>
-</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 powyższa nie obejmuje wogóle takiej sytuacji.
-nieokre¶lone, czyli gdy zmienna <math>x</math> jest niezainicjowana -- regu³a
+Najprostszym sposobem rozwiązania tej trudności jest rozszerzenie konstrukcji <math>e \,\mathbf{then}\, x := n</math>:
-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>
@@ Linia 437: / Linia 341: @@
 </math>
-gdzie symbol <math>\bot</math> oznacza brak warto¶ci.
+gdzie symbol <math>\bot</math> oznacza brak wartości.
-Dodajemy równie¿ regu³ê:
+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
+\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}.
+\mbox{ o ile } s(x) \, \mbox{ jest nieokreślone}</math>
-</math>
-Rozwi±zanie to jest odrobinê nieeleganckie, gdy¿ prawie identyczne regu³y
+Rozwiązanie to jest odrobinę nieeleganckie, gdyż prawie identyczne reguły musimy napisać dwukrotnie.
-musimy napisaæ dwukrotnie.
+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ń:
-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ñ:
 <math>
-\frac{e, s \,\Longrightarrow\, e', s'}
+\frac{e, s \,\Longrightarrow, e', s'}
-{e \,\mathbf{then}\, x := n, s \,\Longrightarrow\, e' \,\mathbf{then}\, x:= n, 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]
+n' \,\mathbf{then}\, x := n, s \,\Longrightarrow, n', s[x \mapsto n]
 </math>
 <math>
-n' \,\mathbf{then}\, x := \bot, s \,\Longrightarrow\, n', s' \quad \mbox{ o ile } s(x)
+n' \,\mathbf{then}\, x := \bot, s \,\Longrightarrow, n', s' \quad \mbox{ o ile } s(x)
-\mbox{ jest okre¶lone i } s' = s \setminus \{ (x, s(x)) \}
+\mbox{ jest określone i } s' = s \setminus \{ (x, s(x)) \}
 </math>
 <br>
@@ Linia 469: / Linia 369: @@
 <br>
-Zanim przejdziemy do kolejnego wariantu, zastanówmy siê czy
+Zanim przejdziemy do kolejnego wariantu, zastanówmy się, czy istnieje inny sposób rozwiązania trudności związanej z <math>n = \bot</math>, który pozwalałby uniknąć wprowadzania dodatkowej konstrukcji
-istnieje inny sposób rozwi±zania trudno¶ci zwi±zanej z <math>n =
-\bot</math>, który pozwala³by unikn±æ wprowadzania dodatkowej konstrukcji
 <math>e \,\mathbf{then}\, x := \bot</math>.
-Pomys³ mo¿e polegaæ na rozszerzeniu
+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 480: / Linia 377: @@
 </math>
-Wtedy nie musimy pisaæ dwóch bardzo podobnych wariantów regu³.
+Wtedy nie musimy pisać dwóch bardzo podobnych wariantów reguł.
-Dodatkowo, w tym rozwi±zaniu warto poczyniæ umowê, ¿e
+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>, przyjmującymi wartość różną od <math>\bot</math> tylko dla skończenie wielu elementów.
-Wtedy stany s± funkcjami ca³kowitymi z <math>\mathbf{Var}</math> w <math>\mathbf{Num}</math>
+Pewnym mankamentem jest to, że teraz <math>n = \bot</math> może pojawiać się w wyrażeniach podobnie jak stałe.
-przyjmuj±cymi warto¶æ ró¿n± od <math>\bot</math> tylko dla skoñczenie
+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 <math>\bot</math> możemy również uważać za roszerzenie składni.
-wielu elementów.
-Pewnym mankamentem jest to, ¿e teraz
-<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
-<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 nieokreśloność:
-elegancko wybrn±æ z sytuacji, rozszerzaj±c operacje arytmetyczne
-na zbiór <math>\mathbf{Num} \cup \{ \bot \}</math> tak, aby zachowywa³y one
-nieokre¶lono¶æ:
 <math>
-n + \bot = \bot + n = \bot
+n + \bot = \bot + n = \bot</math>
-</math>
-Trzeba jednak w takim razie zadbaæ o to, aby wyra¿enie <math>\mathbf{let}\, x = e_1
-\,\mathbf{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>.
+Trzeba jednak w takim razie zadbać o to, aby wyrażenie <math>\mathbf{let}\, x = e_1 \,\mathbf{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>.
+,
 <br>
 '''Wariant 3'''
 <br>
-Zrewidujmy teraz podstawowe za³o¿enia, które dotychczas poczynili¶my.
+Zrewidujmy teraz podstawowe założenia, które dotychczas poczyniliśmy.
-Jednym z nich by³o przyjêcie ogólnej postaci tranzycji:
+Jednym z nich było przyjęcie ogólnej postaci tranzycji:
 <math>
-e, s \,\Longrightarrow\, e', s'
+e, s \,\Longrightarrow, e', s'
 </math>
-pozwalaj±cej na zmianê stanu podczas obliczania wyra¿enia.
+pozwalającej na zmianę stanu podczas obliczania wyrażenia.
-Czy faktycznie by³ to dobry pomys³? Czy mogliby¶my poradziæ sobie
+Czy faktycznie był to dobry pomysł? Czy moglibyśmy poradzić sobie przy pomocy tranzycji postaci
-przy pomocy tranzycji postaci
 <math>
-e, s \,\Longrightarrow\, e', s ?
+e, s \,\Longrightarrow, e', s ?
 </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>
-\frac{e_1, s \,\Longrightarrow\, e'_1, s}
+\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}
+{\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2, s \,\Longrightarrow, \mathbf{let}\, x = e'_1 \,\mathbf{in}\, e_2, s}
 </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:
-Oto mo¿liwa regu³a:
 <math>
-\frac{e, s[x \mapsto n] \,\Longrightarrow\, e', s[x \mapsto n] }
+\frac{e, s[x \mapsto n] \,\Longrightarrow, e', s[x \mapsto n] }
-      {\mathbf{let}\, x = n \,\mathbf{in}\, e, s \,\Longrightarrow\, \mathbf{let}\, x = n \,\mathbf{in}\, e', s}.
+      {\mathbf{let}\, x = n \,\mathbf{in}\, e, s \,\Longrightarrow, \mathbf{let}\, x = n \,\mathbf{in}\, e', s}</math>
-</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> przypisaną zmiennej <math>x</math>.
-obliczamy w prawid³owym stanie, tzn. z warto¶ci± <math>n</math>
+Mały krok w <math>e</math> daje przyczynek do małego kroku w całym wyrażeniu, a przy tym stan pozostaje niezmieniony.
-przypisan± zmiennej <math>x</math>.
+Przy tym wogóle nie potrzebujemy przywracać poprzedniej wartości zmiennej <math>x</math>, ponieważ <math>x</math> zyskuje nową wartość "tylko" na potrzeby obliczania podwyrażenia <math>e</math>!
-Ma³y krok w <math>e</math> daje przyczynek do ma³ego kroku w ca³ym
+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>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>.
-wyra¿eniu, a przy tym stan pozostaje niezmieniony.
+Na końcu musimy oczywiście pozbyć się tej deklaracji za pomocą następującej tranzycji:
-Przy tym wogóle nie potrzebujemy przywracaæ poprzedniej warto¶ci
-zmiennej <math>x</math>, poniewa¿ <math>x</math> zyskuje now± warto¶æ
-''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>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>.
-Na koñcu musimy oczywi¶cie pozbyæ siê tej deklaracji za pomoc±
-nastêpuj±cej tranzycji:
 <math>
-\mathbf{let}\, x = n \,\mathbf{in}\, n', s \,\Longrightarrow\, n', s
+\mathbf{let}\, x = n \,\mathbf{in}\, n', s \,\Longrightarrow, n', s
 </math>
-Podsumujmy. Okazuje siê, ¿e rozwi±zanie nie by³o wcale ³atwe,
+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).
-nawet dla tak pro¶ciutkiego jêzyka. W przysz³o¶ci przekonamy siê,
+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.
-¿e ³atwiej jest poradziæ sobie z zagadnieniem wi±zania identyfikatorów
+Niekiedy jednak rozszerzanie języka będzie zabronione.
-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.
 </div></div>
-}}
 == Zadania domowe ==
@@ Linia 586: / Linia 450: @@
 {{cwiczenie|2|cw2.dom|
-Dotychczas wyst±pienie b³êdu podczas obliczania wyra¿enia,
+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).
-np. odwo³anie do niezainicjowanej zmiennej, powodowa³o, ¿e
+Zmodyfikuj którąś z semantyk z poprzednich zadań tak, aby błąd był komunikowany jako jedna z konfiguracji końcowych.
-wyra¿enie nie posiada³o warto¶ci (nie by³o ci±gu tranzycji
+To znaczy: jeśli obliczenie wyrażenia <math>e</math> w stanie <math>s</math> jest niemożliwe bo wystąpił błąd, to
-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^{*}\, \mathtt{Blad}.
+e, s \,\Longrightarrow^{*}\, \mathtt{Blad}</math>
-</math>
 }}
@@ Linia 603: / Linia 461: @@
 {{cwiczenie|3|cw3.dom|
-Rozwa¿ rozszerzenie jêzyka wyra¿eñ o wyra¿enia boolowskie:
+Rozważ rozszerzenie języka wyrażeń o wyrażenia boolowskie:
 <math>
@@ Linia 632: / Linia 490: @@
 </math>
-Zaproponuj semantykê ma³ych kroków dla tego jêzyka.
+Zaproponuj semantykę małych kroków dla tego języka.
-Rozwa¿ ró¿ne strategie obliczania wyra¿eñ boolowskich, oraz podej¶cie leniwe.
+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{false}</math>, w podejściu leniwym nie ma wogóle potrzeby obliczania <math>b_2</math>.
-gdy <math>b_1</math> zosta³o obliczone do <math>\mathbf{false}</math>, w podej¶ciu leniwym nie ma wogóle potrzeby
-obliczania <math>b_2</math>.
 }}