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

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

Zawartość

Napiszemy semantykę naturalną języka wyrażeń, rozważymy strategię gorliwą (jak na wcześniejszych zajęciach, w semantyce małych kroków) i leniwą. Rozważymy i statyczne i dynamiczne wiązanie identyfikatorów. Następnie rozszerzymy ten język o lambda-abstrakcję i aplikację, otrzymując prosty język funkcyjny.

Różne semantyki naturalne wyrażeń

Ćwiczenie 1 (semantyka gorliwa)

Napisz semantykę dużych kroków dla języka wyrażeń, którego semantykę małokrokową napisaliśmy na jednych z poprzednich ćwiczeń:

$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} | 𝐥 𝐞 𝐭 x = e_{1} 𝐢 𝐧 e_{2}$

Rozwiązanie

Przypomnijmy, że zbiór stanów to $𝐒 𝐭 𝐚 𝐭 𝐞 = 𝐕 𝐚 𝐫 \to_{f i n} 𝐍 𝐮 𝐦$

Nasze tranzycje będą postaci $e, s ⟶ n$ , gdzie $e \in 𝐄 𝐱 𝐩, s \in 𝐒 𝐭 𝐚 𝐭 𝐞, n \in 𝐍 𝐮 𝐦$ . Oto reguły semantyki naturalnej.

$n, s ⟶ n$

$x, s ⟶ n o ile s (x) = n$

$\frac{e_{1}, s ⟶ n_{1} e_{2}, s ⟶ n_{2}}{e_{1} + e_{2}, s ⟶ n} o ile n = n_{1} + n_{2}$

$\frac{e_{1}, s ⟶ n_{1} e_{2}, s [x \mapsto n_{1}] ⟶ n_{2}}{𝐥 𝐞 𝐭 x = e_{1} 𝐢 𝐧 e_{2}, s ⟶ n_{2}}$

$\frac{e_{1}, s ⟶ n_{1} n_{1} \neq 0 e_{2}, s ⟶ n_{2}}{𝐢 𝐟 e_{1} 𝐭 𝐡 𝐞 𝐧 e_{2} 𝐞 𝐥 𝐬 𝐞 e_{3}, s ⟶ n_{2}}$

$\frac{e_{1}, s ⟶ n_{1} n_{1} = 0 e_{3}, s ⟶ n_{3}}{𝐢 𝐟 e_{1} 𝐭 𝐡 𝐞 𝐧 e_{2} 𝐞 𝐥 𝐬 𝐞 e_{3}, s ⟶ n_{3}}$

Zwróćmy uwagę na fakt, że prawidłowe odwzorowanie zasięgu deklaracji $x = e_{1}$ nie predstawia w semantyce naturalnej żadnych trudności, w przeciwieństwie do semantyki małych kroków.

Ćwiczenie 2 (semantyka leniwa)

Zmodyfikuj semantykę z poprzedniego zadania, aby uzyskać leniwą ewaluację wyrażeń, zgodnie z dyrektywą: nie obliczaj wyrażenia, o ile jego wynik nie jest potrzebny (albo: obliczaj wartość wyrażenia dopiero wtedy, gdy jego wynik jest naprawdę potrzebny). Spójrzmy na przykład:

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

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

Rozwiązanie

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

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

Np. odpowiednia reguła dla wyrażenia $𝐥 𝐞 𝐭$ , w semantyce małych kroków mogłaby wyglądać następująco:

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

Czyli stan zawiera, dla każdej zmiennej, parę (wyrażenie definiujące, stan w momencie deklaracji).

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

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

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

i przyjmijmy, że

$𝐒 𝐭 𝐚 𝐭 𝐞 = ⋃_{n \in n a t} {𝐒 𝐭 𝐚 𝐭 𝐞}_{n}$

Tranzycje będą znów postaci: $e, s ⟶ n$ Podamy tylko reguły dla wystąpienia zmiennej i dla wyrażenia $𝐥 𝐞 𝐭$ ,. Reguły dla pozostałych konstrukcji języka pozostają praktycznie bez zmian.

$\frac{e, s^{'} ⟶ n}{x, s ⟶ n} o ile s (x) = (e, s^{'})$

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

Ćwiczenie 3 (semantyka dynamiczna)

Rozważmy teraz zupełnie inny mechanizm wiązania identyfikatorów zwany wiązaniem dynamicznym. Dla odróżnienia, dotychczasowy sposób wiązania (widoczności) identyfikatorów będziemy nazywać wiązaniem statycznym. Oto przykładowe wyrażenie:

$𝐥 𝐞 𝐭 y = x + 1 𝐢 𝐧 𝐥 𝐞 𝐭 x = 10 𝐢 𝐧 y$

które nie ma wartości w pustym stanie początkowym, według semantyk z poprzednich zadań, ponieważ odwołanie do zmiennej $x$ w deklaracji $y = x + 1$ jest niepoprawne. Tak samo jest nawet w semantyce leniwej, gdyż wartość zmiennej $y$ będzie w końcu policzona i będzie wymagała odwołania do $x$ w stanie pustym.

Natomiast wyobrażmy sobie, że zmieniamy semantykę leniwą następująco: odwołanie do zmiennej $x$ podczas obliczania wartości $y$ będzie odnosiło się nie do stanu w momencie deklaracji $y$ , ale do stanu w momencie odwołania do $y$ . Jest to dość rewolucyjna zmiana, zapewne sprzeczna z intuicjami programisty (statyczne reguły widoczności zamieniamy na dynamiczne). W szczególności powyższe wyrażenie policzy się w semantyce dynamicznej do wartości 11, ponieważ stan w momencie odwołania do zmiennej $y$ przypisuje zmiennej $x$ wartość 10 !

Napisz semantykę naturalną dla wiązania dynamicznego.

Rozwiązanie

Teraz w stanie wystarczy przechowywać "wyrażenie" definiujące wartość danej zmiennej:

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

Nie potrzebujemy zapamiętywać stanu, w którym byliśmy w momencie deklaracji. Do obliczenia zapamiętanego wyrażenia użyjemy stanu, w którym będziemy w momencie odwołania do danej zmiennej. Znów podajemy tylko reguły dla wystąpienia zmiennej i dla wyrażenia $𝐥 𝐞 𝐭$ ,, gdyż pozostałe reguły pozostają bez zmian

$\frac{e, s ⟶ n}{x, s ⟶ n} o ile s (x) = e$

$\frac{e_{2}, s [x \mapsto e_{1}] ⟶ n}{𝐥 𝐞 𝐭 x = e_{1} 𝐢 𝐧 e_{2}, s ⟶ n}$

Pytanie: czy $𝐥 𝐞 𝐭 x = x + 1 𝐢 𝐧 x$ oblicza się do jakiejś wartości w stanie $\emptyset$ ?

Prosty język funkcyjny

Ćwiczenie 4 (przekazywanie parametru przez wartość)

Rozważmy prosty język funkcyjny $F$ rozszerzający język wyrażeń z poprzednich zadań następująco:

$e : : = \dots | λ x . e | e_{1} (e_{2})$

Lambda-abstrakcja $λ x . e$ reprezentuje anonimową (nienazwaną) funkcję jednoargumentową, natomiast wyrażenie $e_{1} (e_{2})$ to aplikacja $e_{1}$ do $e_{2}$ (wyrażenie $e_{1}$ powinno zatem obliczać się do funkcji). Np.

$(λ x . x + 3) (2) ⟶ 5$

Przyjmijmy statyczną widoczność identyfikatorów. Możliwe są różne mechanizmy przekazywania parametrów. Na razie wybierzmy mechanizm przekazywania przez wartość, zapewne doskonale znany Czytelnikowi: wyrażenie będące parametrem aktualnym jest obliczane przed wywołaniem funkcji, czyli w stanie, w którym jesteśmy z momencie wywołania funkcji.

Zaproponuj semantykę naturalną dla tego języka dla obydwu mechanizmów przekazywania parametrów.

Rozwiązanie

Zauważmy, że oprócz deklaracji zmiennych, również machanizm przekazywania parametru do funkcji wymaga zmiany stanu.

Tranzycje będą postaci

$e, s ⟶ v$

gdzie $v$ reprezentuje wartość, do której oblicza się program $e$ . Z tym, że wartościami będą nie tylko wartości liczbowe. Na przykład $λ x . x$ oblicza się również do pewnej wartość, która w tym przypadku powinna reprezentować jakoś funkcję identycznościową. Wystarczającą reprezentacją funkcji będzie trójka: $⟨ x, e, s ⟩$ , gdzie $x$ jest nazwą parametru formalnego, $e$ jest ciałem funkcji, a $s$ jest stanem, w którym należy obliczać wartość funkcji po zaaplikowaniu do jakiegoś parametru aktualnego. Oto prosty przykład pokazujący, dlaczego powinniśmy pamiętać stan:

$𝐥 𝐞 𝐭 x = 7 𝐢 𝐧 𝐥 𝐞 𝐭 f = λ z . x + z 𝐢 𝐧 𝐥 𝐞 𝐭 x = f (1) 𝐢 𝐧 f (10)$

Funkcja $f$ zwiększa parametr aktualny o $x$ . Program oblicza się do wartości $17$ , gdyż wystąpienie zmiennej $x$ w ciele funkcji $f$ wiąże statycznie, a zatem odnosi się zawsze do deklaracji $x = 7$ , mimo tego, że w momencie wywołania tej funkcji wartość zmiennej $x$ wynosi $8$ .

Oto jedyna reguła, jakiej będziemy potrzebować dla lambda-abstrakcji:

$λ x . e, s ⟶ ⟨ x, e, s ⟩$

Nie potrafimy zrobić z funkcją $λ x . e$ nic innego jak zapamiętać informację niezbędną do obliczania jej wartości w przyszłości. Zatem zbiór wartości będzie następujący:

$v \in 𝐕 𝐚 𝐥 𝐮 𝐞 𝐬 = 𝐍 𝐮 𝐦 \cup (𝐕 𝐚 𝐫 \times 𝐄 𝐱 𝐩 \times 𝐒 𝐭 𝐚 𝐭 𝐞)$

a zbiór stanów $𝐒 𝐭 𝐚 𝐭 𝐞$ określony jest następującym równaniem:

$𝐒 𝐭 𝐚 𝐭 𝐞 = 𝐕 𝐚 𝐫 \to_{f i n} 𝐕 𝐚 𝐥 𝐮 𝐞 𝐬$

Zacznijmy od stałych, zmiennych i lambda-abstrakcji:

$n, s ⟶ n x, s ⟶ v o ile s (x) = v λ x . e, s ⟶ ⟨ x, e, s ⟩$

W regule dla zmiennej, $v$ oznacza albo wartość liczbową albo funkcyjną. Pomijamy regułę dla dodawania, bo jest ona identyczna jak dla gorliwej semantyki wyrażeń. Reguła dla $𝐥 𝐞 𝐭 x = e_{1} 𝐢 𝐧 e_{2}$ będzie prawie taka sama jak dla wyrażeń, z tą różnicą, że wyrażenie $e_{1}$ definiujące wartość zmiennej $x$ może się teraz obliczać do wartości funkcyjnej, np. $𝐥 𝐞 𝐭 x = (λ y . y + y) 𝐢 𝐧 x (0)$ .

$\frac{e_{1}, s ⟶ v_{1} e_{2}, s [x \mapsto v_{1}] ⟶ v_{2}}{𝐥 𝐞 𝐭 x = e_{1} 𝐢 𝐧 e_{2}, s ⟶ v_{2}}$

Pozostała nam już tylko reguła dla aplikacji: najpierw oblicz funkcję; następnie oblicz wartość parametru aktualnego; wreszcie przekaż ją do ciała funkcji (czyli oblicz ciało funkcji w zmodyfikowanym stanie):

$\frac{e_{1}, s ⟶ ⟨ x, e, s^{'} ⟩ e_{2}, s ⟶ v^{'} e, s^{'} [x \mapsto v^{'}] ⟶ v}{e_{1} (e_{2}), s ⟶ v}$

Zwróćmy uwagę na wymóg, że $e_{1}$ oblicza się do wartości funkcyjnej $⟨ x, e, s^{'} ⟩$ . W szczególności np. wyrażenie $7 (3 + 4)$ jest niepoprawne. Natomiast parametr aktualny nie musi być liczbą, może być funkcją, np. w programie:

$𝐥 𝐞 𝐭 g = λ f . λ x . f (x) 𝐢 𝐧 g (λ x . x + 1) (7)$

który oblicza się do wartości $8$ .

Ćwiczenie 5 (przekazywanie parametru przez nazwę)

Zaproponuj leniwą semantykę języka $F$ z mechnizmem przekazywanie parametru "przez nazwę". Mechanizm ten stanowi leniwy odpowiednik przekazywania przez wartość: nie obliczamy wyrażenia będącego parametrem aktualnym, a zamiast jego wartości przekazujemy do funkcji to wyrażenie wraz ze stanem z miejsca wywołania funkcji. To ten stan bedzie brany pod uwagę, gdy obliczana będzie wartość parametru, tzn. przy odwołaniu w ciele funkcji do parametru formalnego. Oto przykład programu:

$𝐥 𝐞 𝐭 f = λ x . 7 𝐢 𝐧 f (y)$

który w stanie pustym (wszystkie zmienne nieokreślone) nie ma wartości przy przekazywaniu parametru przez wartość (bo odwołanie do zmiennej $y$ jest niepoprawne), a oblicza się do wartości $7$ jeśli wybierzemy mechanizm przekazywania przez nazwę.

Rozwiązanie

Zbiór wartości $𝐕 𝐚 𝐥 𝐮 𝐞 𝐬$ stojących po prawej stronie symbolu $⟶$ , będzie taki sam jak w poprzednim zadaniu. Natomiast zbiór stanów taki sam jak w semantyce leniwej wyrażeń:

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

Podamy tylko trzy reguły: dla wystąpienie zmiennej, deklaracji $𝐥 𝐞 𝐭$ , i aplikacji -- wszystkie pozostałe reguły pozostają takie same jak w poprzednim zadaniu.

$\frac{e, s^{'} ⟶ v}{x, s ⟶ v} o ile s (x) = (e, s^{'})$

$\frac{e_{2}, s [x \mapsto (e, s)] ⟶ v}{𝐥 𝐞 𝐭 x = e_{1} 𝐢 𝐧 e_{2}, s ⟶ v}$

$\frac{e_{1}, s ⟶ ⟨ x, e, s^{'} ⟩ e, s^{'} [x \mapsto (e_{2}, s)] ⟶ v}{e_{1} (e_{2}), s ⟶ v}$

Podstawowa różnica w ostatnej regule w porównaniu do poprzedniego zadania to brak ewaluacji parametru aktualnego $e_{2}$ . Zwróćmy też uwagę na wyrażenie $s^{'} [x \mapsto (e_{2}, s)]$ , w którym $s \neq s^{'}$ . Stany, których potrzebowaliśmy dotychczas podczas poprzednich zajęć, miały zawsze postać $s [x \mapsto (e, s)]$ .

Zadania domowe

Ćwiczenie 1

Podaj przykład wyrażenia takiego, które:

ma wartość w semantyce statycznej i dynamicznej, ale w każdej inną
ma wartość w semantyce leniwej, a nie ma w dynamicznej
ma wartość w semantyce dynamicznej, a nie ma w leniwej.

Ćwiczenie 2

W semantyce leniwej wyrażeń, jeśli jest wiele odwołań do jakiejś zmiennej, to obliczenie wartości tej zmiennej nastąpi za każdym razem od nowa. Zmodyfikuj tę semantykę tak, aby wartość ta była obliczana co najwyżej raz. Zatem po pierwszym odwołaniu do zmiennej, jej obliczona wartość powinna zostać umieszczona w stanie, zastępując parę (wyrażenie, stan).

Ćwiczenie 3

Zaproponuj dynamiczne odpowiedniki obydwu statycznych semantyk dla języka funkcyjnego $F$ . Czyli zakładamy, że widoczność identyfikatorów, m.in. w ciele funkcji, jest dynamiczna. Oto przykład programu, który w semantyce statycznej oblicza się do wartości $12$ , a w dynamicznej do wartości $5$ (parametr przekazywany przez wartość):

$𝐥 𝐞 𝐭 x = 7 𝐢 𝐧 𝐥 𝐞 𝐭 f = λ z . z + x 𝐢 𝐧 𝐥 𝐞 𝐭 x = 0 𝐢 𝐧 f (5)$

Rozważ dwa mechanizmy przekazywania parametrów:

przez wartość
przez nazwę

Ten drugi mechanizm rozumiemy teraz następująco: parametr aktualny nie jest obliczany w momencie zaaplikowania do niego funkcji, a do ciała funkcji przekazuje się wyrażenie będące parametrem aktualnym. W momencie odwołania do parametru formalnego w ciele funkcji, wyrażenie będące parametrem aktualnym jest obliczane w bieżącym stanie (a nie w stanie z miejsca wywołania funkcji). Jako przykład rozważmy program:

$(λ z . 𝐥 𝐞 𝐭 x = 10 𝐢 𝐧 z + z) (x) + 1$

Przy przekazywaniu przez wartość w stanie pustym program się nie obliczy, ponieważ nie da się obliczyć parametru aktualnego $x$ . Natomiast przy przekazywaniu przez nazwę, parametr aktualny będzie obliczany dopiero w momencie odwołania do parametru formalnego $z$ , czyli w momencie obliczania wartości wyrażenia $z + z$ . W stanie tym zmienna $x$ ma już wartość, a zatem wartością całego programu będzie 21.

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

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

Spis treści

Zawartość

Różne semantyki naturalne wyrażeń

Prosty język funkcyjny

Zadania domowe

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia

@@ Linia 1: / Linia 1: @@
+== Zawartość ==
-== Zawarto¶æ ==
+Napiszemy semantykę naturalną języka wyrażeń, rozważymy strategię gorliwą (jak na wcześniejszych zajęciach, w semantyce małych kroków) i leniwą.
+Rozważymy i statyczne i dynamiczne wiązanie identyfikatorów.
+Następnie rozszerzymy ten język o lambda-abstrakcję i aplikację, otrzymując prosty język funkcyjny.
-Napiszemy semantykê naturaln± jêzyka wyra¿eñ,
-rozwa¿ymy strategiê gorliw± (jak na wcze¶niejszych zajêciach,
-w semantyce ma³ych kroków) i leniw±.
-Rozwa¿ymy i statyczne i dynamiczne wi±zanie identyfikatorów.
-Nastêpnie rozszerzymy ten jêzyk o lambda-abstrakcjê i aplikacjê,
-otrzymuj±c prosty jêzyk funkcyjny.
+== Różne semantyki naturalne wyrażeń ==
-== Ró¿ne semantyki naturalne wyra¿eñ ==
@@ Linia 17: / Linia 13: @@
-Napisz semantykê du¿ych kroków
+Napisz semantykę dużych kroków dla języka wyrażeń, którego semantykę małokrokową napisaliśmy na jednych z poprzednich ćwiczeń:
-dla jêzyka wyra¿eñ, którego semantykê ma³o-krokow±
-napisali¶my na jednych z poprzednich æwiczeñ:
 <math>
@@ Linia 40: / Linia 34: @@
-{{rozwiazanie||roz1|
-<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
+<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">
-Przypomnijmy, ¿e zbiór stanów to
+Przypomnijmy, że zbiór stanów to
 <math>
 \mathbf{State} \, = \, \mathbf{Var} \to_{\mathrm{fin}} \mathbf{Num}
 </math>
-Nasze tranzycje bêd± postaci <math>e, s \,\longrightarrow\, n</math>, gdzie
+Nasze tranzycje będą postaci <math>e, s \,\longrightarrow\, n</math>, gdzie <math>e \in \mathbf{Exp}, s \in \mathbf{State}, n \in \mathbf{Num}</math>.
-<math>e \in \mathbf{Exp}, s \in \mathbf{State}, n \in \mathbf{Num}</math>.
+Oto reguły semantyki naturalnej.
-Oto regu³y semantyki naturalnej.
 <math>
@@ Linia 81: / Linia 75: @@
 </math>
-Zwróæmy uwagê na fakt, ¿e prawid³owe odwzorowanie zasiêgu deklaracji <math>x = e_1</math> nie predstawia
+Zwróćmy uwagę na fakt, że prawidłowe odwzorowanie zasięgu deklaracji <math>x = e_1</math> nie predstawia w semantyce naturalnej żadnych trudności, w przeciwieństwie do semantyki małych kroków.
-w semantyce naturalnej ¿adnych trudno¶ci, w przeciwieñstwie do
-semantyki ma³ych kroków.
 </div></div>
-}}
@@ Linia 92: / Linia 84: @@
-Zmodyfikuj semantykê z poprzedniego zadania, aby uzyskaæ
+Zmodyfikuj semantykę z poprzedniego zadania, aby uzyskać ''leniwą'' ewaluację wyrażeń, zgodnie z dyrektywą: nie obliczaj wyrażenia, o ile jego wynik nie jest potrzebny (albo: obliczaj wartość wyrażenia dopiero wtedy, gdy jego wynik jest naprawdę potrzebny).
-''leniw±'' ewaluacjê wyra¿eñ, zgodnie z dyrektyw±: nie obliczaj
+Spójrzmy na przykład:
-wyra¿enia o ile jego wynik nie jest potrzebny
-(albo: obliczaj warto¶æ wyra¿enia dopiero wtedy, gdy jego wynik jest
-naprawdê potrzebny). Spójrzmy na przyk³ad:
 <math>
@@ Linia 102: / Linia 91: @@
 </math>
-Wed³ug semantyki z poprzedniego zadania wyra¿nie to nie ma warto¶ci,
+Według semantyki z poprzedniego zadania wyrażnie to nie ma wartości, bo w deklaracji <math>y = y+y</math> jest odwołanie do niezainicjowanej zmiennej.
-bo w deklaracji <math>y = y+y</math> jest odwo³anie do niezainicjowanej
+Natomiast w semantyce leniwej wyrażenie to obliczy się do wartości <math>14</math>, gdyż wyrażenie <math>y+y</math> nie będzie wogóle obliczane.
-zmiennej.
+Będzie tak dlatego, że w wyrażeniu <math>x+x</math> nie ma odwołań do zmiennej <math>y</math>.
-Natomiast w semantyce leniwej wyra¿enie to obliczy siê do warto¶ci
-<math>14</math>, gdy¿ wyra¿enie <math>y+y</math> nie bêdzie wogóle obliczane.
-Bêdzie tak dlatego, ¿e w wyra¿eniu <math>x+x</math> nie ma odwo³añ do
-zmiennej <math>y</math>.
 }}
-{{rozwiazanie||roz2|
-<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
+<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">
-Semantyka ''leniwa'' bêdzie bardzo podobna do tej z poprzedniego zadania.
+Semantyka ''leniwa'' będzie bardzo podobna do tej z poprzedniego zadania.
-Zasadnicza ró¿nica dotyczy informacji przechowywanej w stanie.
+Zasadnicza różnica dotyczy informacji przechowywanej w stanie.
-Dotychczas <math>s(x)</math> nala¿a³ do zbioru <math>\in \mathbf{Num}</math>, gdy¿ podwyra¿enie <math>e</math> w
+Dotychczas <math>s(x)</math> nalażał do zbioru <math>\in \mathbf{Num}</math>, gdyż podwyrażenie <math>e</math> w <math>\mathbf{let}\, x = e \,\mathbf{in}\, \ldots</math> obliczało sie natychmiast.
-<math>\mathbf{let}\, x = e \,\mathbf{in}\, \ldots</math> oblicza³o sie natychmiast.
+Jeśli chcemy opóżnic obliczenie tego podwyrażenia, to w <math>s(x)</math> powinniśmy zapamiętać całe (nieobliczone) wyrażenie <math>e</math> wraz ze stanem bieżącym.
-Je¶li chcemy opó¿nic obliczenie tego podwyra¿enia, to w
-<math>s(x)</math> powinni¶my zapamiêtaæ ca³e (nieobliczone) wyra¿enie <math>e</math>
-wraz ze stanem bie¿±cym.
 Czyli
 <math>
-\mathbf{State} \, = \, \mathbf{Var} \to_{\mathrm{fin}} \mathbf{Exp} \times \mathbf{State}.
+\mathbf{State} \, = \, \mathbf{Var} \to_{\mathrm{fin}} \mathbf{Exp} \times \mathbf{State}</math>
-</math>
-Np. odpowiednia regu³a dla wyra¿enia <math>\mathbf{let}\,</math> w semantyce
+Np. odpowiednia reguła dla wyrażenia <math>\mathbf{let}\ </math>, w semantyce małych kroków mogłaby wyglądać następująco:
-ma³ych kroków mog³aby wygl±daæ nastêpuj±co:
 <math>
-\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2, s \,\Longrightarrow\, e_2, s[x \mapsto (e_1, s)].
+\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2, s \,\Longrightarrow, e_2, s[x \mapsto (e_1, s)]</math>
-</math>
-Czyli stan zawiera, dla ka¿dej zmiennej, parê
+Czyli stan zawiera, dla każdej zmiennej, parę (wyrażenie definiujące, stan w momencie deklaracji).
-(wyra¿enie definiuj±ce, stan w momencie deklaracji).
-Uwa¿nego czytelnika zapewne zaniepokoi³ fakt, ¿e <math>\mathbf{State}</math>
+Uważnego Czytelnika zapewne zaniepokoił fakt, że <math>\mathbf{State}</math> stoi zarówno po lewej, jak i po prawej stronie równania
-stoi zarówno po lewej jak i po prawej stronie równania
 <math>
-\mathbf{State} \, = \, \mathbf{Var} \to_{\mathrm{fin}} \mathbf{Exp} \times \mathbf{State}.
+\mathbf{State} \, = \, \mathbf{Var} \to_{\mathrm{fin}} \mathbf{Exp} \times \mathbf{State}</math>
-</math>
+Również zapis <math>s[x \mapsto (e_1, s)]</math> może wzbudzić niepokój, gdyż sugeruje on, iż <math>s(x)</math> zawiera jako jeden z elementów pary obiekt "tego samego typu" co <math>s</math>.
-Równie¿ zapis <math>s[x \mapsto (e_1, s)]</math> mo¿e wzbudziæ niepokój,
+Formalnego rozwiązania tego typu dylematów dostarcza teoria dziedzin.
-gdy¿ sugeruje on, i¿ <math>s(x)</math> zawiera, jako jeden z elementów pary,
+Natomiast na użytek semantyki operacyjnej wystarczy, jeśli uznamy, iż równanie
-obiekt ''tego samego typu'' co <math>s</math>.
-Formalnego rozwi±zania tego typu dylematów dostarcza teoria dziedzin.
-Natomiast na u¿ytek semantyki operacyjnej wystarczy, je¶li
-uznamy, i¿ równanie
 <math>
 \mathbf{State} \, = \, \mathbf{Var} \to_{\mathrm{fin}} \mathbf{Exp} \times \mathbf{State}
 </math>
-stanowi skrótowy zapis nastêpuj±cej definicji.
+stanowi skrótowy zapis następującej definicji.
-Zdefiniujmy <math>\mathbf{State}_0, \mathbf{State}_1, \ldots</math> nastêpuj±co:
+Zdefiniujmy <math>\mathbf{State}_0, \mathbf{State}_1, \ldots</math> następująco:
 <math>
@@ Linia 164: / Linia 138: @@
 </math>
-i przyjmijmy, ¿e
+i przyjmijmy, że
 <math>
-\mathbf{State} = \bigcup_{n \in \nat} \mathbf{State}_{n}
+\mathbf{State} = \bigcup_{n \in nat} \mathbf{State}_{n}
 </math>
-Tranzycje bêd± znów postaci:
+Tranzycje będą znów postaci:
 <math>
-e, s \,\longrightarrow\, n.
+e, s \,\longrightarrow\, n</math>
-</math>
+Podamy tylko reguły dla wystąpienia zmiennej i dla wyrażenia <math>\mathbf{let}\ </math>,.
-Podamy tylko regu³y dla wyst±pienia zmiennej i dla wyra¿enia
+Reguły dla pozostałych konstrukcji języka pozostają praktycznie bez zmian.
-<math>\mathbf{let}\,</math>. Regu³y dla pozosta³ych konstrukcji jêzyka pozostaj± praktycznie bez zmian.
 <math>
@@ Linia 188: / Linia 161: @@
 </div></div>
-}}
@@ Linia 194: / Linia 167: @@
-Rozwa¿my teraz zupe³nie inny mechanizm wi±zania identyfikatorów,
+Rozważmy teraz zupełnie inny mechanizm wiązania identyfikatorów zwany ''wiązaniem dynamicznym''.
-zwany ''wi±zaniem dynamicznym''.
+Dla odróżnienia, dotychczasowy sposób wiązania (widoczności) identyfikatorów będziemy nazywać ''wiązaniem statycznym''.
-Dla odró¿nienia, dotychczasowy sposób wi±zania (widoczno¶ci)
+Oto przykładowe wyrażenie:
-identyfikatorów bêdziemy nazywaæ ''wi±zaniem statycznym''.
-Oto przyk³adowe wyra¿enie:
 <math>
@@ Linia 204: / Linia 175: @@
 </math>
-które nie ma warto¶ci w pustym stanie pocz±tkowym,
+które nie ma wartości w pustym stanie początkowym, według semantyk z poprzednich zadań, ponieważ odwołanie do zmiennej <math>x</math> w deklaracji <math>y = x+1</math> jest niepoprawne.
-wed³ug semantyk z poprzednich zadañ, poniewa¿
+Tak samo jest nawet w semantyce leniwej, gdyż wartość zmiennej <math>y</math> będzie w końcu policzona i będzie wymagała odwołania do <math>x</math> w stanie pustym.
-odwo³anie do zmiennej <math>x</math> w deklaracji <math>y = x+1</math>
-jest niepoprawne.
-Tak samo jest nawet w semantyce leniwej, gdy¿ warto¶æ zmiennej
-<math>y</math> bêdzie w koñcu policzona, i bêdzie wymaga³a odwo³ania do <math>x
-</math> w stanie pustym.
-Natomiast wyobra¿my sobie, ¿e zmieniamy semantykê leniw± nastêpuj±co:
+Natomiast wyobrażmy sobie, że zmieniamy semantykę leniwą następująco: odwołanie do zmiennej <math>x</math> podczas obliczania wartości <math>y</math> będzie odnosiło się nie do stanu w momencie deklaracji <math>y</math>, ale do stanu w momencie ''odwołania'' do <math>y</math>.
-odwo³anie do zmiennej <math>x</math> podczas obliczania warto¶ci <math>y</math>
+Jest to dość rewolucyjna zmiana, zapewne sprzeczna z intuicjami programisty (statyczne reguły widoczności zamieniamy na ''dynamiczne'').
-bêdzie odnosi³o siê nie do stanu w momencie deklaracji <math>y</math>,
+W szczególności powyższe wyrażenie policzy się w semantyce dynamicznej do wartości 11, ponieważ stan w momencie odwołania do zmiennej <math>y</math> przypisuje zmiennej <math>x</math> wartość 10 !
-ale do stanu w momencie ''odwo³ania'' do <math>y</math>.
-Jest to do¶æ rewolucyjna zmiana, zapewne sprzeczna z intuicjami
-programisty (statyczne regu³y widoczno¶ci zamieniamy na
-''dynamiczne''). W szczególno¶ci powy¿sze wyra¿enie policzy siê
-w semantyce dynamicznej do warto¶ci 11, poniewa¿ stan w momencie
-odwo³ania do zmiennej <math>y</math> przypisuje zmiennej <math>x</math>
-warto¶æ 10 !
-Napisz semantykê naturaln± dla wi±zania dynamicznego.
+Napisz semantykę naturalną dla wiązania dynamicznego.
 }}
-{{rozwiazanie||roz3|
-<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
+<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">
-Teraz w stanie wystarczy przechowywaæ ''wyra¿enie'' definiuj±ce
+Teraz w stanie wystarczy przechowywać "wyrażenie" definiujące wartość danej zmiennej:
-warto¶æ danej zmiennej:
 <math>
-\mathbf{State} = \mathbf{Var} \to_{\mathrm{fin}} \mathbf{Exp}.
+\mathbf{State} = \mathbf{Var} \to_{\mathrm{fin}} \mathbf{Exp}</math>
-</math>
-Nie potrzebujemy zapamiêtywaæ stanu, w którym byli¶my w momencie
+Nie potrzebujemy zapamiętywać stanu, w którym byliśmy w momencie deklaracji.
-deklaracji. Do obliczenia zapamiêtanego wyra¿enia u¿yjemy stanu,
+Do obliczenia zapamiętanego wyrażenia użyjemy stanu, w którym będziemy w momencie odwołania do danej zmiennej.
-w którym bêdziemy w momencie odwo³ania do danej zmiennej.
+Znów podajemy tylko reguły dla wystąpienia zmiennej i dla wyrażenia <math>\mathbf{let}\ </math>,, gdyż pozostałe reguły pozostają bez zmian
-Znów podajemy tylko regu³y dla wyst±pienia zmiennej i dla
-wyra¿enia <math>\mathbf{let}\,</math>, gdy¿ pozosta³e regu³y pozostaj± bez zmian
 <math>
@@ Linia 254: / Linia 210: @@
 </math>
-'''Pytanie:''' czy <math>\mathbf{let}\, x = x+1 \,\mathbf{in}\, x</math> oblicza siê do jakiej¶
+'''Pytanie:''' czy <math>\mathbf{let}\, x = x+1 \,\mathbf{in}\, x</math> oblicza się do jakiejś wartości w stanie <math>\emptyset</math>?
-warto¶ci w stanie <math>\emptyset</math>?
 </div></div>
-}}
+== Prosty język funkcyjny ==
-== Prosty jêzyk funkcyjny ==
+{{cwiczenie|4 (przekazywanie parametru przez wartość)|cw4|
-{{cwiczenie|4 (przekazywanie parametru przez warto¶æ)|cw4|
+Rozważmy prosty język funkcyjny <math>F</math> rozszerzający język wyrażeń z poprzednich zadań następująco:
-Rozwa¿my prosty jêzyk funkcyjny <math>F</math> rozszerzaj±cy
-jêzyk wyra¿eñ z poprzednich zadañ nastêpuj±co:
 <math>
@@ Linia 277: / Linia 229: @@
 </math>
-''Lambda-abstrakcja'' <math>\lambda x.e</math> reprezentuje anonimow±
+''Lambda-abstrakcja'' <math>\lambda x.e</math> reprezentuje anonimową (nienazwaną) funkcję jednoargumentową, natomiast wyrażenie <math>e_1(e_2)</math> to ''aplikacja'' <math>e_1</math> do <math>e_2</math> (wyrażenie <math>e_1</math> powinno zatem obliczać się do funkcji).
-(nienazwan±) funkcjê jednoargumentow±, natomiast wyra¿enie
-<math>e_1(e_2)</math> to ''aplikacja'' <math>e_1</math> do <math>e_2</math> (wyra¿enie
-<math>e_1</math> powinno zatem obliczaæ siê do funkcji).
 Np.
 <math>
-(\lambda x. x+3)(2) \,\longrightarrow\, 5.
+(\lambda x. x+3)(2) \,\longrightarrow\, 5</math>
-</math>
-Przyjmijmy statyczn± widoczno¶æ identyfikatorów.
+Przyjmijmy statyczną widoczność identyfikatorów.
-Mo¿liwe s± ró¿ne mechanizmy przekazywania parametrów.
+Możliwe są różne mechanizmy przekazywania parametrów.
-Na razie wybierzmy mechanizm przekazywania przez warto¶æ,
+Na razie wybierzmy mechanizm przekazywania przez wartość,
-zapewne doskonale znany Czytelnikowi: wyra¿enie
+zapewne doskonale znany Czytelnikowi: wyrażenie będące parametrem aktualnym jest obliczane przed wywołaniem funkcji, czyli w stanie, w którym jesteśmy z momencie wywołania funkcji.
-bêd±ce parametrem aktualnym jest obliczane przed wywo³aniem funkcji,
-czyli w stanie, w którym jeste¶my z momencie wywo³ania funkcji.
-Zaproponuj semantykê naturaln± dla tego jêzyka
+Zaproponuj semantykę naturalną dla tego języka dla obydwu mechanizmów przekazywania parametrów.
-dla obydwu mechanizmów przekazywania parametrów.
 }}
-{{rozwiazanie||roz4|
-<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
+<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">
-Zauwa¿my, ¿e oprócz deklaracji zmiennych, równie¿
+Zauważmy, że oprócz deklaracji zmiennych, również machanizm przekazywania parametru do funkcji wymaga zmiany stanu.
-machanizm przekazywania parametru do funkcji wymaga zmiany stanu.
-Tranzycje bêd± postaci
+Tranzycje będą postaci
 <math>
@@ Linia 312: / Linia 257: @@
 </math>
-gdzie <math>v</math> reprezentuje warto¶æ, do której oblicza siê program <math>e</math>.
+gdzie <math>v</math> reprezentuje wartość, do której oblicza się program <math>e</math>.
-Z tym, ¿e warto¶ciami bêd± nie tylko warto¶ci liczbowe. Na przyk³ad
+Z tym, że wartościami będą nie tylko wartości liczbowe. Na przykład
 <math>
 \lambda x. x
 </math>
-oblicza siê równie¿ do pewnej warto¶æ, która w tym przypadku powinna reprezentowaæ
+oblicza się również do pewnej wartość, która w tym przypadku powinna reprezentować jakoś ''funkcję'' identycznościową. Wystarczającą reprezentacją funkcji będzie trójka:
-jako¶ ''funkcjê'' iudentyczno¶ciow±. Wystarczaj±c± reprezentacj±
+<math>\langle x, e, s \rangle</math>, gdzie <math>x</math> jest nazwą parametru formalnego, <math>e</math> jest ciałem funkcji, a <math>s</math> jest stanem, w którym należy obliczać wartość funkcji po zaaplikowaniu do jakiegoś parametru aktualnego.
-funkcji bêdzie trójka:
+Oto prosty przykład pokazujący, dlaczego powinniśmy pamiętać stan:
-<math>\langle x, e, s \rangle</math>,
-gdzie <math>x</math> jest nazw± parametru formalnego, <math>e</math> jest cia³em
-funkcji a <math>s</math> jest stanem, w którym nale¿y obliczaæ warto¶æ
-funkcji po zaaplikowaniu do jakiego¶ parametru aktualnego.
-Oto prosty przyk³ad pokazuj±cy, dlaczego powinni¶my pamiêtaæ stan:
 <math>
-\mathbf{let}\, x = 7 \,\mathbf{in}\, \mathbf{let}\, f = \lambda z.x+z \,\mathbf{in}\, \mathbf{let}\, x = f(1) \,\mathbf{in}\, f(10).
+\mathbf{let}\, x = 7 \,\mathbf{in}\, \mathbf{let}\, f = \lambda z.x+z \,\mathbf{in}\, \mathbf{let}\, x = f(1) \,\mathbf{in}\, f(10)</math>
-</math>
-Funkcja <math>f</math> zwiêksza parametr aktualny o <math>x</math>.
+Funkcja <math>f</math> zwiększa parametr aktualny o <math>x</math>.
-Program oblicza siê do warto¶ci <math>17</math>, gdy¿ wyst±pienie
+Program oblicza się do wartości <math>17</math>, gdyż wystąpienie zmiennej <math>x</math> w ciele funkcji <math>f</math> wiąże statycznie, a zatem odnosi się zawsze do deklaracji <math>x = 7</math>, mimo tego, że w momencie wywołania tej funkcji wartość zmiennej <math>x</math> wynosi <math>8</math>.
-zmiennej <math>x</math> w ciele funkcji <math>f</math> wi±¿e statycznie
-a zatem odnosi siê zawsze do deklaracji <math>x = 7</math>, mimo tego,
-¿e w momencie wywo³ania tej funkcji warto¶æ zmiennej <math>x</math>
-wynosi <math>8</math>.
-Oto jedyna regu³a, jakiej bêdziemy potrzebowaæ dla lambda-abstrakcji:
+Oto jedyna reguła, jakiej będziemy potrzebować dla lambda-abstrakcji:
 <math>
-\lambda x.e, s \,\longrightarrow\, \langle x, e, s \rangle
+\lambda x.e, s \,\longrightarrow\, \langle x, e, s \rangle</math>
-</math>
-Nie potrafimy zrobiæ z funkcj± <math>\lambda x. e</math> nic innego jak
+Nie potrafimy zrobić z funkcją <math>\lambda x. e</math> nic innego jak zapamiętać informację niezbędną do obliczania jej wartości w przyszłości.
-zapamiêtaæ informacjê niezbêdn± do obliczania jej warto¶ci
+Zatem zbiór wartości będzie następujący:
-w przyszlo¶ci.
-Zatem zbiór warto¶ci bedzie nastêpuj±cy:
 <math>
@@ Linia 352: / Linia 284: @@
 </math>
-a zbiór stanów <math>\mathbf{State}</math> okre¶lony jest nastêpuj±cym równaniem:
+a zbiór stanów <math>\mathbf{State}</math> określony jest następującym równaniem:
 <math>
-\mathbf{State} = \mathbf{Var} \to_{\mathrm{fin}} \mathbf{Values}.
+\mathbf{State} = \mathbf{Var} \to_{\mathrm{fin}} \mathbf{Values}</math>
-</math>
-Zacznijmy od sta³ych, zmiennych i lambda-abstrakcji:
+Zacznijmy od stałych, zmiennych i lambda-abstrakcji:
 <math>
@@ Linia 368: / Linia 299: @@
 </math>
-W regule dla zmiennej, <math>v</math> oznacza albo warto¶æ liczbow± albo
+W regule dla zmiennej, <math>v</math> oznacza albo wartość liczbową albo funkcyjną.
-funkcyjn±. Pomijamy regu³ê dla dodawania, bo jest ona identyczna
+Pomijamy regułę dla dodawania, bo jest ona identyczna jak dla gorliwej semantyki wyrażeń.
-jak dla gorliwej semantyki wyra¿eñ.
+Reguła dla <math>\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2</math> będzie prawie taka sama jak dla wyrażeń, z tą różnicą, że wyrażenie <math>e_1</math> definiujące wartość zmiennej <math>x</math> może się teraz obliczać do wartości funkcyjnej, np. <math>\mathbf{let}\, x = (\lambda y.y+y) \,\mathbf{in}\, x(0)</math>.
-Regu³a dla <math>\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2</math> bêdzie prawie taka sama jak dla wyra¿eñ,
-z t± ró¿nic±, ¿e wyra¿enie <math>e_1</math> definiuj±ce warto¶æ zmiennej <math>x</math>
-mo¿e siê teraz obliczaæ do warto¶ci funkcyjnej, np.
-<math>\mathbf{let}\, x = (\lambda y.y+y) \,\mathbf{in}\, x(0)</math>.
 <math>
@@ Linia 381: / Linia 308: @@
 </math>
-Pozosta³a nam ju¿ tylko regu³a dla aplikacji: najpierw oblicz funkcjê;
+Pozostała nam już tylko reguła dla aplikacji: najpierw oblicz funkcję; następnie oblicz wartość parametru aktualnego; wreszcie przekaż ją do ciała funkcji (czyli oblicz ciało funkcji w zmodyfikowanym stanie):
-nastêpnie oblicz warto¶æ parametru aktualnego; wreszcie przeka¿ j±
-do cia³a funkcji (czyli oblicz cia³o funkcji w zmodyfikowanym stanie):
 <math>
@@ Linia 392: / Linia 317: @@
 </math>
-Zwróæmy uwagê na wymóg, ¿e <math>e_1</math> oblicza siê do warto¶ci
+Zwróćmy uwagę na wymóg, że <math>e_1</math> oblicza się do wartości funkcyjnej <math>\langle x, e, s' \rangle</math>.
-funkcyjnej <math>\langle x, e, s' \rangle</math>.
+W szczególności np. wyrażenie <math>7(3+4)</math> jest niepoprawne.
-W szczególno¶ci np. wyra¿enie <math>7(3+4)</math> jest
+Natomiast parametr aktualny nie musi być liczbą, może być funkcją, np. w programie:
-niepoprawne. Natomiast parametr aktualny nie musi byæ liczb±, mo¿e byæ
-funkcj±, np. w programie:
 <math>
@@ Linia 403: / Linia 326: @@
 </math>
-który oblicza siê do warto¶ci <math>8</math>.
+który oblicza się do wartości <math>8</math>.
 </div></div>
-}}
-{{cwiczenie|5 (przekazywanie parametru przez nazwê)|cw5|
+{{cwiczenie|5 (przekazywanie parametru przez nazwę)|cw5|
-Zaproponuj ''leniw±'' semantykê jêzyka <math>F</math> z mechnizmem
+Zaproponuj ''leniwą'' semantykę języka <math>F</math> z mechnizmem przekazywanie parametru "przez nazwę".
-przekazywanie parametru ''przez nazwê''.
+Mechanizm ten stanowi leniwy odpowiednik przekazywania przez wartość: nie obliczamy wyrażenia będącego parametrem aktualnym, a zamiast jego wartości przekazujemy do funkcji to wyrażenie wraz ze
-Mechanizm ten stanowi leniwy odpowiednik przekazywania przez warto¶æ:
+stanem z miejsca wywołania funkcji.
-nie obliczamy wyra¿enia bêd±cego parametrem aktualnym, a zamiast
+To ten stan bedzie brany pod uwagę, gdy obliczana będzie wartość parametru, tzn. przy odwołaniu w ciele funkcji do parametru formalnego. Oto przykład programu:
-jego warto¶ci przekazujemy do funkcji to wyra¿enie wraz ze
-stanem z miejsca wywo³ania funkcji.
-To ten stan bedzie brany pod uwagê, gdy obliczana bêdzie
-warto¶æ parametru, tzn. przy odwo³aniu w ciele funkcji do
-parametru formalnego. Oto przyk³ad programu:
 <math>
@@ Linia 426: / Linia 344: @@
 </math>
-który w stanie pustym (wszystkie zmienne nieokre¶lone)
+który w stanie pustym (wszystkie zmienne nieokreślone)
-nie ma warto¶ci przy przekazywaniu parametru przez warto¶æ
+nie ma wartości przy przekazywaniu parametru przez wartość
-(bo odwo³anie do zmiennej <math>y</math> jest niepoprawne) a oblicza siê
+(bo odwołanie do zmiennej <math>y</math> jest niepoprawne), a oblicza się
-do warto¶ci <math>7</math> je¶li wybierzemy mechanizm przekazywania przez
+do wartości <math>7</math> jeśli wybierzemy mechanizm przekazywania przez
-nazwê.
+nazwę.
 }}
-{{rozwiazanie||roz5|
+<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">
-<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
+Zbiór wartości <math>\mathbf{Values}</math> stojących po prawej stronie symbolu <math>\,\longrightarrow\ </math>, będzie taki sam jak w poprzednim zadaniu.
+Natomiast zbiór stanów taki sam jak w semantyce leniwej wyrażeń:
-Zbiór warto¶ci <math>\mathbf{Values}</math> stoj±cych po prawej stronie symbolu <math>\,\longrightarrow\,</math>
-bêdzie taki sam jak w poprzednim zadaniu.
-Natomiast zbiór stanów taki sam jak w semantyce leniwej wyra¿eñ:
 <math>
-\mathbf{State} = \mathbf{Var} \to_{\mathrm{fin}} \mathbf{Exp} \times \mathbf{State}.
+\mathbf{State} = \mathbf{Var} \to_{\mathrm{fin}} \mathbf{Exp} \times \mathbf{State}</math>
-</math>
-Podamy tylko trzy regu³y: dla wyst±pienie zmiennej, deklaracji <math>\mathbf{let}\,</math>
+Podamy tylko trzy reguły: dla wystąpienie zmiennej, deklaracji <math>\mathbf{let}\ </math>, i aplikacji -- wszystkie pozostałe reguły pozostają takie same jak w poprzednim zadaniu.
-i aplikacji -- wszystkie pozosta³e regu³y pozostaj± w³a¶ciwie
-takie same jak w poprzednim zadaniu.
 <math>
@@ Linia 466: / Linia 380: @@
 </math>
-Podstawowa ró¿nica w ostatnej regule w porównaniu do poprzedniego
+Podstawowa różnica w ostatnej regule w porównaniu do poprzedniego zadania to ''brak ewaluacji'' parametru aktualnego <math>e_2</math>.
-zadania to ''brak ewaluacji'' parametru aktualnego <math>e_2</math>.
+Zwróćmy też uwagę na wyrażenie <math>s'[x \mapsto (e_2, s)]</math>, w którym <math>s \neq s'</math>.
-Zwróæmy te¿ uwagê na wyra¿enie
+Stany, których potrzebowaliśmy dotychczas podczas poprzednich zajęć, miały zawsze postać <math>s[x \mapsto (e, s)]</math>.
-<math>s'[x \mapsto (e_2, s)]</math>, w którym <math>s \neq s'</math>.
-Stany, których potrzebowali¶my dotychczas podczas poprzednich zajêæ, mia³y zawsze postaæ
-<math>s[x \mapsto (e, s)</math>.
 </div></div>
-}}
 == Zadania domowe ==
@@ Linia 482: / Linia 391: @@
 {{cwiczenie|1|cw1.dom|
-Podaj przyk³ad wyra¿enia takiego, które:
+Podaj przykład wyrażenia takiego, które:
-* ma warto¶æ w semantyce statycznej i dynamicznej, ale w ka¿dej inn±
+* ma wartość w semantyce statycznej i dynamicznej, ale w każdej inną
-* ma warto¶æ w semantyce leniwej a nie ma w dynamicznej
+* ma wartość w semantyce leniwej, a nie ma w dynamicznej
-* ma warto¶æ w semantyce dynamicznej a nie ma w leniwej.
+* ma wartość w semantyce dynamicznej, a nie ma w leniwej.
 }}
@@ Linia 492: / Linia 401: @@
 {{cwiczenie|2|cw2.dom|
-W semantyce leniwej wyra¿eñ, je¶li jest wiele odwo³añ do jakiej¶
+W semantyce leniwej wyrażeń, jeśli jest wiele odwołań do jakiejś zmiennej, to obliczenie wartości tej zmiennej nastąpi za każdym razem od nowa.
-zmiennej, to obliczenie warto¶ci tej zmiennej nast±pi za ka¿dym razem
+Zmodyfikuj tę semantykę tak, aby wartość ta była obliczana ''co najwyżej'' raz.
-od nowa. Zmodyfikuj tê semantykê tak, aby warto¶æ ta by³a obliczana
+Zatem po pierwszym odwołaniu do zmiennej, jej obliczona wartość powinna zostać umieszczona w stanie, zastępując parę (wyrażenie, stan).
-''co najwy¿ej'' raz.
-Zatem po pierwszym odwo³aniu do zmiennej, jej obliczona warto¶æ
-powinna zostaæ umieszczona w stanie, zastêpuj±c parê (wyra¿enie, stan).
 }}
@@ Linia 503: / Linia 409: @@
 {{cwiczenie|3|cw3.dom|
-Zaproponuj ''dynamiczne'' odpowiedniki obydwu ''statycznych'' semantyk dla
+Zaproponuj ''dynamiczne'' odpowiedniki obydwu ''statycznych'' semantyk dla języka funkcyjnego <math>F</math>.
-jêzyka funkcyjnego <math>F</math>.
+Czyli zakładamy, że widoczność identyfikatorów, m.in. w ciele funkcji, jest dynamiczna.
-Czyli zak³adamy, ¿e widoczno¶æ identyfikatorów, m.in. w ciele funkcji,
+Oto przykład programu, który w semantyce statycznej oblicza się do wartości <math>12</math>, a w dynamicznej do wartości <math>5</math>
-jest dynamiczna.
+(parametr przekazywany przez wartość):
-Oto przyk³ad programu, który w semantyce statycznej oblicza siê do
-warto¶ci <math>12</math>, a w dynamicznej do warto¶ci <math>5</math>
-(parametr przekazywany przez warto¶æ):
 <math>
@@ Linia 517: / Linia 420: @@
 </math>
-Rozwa¿ dwa mechanizmy przekazywania parametrów:
+Rozważ dwa mechanizmy przekazywania parametrów:
-* przez warto¶æ
+* przez wartość
-* przez nazwê
+* przez nazwę
-Ten drugi mechanizm rozumiemy teraz nastêpuj±co. Parametr aktualny nie
+Ten drugi mechanizm rozumiemy teraz następująco: parametr aktualny nie jest obliczany w momencie zaaplikowania do niego funkcji,
-jest obliczany w momencie zaaplikowania do niego funkcji,
+a do ciała funkcji przekazuje się wyrażenie będące parametrem aktualnym.
-a do cia³a funkcji przekazuje siê wyra¿enie bêd±ce parametrem aktualnym.
+W momencie odwołania do parametru formalnego w ciele funkcji, wyrażenie
-W momencie odwo³ania do parametru formalnego w ciele funkcji,
+będące parametrem aktualnym jest obliczane w bieżącym stanie (a nie w stanie z miejsca wywołania funkcji).
-wyra¿enie
+Jako przykład rozważmy program:
-bêd±ce parametrem aktualnym jest obliczane w bie¿±cym stanie (a nie w
-stanie z miejsca wywo³ania funkcji).
-Jako przyk³ad pozwa¿my program:
 <math>
@@ Linia 535: / Linia 435: @@
 </math>
-Przy przekazywaniu przez warto¶æ, w stanie pustym program siê nie
+Przy przekazywaniu przez wartość w stanie pustym program się nie obliczy, ponieważ nie da się obliczyć parametru aktualnego <math>x</math>.
-obliczy, poniewa¿ nie da siê obliczyæ parametru aktualnego <math>x</math>.
+Natomiast przy przekazywaniu przez nazwę, parametr aktualny będzie obliczany dopiero w momencie odwołania do parametru formalnego <math>z</math>, czyli w momencie obliczania wartości wyrażenia <math>z + z</math>.
-Natomiast przy przekazywaniu przez nazwê, parametr aktualny bêdzie
+W stanie tym zmienna <math>x</math> ma już wartość, a zatem wartością całego programu będzie 21.
-obliczany dopiero w momencie odwo³ania do parametru formalnego <math>z
-</math>, czyli w momencie obliczania warto¶ci wyra¿enia <math>z + z</math>.
-W stanie tym zmienna <math>x</math> ma ju¿ warto¶æ, a zatem warto¶ci±
-ca³ego programu bêdzie 21.
 }}