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

← poprzednia edycja następna edycja →

WizualnieWikikod

Wersja z 08:22, 11 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:22, 11 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 11: / Linia 11: @@
 {{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 29: @@
 </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.
@@ Linia 44: / Linia 40: @@
 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, ze 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ąc, ż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 oznaczac 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.
@@ Linia 67: / Linia 56: @@
 </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 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.
-<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
 </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 91: / Linia 77: @@
 {{
 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 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>.
 }}
@@ Linia 102: / Linia 86: @@
 </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:
@@ Linia 112: / Linia 94: @@
 </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
-<math>e_1</math> czy drugi?
 Jeśli wybierzemy lewy (strategia ''lewostronna''), otrzymamy regułę:
@@ Linia 144: / Linia 124: @@
 </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>
@@ Linia 157: / Linia 131: @@
 </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>
@@ Linia 169: / Linia 141: @@
 </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>
@@ Linia 184: / Linia 153: @@
 </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
-kolejna (następna) konfiguracja nie jest wyznaczona jednoznacznie.
 Jest tak, gdyż możemy mieć do wyboru dwie różne tranzycje
@@ Linia 196: / Linia 163: @@
 </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.
@@ Linia 229: / Linia 194: @@
 </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ą na zmienna <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>;
-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ą
+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.
-''nieokreślone'', czyli zmienne są niezainicjowane, a odwołanie do
-niezainicjowanej zmiennej jest uważane za niepoprawne.
 }}
@@ Linia 283: / Linia 236: @@
 <div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
-Podobnie jak poprzednio,
+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.
-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:
@@ Linia 292: / Linia 243: @@
 \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>
@@ Linia 301: / Linia 250: @@
 </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>
@@ Linia 308: / Linia 256: @@
 </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
-<math>e'</math> a nowym stanem jest <math>s'</math>.
 Stan może się teraz zmienić na skutek deklaracji zmiennych.
 Spróbujmy rozszerzyc semantykę z poprzedniego zadania.
 Ponieważ stan jest funkcją częściową, musimy zmienić niektóre reguły, np.
@@ Linia 320: / Linia 266: @@
 </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>
@@ Linia 328: / Linia 273: @@
 </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 284: @@
 </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:
@@ Linia 353: / Linia 293: @@
 </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?
@@ Linia 366: / Linia 304: @@
 </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
@@ Linia 378: / Linia 315: @@
 </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 322: @@
 <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
@@ Linia 402: / Linia 335: @@
 </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
-<math>e_2</math> a następnie na przypisaniu zmiennej <math>x</math> danej wartości.
 Rozszerzmy zatem składnię następujaco:
@@ Linia 413: / Linia 344: @@
 </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 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
-między nimi to kolejność obliczenia <math>e</math> i przypisania wartości
-na zmienną <math>x</math>.
 Oto nowa reguła
@@ Linia 424: / Linia 352: @@
 </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 445: / Linia 370: @@
 </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>
@@ Linia 463: / Linia 386: @@
 \mbox{ jest określone i } s' = s \setminus \{ (x, s(x)) \}
 </math>
 <br>
@@ Linia 469: / Linia 391: @@
 <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 481: / Linia 400: @@
 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ć sie 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>
-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ść wyrażenia <math>e_1</math> jest różna od <math>\bot</math>.
-\,\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'''
@@ Linia 518: / Linia 425: @@
 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>
@@ Linia 525: / Linia 431: @@
 </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 438: @@
 </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>.
 Oto możliwa reguła:
@@ Linia 543: / Linia 447: @@
 </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>
@@ Linia 562: / Linia 457: @@
 </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
-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.
@@ Linia 586: / Linia 476: @@
 {{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>
@@ Linia 634: / Linia 519: @@
 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{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>.
 }}