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

← poprzednia edycja następna edycja →

WizualnieWikikod

Wersja z 08:04, 10 sie 2006

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

{{{3}}}

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

Przykład

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

{{{3}}}

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

Wersja z 08:04, 10 sie 2006

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¶æ ==
+== Zawartość ==
-Tematem tych zajêæ jest semantyka operacyjna wyra¿eñ (ma³e kroki).
+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 30: @@
 </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.
+Zaproponuj semantykę operacyjną (małe kroki) dla tego języka.
 }}
@@ Linia 44: / Linia 44: @@
 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>.
 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>.
-Dla u³atwienia zapisywania regu³ zak³adamy, ze sta³e
+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
+Będziemy potrzebować zbioru ''stanów'', opisujących wartości
 przypisane zmiennym.
-Najprostszym rozwi±zaniem jest przyj±c, ¿e stan to funkcja
+Najprostszym rozwiązaniem jest przyjąc, że stan to funkcja
 z <math>\mathbf{Var}</math> do <math>\mathbf{Num}</math>.
 Oznaczmy przez <math>\mathbf{State}</math> zbiór wszystkich takich funkcji;
-stany oznaczac bêdziemy przez <math>s, s_1, s', \ldots \in \mathbf{State}</math>.
+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
@@ Linia 67: / 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 78: / 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
+Zatem przyjmijmy, że zbiór konfiguracji to
 <math>
@@ Linia 87: / Linia 87: @@
 </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ę to druga postać tranzycji nie jest
-niezbêdna, gdy¿ mogliby¶my umówiæ siê, ¿e konfiguracje koñcowe
+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>
@@ Linia 102: / Linia 102: @@
 </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ê
+ze stałej liczbowej, podczas gdy <math>n</math> po prawej stronie reprezentuje liczbę
-bêd±c± warto¶ci± wyra¿enia.
+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>
@@ Linia 112: / Linia 112: @@
 </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
+kroków, musimy zdecydować się czy najpierw obliczyć pierwszy (lewy) składnik
 <math>e_1</math> czy drugi?
-Je¶li wybierzemy lewy (strategia ''lewostronna''), otrzymamy regu³ê:
+Jeśli wybierzemy lewy (strategia ''lewostronna''), otrzymamy regułę:
 <math>
@@ Linia 123: / Linia 123: @@
 </math>
-Regu³y tej postaci bêdziemy zapisywaæ tak:
+Reguły tej postaci będziemy zapisywać tak:
 <math>
@@ Linia 130: / Linia 130: @@
 </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 138: / Linia 138: @@
 </math>
-A na koñcu dodajemy:
+A na końcu dodajemy:
 <math>
@@ Linia 144: / Linia 144: @@
 </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
+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>.
+języka, a drugie oznacza operację dodawania w zbiorze <math>\mathbf{Num}</math>.
-Pozwalamy sobie na tak± kolizjê oznaczeñ, gdy¿ nie powinna ona
+Pozwalamy sobie na taką kolizję oznaczeń, gdyż nie powinna ona
-prowadziæ do niejednoznaczno¶ci. Pamiêtajmy, ¿e sk³adnia jêzyka jest
+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
+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
+dobrze pisać np. <math>{\mathrm{add}}(e_1, e_2)</math> a wtedy reguła
-wygl±da³aby tak:
+wyglądałaby tak:
 <math>
@@ Linia 157: / Linia 157: @@
 </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
+''prawostronna'', którą otrzymujemy zastępując pierwsze dwie z trzech
-powy¿szych regu³ przez:
+powyższych reguł przez:
 <math>
@@ Linia 169: / Linia 169: @@
 </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>:
@@ Linia 184: / Linia 184: @@
 </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
+Ta dowolność prowadzi do ''niedeterminizmu'', czyli do sytuacji, gdy
-kolejna (nastêpna) konfiguracja nie jest wyznaczona jednoznacznie.
+kolejna (następna) konfiguracja nie jest wyznaczona jednoznacznie.
-Jest tak, gdy¿ mo¿emy mieæ do wyboru dwie ró¿ne tranzycje
+Jest tak, gdyż możemy mieć do wyboru dwie różne tranzycje
 <math>
@@ Linia 196: / Linia 196: @@
 </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¶æ
+<math>e_1</math> i <math>e_2</math> nie wpływa w tym przypadku na końcową wartość
-ca³ego wyra¿enia.
+całego wyrażenia.
-Na koniec regu³y dla wyra¿enia warunkowego.
+Na koniec reguły dla wyrażenia warunkowego.
 <math>
@@ Linia 221: / Linia 221: @@
 {{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 229: @@
 </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.
+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¶æ.
+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''
+Ogólniej, odwołania do zmiennej w wyrażeniu odnoszą się do ''najbliższej''
-(najbardziej zagnie¿dzonej) deklaracji tej zmiennej.
+(najbardziej zagnieżdzonej) deklaracji tej zmiennej.
-Taki mechanizm wi±zania identyfikatorów nazywamy ''wi±zaniem
+Taki mechanizm wiązania identyfikatorów nazywamy ''wiązaniem
 statycznym''.
-Przyjmujemy zwyk³e (statyczne) regu³y przes³aniania zmiennych, np.
+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
+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>
+deklaracja <math>x = e</math> ''przesłania'' deklarację <math>x = e_1</math>
-w wyra¿eniu <math>e'</math>.
+w wyrażeniu <math>e'</math>.
-Zak³adamy, ¿e na pocz±tku warto¶ci wszystkich zmiennych s±
+Zakładamy, że na początku wartości wszystkich zmiennych są
-''nieokre¶lone'', czyli zmienne s± niezainicjowane, a odwo³anie do
+''nieokreślone'', czyli zmienne są niezainicjowane, a odwołanie do
-niezainicjowanej zmiennej jest uwa¿ane za niepoprawne.
+niezainicjowanej zmiennej jest uważane za niepoprawne.
 }}
@@ Linia 268: / Linia 268: @@
 <math>
 \mathbf{let}\, z = 5 \,\mathbf{in}\, x+z
-\quad \quad \mapsto \quad \quad \mbox{brak wyniku; odwo³anie do niezainicjowanej
+\quad \quad \mapsto \quad \quad \mbox{brak wyniku; odwołanie do niezainicjowanej
 zmiennej}\, x
 </math>
@@ Linia 284: / Linia 284: @@
 Podobnie jak poprzednio,
-stan powinien opisywaæ warto¶ci przypisane zmiennym.
+stan powinien opisywać wartości przypisane zmiennym.
 Tym razem jednak
-uwzglêdnimy niezainicjowane zmienne, czyli zmienne bez ¿adnej warto¶ci.
+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:
 <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>
+Wartość wyrażenia <math>e</math> w stanie początkowym wynosi <math>n</math>
 o ile zachodzi:
@@ Linia 301: / Linia 301: @@
 </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 trochê ogólniejsza:
+ale pierwsza postać będzie trochę ogólniejsza:
 <math>
@@ Linia 308: / Linia 308: @@
 </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>.
-Stan mo¿e siê teraz zmieniæ na skutek deklaracji zmiennych.
+Stan może się teraz zmienić na skutek deklaracji zmiennych.
-Spróbujmy rozszerzyc semantykê z poprzedniego zadania.
+Spróbujmy rozszerzyc 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>.
-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 329: @@
 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.
+i pozostawiając niezmienione wartości dla pozostałych zmiennych.
 Formanie
@@ Linia 342: / Linia 342: @@
 </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
+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 353: / Linia 353: @@
 </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>.
 '''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 366: @@
 </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>
@@ Linia 378: / Linia 378: @@
 </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>
+<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).
+poprzednią wartość (a właściwie brak wartości w przykładzie powyżej).
 Przedyskutujmy kilka wariantów.
@@ Linia 388: / Linia 388: @@
 <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>
@@ Linia 396: / Linia 396: @@
 </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>
-czyli potrzebujemy konstrukcji sk³adniowej, która polega na obliczeniu
+czyli potrzebujemy konstrukcji składniowej, która polega na obliczeniu
-wyra¿enia
+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:
+Rozszerzmy zatem składnię następujaco:
 <math>
@@ Linia 413: / Linia 413: @@
 </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 (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
+Oto nowa reguła
 <math>
@@ Linia 424: / Linia 424: @@
 </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.
+powyższa nie obejmuje wogóle takiej sytuacji.
-Najprostszym sposobem rozwi±zania tej trudno¶ci jest rozszerzenie
+Najprostszym sposobem rozwiązania tej trudności jest rozszerzenie
 konstrukcji <math>e \,\mathbf{then}\, x := n</math>:
@@ Linia 437: / Linia 437: @@
 </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
-\mbox{ o ile } s(x) \, \mbox{ jest nieokre¶lone}.
+\mbox{ o ile } s(x) \, \mbox{ jest nieokreślone}.
 </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>
+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ñ:
+z semantyką pozostałych wyrażeń:
 <math>
@@ Linia 461: / Linia 461: @@
 <math>
 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>
@@ Linia 469: / Linia 469: @@
 <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 =
+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>.
-Pomys³ mo¿e polegaæ na rozszerzeniu
+Pomysł może polegać na rozszerzeniu
 zbioru <math>\mathbf{Num}</math> o dodatkowy element <math>\bot</math>:
@@ Linia 480: / Linia 480: @@
 </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>
+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
+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
+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
+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¶æ:
+nieokreśloność:
 <math>
@@ Linia 501: / Linia 501: @@
 </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
-\,\mathbf{in}\, e_2</math> oblicza³o siê normalnie tylko wtedy, gdy warto¶æ
+\,\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>.
+wyrażenia <math>e_1</math> jest różna od <math>\bot</math>.
@@ Linia 510: / Linia 510: @@
 <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>
@@ Linia 517: / Linia 517: @@
 </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
@@ Linia 525: / Linia 525: @@
 </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 533: / Linia 533: @@
 </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>
@@ Linia 543: / Linia 543: @@
 </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.
+wyrażeniu, a przy tym stan pozostaje niezmieniony.
-Przy tym wogóle nie potrzebujemy przywracaæ poprzedniej warto¶ci
+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
+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>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±
+Na końcu musimy oczywiście pozbyć się tej deklaracji za pomocą
-nastêpuj±cej tranzycji:
+następującej tranzycji:
 <math>
@@ Linia 562: / Linia 562: @@
 </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ê,
+nawet dla tak prościutkiego języka. W przyszłości przekonamy się,
-¿e ³atwiej jest poradziæ sobie z zagadnieniem wi±zania identyfikatorów
+że łatwiej jest poradzić sobie z zagadnieniem wiązania identyfikatorów
-w semantyce naturalnej (du¿e kroki).
+w semantyce naturalnej (duże kroki).
-W wariancie 1 i 2 wprowadzili¶my do jêzyka dodatkowe elementy, tak,
+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æ
+by łatwiej było pisać reguły. W przyszłości będziemy czasem stosować
-takie podej¶cie.
+takie podejście.
-Niekiedy jednak rozszerzanie jêzyka bêdzie zabronione.
+Niekiedy jednak rozszerzanie języka będzie zabronione.
 </div></div>
@@ Linia 586: / Linia 586: @@
 {{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
+np. odwołanie do niezainicjowanej zmiennej, powodowało, że
-wyra¿enie nie posiada³o warto¶ci (nie by³o ci±gu tranzycji
+wyrażenie nie posiadało wartości (nie było ciągu tranzycji
-prowadz±cych do konfiguracji koñcowej). Zmodyfikuj któr±¶ z semantyk
+prowadzących do konfiguracji końcowej). Zmodyfikuj którąś z semantyk
-z poprzednich zadañ tak, aby b³±d by³ komunikowany
+z poprzednich zadań tak, aby błąd był komunikowany
-jako jedna z konfiguracji koñcowych. To znaczy: je¶li obliczenie
+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
+błąd, to
 <math>
@@ Linia 603: / Linia 603: @@
 {{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 632: @@
 </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
+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>.
 }}