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

Wersja z 08:09, 10 sie 2006

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ło-krokową 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

{{{3}}}

Ć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

{{{3}}}

Ć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

{{{3}}}

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

{{{3}}}

Ć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

{{{3}}}

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 pozważ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

Wersja z 08:09, 10 sie 2006

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ñ,
+Napiszemy semantykę naturalną języka wyrażeń,
-rozwa¿ymy strategiê gorliw± (jak na wcze¶niejszych zajêciach,
+rozważymy strategię gorliwą (jak na wcześniejszych zajęciach,
-w semantyce ma³ych kroków) i leniw±.
+w semantyce małych kroków) i leniwą.
-Rozwa¿ymy i statyczne i dynamiczne wi±zanie identyfikatorów.
+Rozważymy i statyczne i dynamiczne wiązanie identyfikatorów.
-Nastêpnie rozszerzymy ten jêzyk o lambda-abstrakcjê i aplikacjê,
+Następnie rozszerzymy ten język o lambda-abstrakcję i aplikację,
-otrzymuj±c prosty jêzyk funkcyjny.
+otrzymując prosty język funkcyjny.
-== Ró¿ne semantyki naturalne wyra¿eñ ==
+== Różne semantyki naturalne wyrażeń ==
@@ Linia 17: / Linia 17: @@
-Napisz semantykê du¿ych kroków
+Napisz semantykę dużych kroków
-dla jêzyka wyra¿eñ, którego semantykê ma³o-krokow±
+dla języka wyrażeń, którego semantykę mało-krokową
-napisali¶my na jednych z poprzednich æwiczeñ:
+napisaliśmy na jednych z poprzednich ćwiczeń:
 <math>
@@ Linia 44: / Linia 44: @@
 <div class="mw-collapsible mw-made=collapsible mw-collapsed"><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>.
-Oto regu³y semantyki naturalnej.
+Oto reguły semantyki naturalnej.
 <math>
@@ Linia 81: / Linia 81: @@
 </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
+w semantyce naturalnej żadnych trudności, w przeciwieństwie do
-semantyki ma³ych kroków.
+semantyki małych kroków.
 </div></div>
@@ Linia 92: / Linia 92: @@
-Zmodyfikuj semantykê z poprzedniego zadania, aby uzyskaæ
+Zmodyfikuj semantykę z poprzedniego zadania, aby uzyskać
-''leniw±'' ewaluacjê wyra¿eñ, zgodnie z dyrektyw±: nie obliczaj
+''leniwą'' ewaluację wyrażeń, zgodnie z dyrektywą: nie obliczaj
-wyra¿enia o ile jego wynik nie jest potrzebny
+wyrażenia o ile jego wynik nie jest potrzebny
-(albo: obliczaj warto¶æ wyra¿enia dopiero wtedy, gdy jego wynik jest
+(albo: obliczaj wartość wyrażenia dopiero wtedy, gdy jego wynik jest
-naprawdê potrzebny). Spójrzmy na przyk³ad:
+naprawdę potrzebny). Spójrzmy na przykład:
 <math>
@@ Linia 102: / Linia 102: @@
 </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
+bo w deklaracji <math>y = y+y</math> jest odwołanie do niezainicjowanej
 zmiennej.
-Natomiast w semantyce leniwej wyra¿enie to obliczy siê do warto¶ci
+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.
+<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
+Będzie tak dlatego, że w wyrażeniu <math>x+x</math> nie ma odwołań do
 zmiennej <math>y</math>.
 }}
@@ Linia 116: / Linia 116: @@
 <div class="mw-collapsible mw-made=collapsible mw-collapsed"><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
+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>
+<math>s(x)</math> powinniśmy zapamiętać całe (nieobliczone) wyrażenie <math>e</math>
-wraz ze stanem bie¿±cym.
+wraz ze stanem bieżącym.
 Czyli
@@ Linia 129: / Linia 129: @@
 </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>
@@ Linia 136: / Linia 136: @@
 </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
 <math>
 \mathbf{State} \, = \, \mathbf{Var} \to_{\mathrm{fin}} \mathbf{Exp} \times \mathbf{State}.
 </math>
-Równie¿ zapis <math>s[x \mapsto (e_1, s)]</math> mo¿e wzbudziæ niepokój,
+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,
+gdyż sugeruje on, iż <math>s(x)</math> zawiera, jako jeden z elementów pary,
 obiekt ''tego samego typu'' co <math>s</math>.
-Formalnego rozwi±zania tego typu dylematów dostarcza teoria dziedzin.
+Formalnego rozwiązania tego typu dylematów dostarcza teoria dziedzin.
-Natomiast na u¿ytek semantyki operacyjnej wystarczy, je¶li
+Natomiast na użytek semantyki operacyjnej wystarczy, jeśli
-uznamy, i¿ równanie
+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 164: @@
 </math>
-i przyjmijmy, ¿e
+i przyjmijmy, że
 <math>
@@ Linia 170: / Linia 170: @@
 </math>
-Tranzycje bêd± znów postaci:
+Tranzycje będą znów postaci:
 <math>
 e, s \,\longrightarrow\, n.
 </math>
-Podamy tylko regu³y dla wyst±pienia zmiennej i dla wyra¿enia
+Podamy tylko reguły dla wystąpienia zmiennej i dla wyrażenia
-<math>\mathbf{let}\,</math>. 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 194: / Linia 194: @@
-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)
+Dla odróżnienia, dotychczasowy sposób wiązania (widoczności)
-identyfikatorów bêdziemy nazywaæ ''wi±zaniem statycznym''.
+identyfikatorów będziemy nazywać ''wiązaniem statycznym''.
-Oto przyk³adowe wyra¿enie:
+Oto przykładowe wyrażenie:
 <math>
@@ Linia 204: / Linia 204: @@
 </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¿
+według semantyk z poprzednich zadań, ponieważ
-odwo³anie do zmiennej <math>x</math> w deklaracji <math>y = x+1</math>
+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
+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>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>
+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>,
+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>.
+ale do stanu w momencie ''odwołania'' do <math>y</math>.
-Jest to do¶æ rewolucyjna zmiana, zapewne sprzeczna z intuicjami
+Jest to dość rewolucyjna zmiana, zapewne sprzeczna z intuicjami
-programisty (statyczne regu³y widoczno¶ci zamieniamy na
+programisty (statyczne reguły widoczności zamieniamy na
-''dynamiczne''). W szczególno¶ci powy¿sze wyra¿enie policzy siê
+''dynamiczne''). W szczególności powyższe wyrażenie policzy się
-w semantyce dynamicznej do warto¶ci 11, poniewa¿ stan w momencie
+w semantyce dynamicznej do wartości 11, ponieważ stan w momencie
-odwo³ania do zmiennej <math>y</math> przypisuje zmiennej <math>x</math>
+odwołania do zmiennej <math>y</math> przypisuje zmiennej <math>x</math>
-warto¶æ 10 !
+wartość 10 !
-Napisz semantykê naturaln± dla wi±zania dynamicznego.
+Napisz semantykę naturalną dla wiązania dynamicznego.
 }}
@@ Linia 231: / Linia 231: @@
 <div class="mw-collapsible mw-made=collapsible mw-collapsed"><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>
@@ Linia 238: / Linia 238: @@
 </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. Do obliczenia zapamiêtanego wyra¿enia u¿yjemy stanu,
+deklaracji. 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
+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
+wyrażenia <math>\mathbf{let}\,</math>, gdyż pozostałe reguły pozostają bez zmian
 <math>
@@ Linia 254: / Linia 254: @@
 </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>
@@ Linia 261: / Linia 261: @@
-== 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
+Rozważmy prosty język funkcyjny <math>F</math> rozszerzający
-jêzyk wyra¿eñ z poprzednich zadañ nastêpuj±co:
+język wyrażeń z poprzednich zadań następująco:
 <math>
@@ Linia 277: / Linia 277: @@
 </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
+(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(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).
+<math>e_1</math> powinno zatem obliczać się do funkcji).
 Np.
@@ Linia 287: / Linia 287: @@
 </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,
+będące parametrem aktualnym jest obliczane przed wywołaniem funkcji,
-czyli w stanie, w którym jeste¶my z momencie wywo³ania 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.
 }}
@@ Linia 303: / Linia 303: @@
 <div class="mw-collapsible mw-made=collapsible mw-collapsed"><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.
-Tranzycje bêd± postaci
+Tranzycje będą postaci
 <math>
@@ Linia 312: / Linia 312: @@
 </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ê'' iudentyczno¶ciow±. Wystarczaj±c± reprezentacj±
+jakoś ''funkcję'' iudentycznościową. Wystarczającą reprezentacją
-funkcji bêdzie trójka:
+funkcji będzie trójka:
 <math>\langle x, e, s \rangle</math>,
-gdzie <math>x</math> jest nazw± parametru formalnego, <math>e</math> jest cia³em
+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 a <math>s</math> jest stanem, w którym należy obliczać wartość
-funkcji po zaaplikowaniu do jakiego¶ parametru aktualnego.
+funkcji po zaaplikowaniu do jakiegoś parametru aktualnego.
-Oto prosty przyk³ad pokazuj±cy, dlaczego powinni¶my pamiêtaæ stan:
+Oto prosty przykład pokazujący, dlaczego powinniśmy pamiętać stan:
 <math>
@@ Linia 330: / Linia 330: @@
 </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
+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,
+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>
+ż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>
@@ Linia 343: / Linia 343: @@
 </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
+zapamiętać informację niezbędną do obliczania jej wartości
-w przyszlo¶ci.
+w przyszlości.
-Zatem zbiór warto¶ci bedzie nastêpuj±cy:
+Zatem zbiór wartości bedzie następujący:
 <math>
@@ Linia 352: / Linia 352: @@
 </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>
@@ Linia 358: / Linia 358: @@
 </math>
-Zacznijmy od sta³ych, zmiennych i lambda-abstrakcji:
+Zacznijmy od stałych, zmiennych i lambda-abstrakcji:
 <math>
@@ Linia 368: / Linia 368: @@
 </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±. Pomijamy regu³ê dla dodawania, bo jest ona identyczna
+funkcyjną. 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ñ,
+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>
+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.
+może się teraz obliczać do wartości funkcyjnej, np.
 <math>\mathbf{let}\, x = (\lambda y.y+y) \,\mathbf{in}\, x(0)</math>.
@@ Linia 381: / Linia 381: @@
 </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±
+następnie oblicz wartość parametru aktualnego; wreszcie przekaż ją
-do cia³a funkcji (czyli oblicz cia³o funkcji w zmodyfikowanym stanie):
+do ciała funkcji (czyli oblicz ciało funkcji w zmodyfikowanym stanie):
 <math>
@@ Linia 392: / Linia 392: @@
 </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>.
-W szczególno¶ci np. wyra¿enie <math>7(3+4)</math> jest
+W szczególności np. wyrażenie <math>7(3+4)</math> jest
-niepoprawne. Natomiast parametr aktualny nie musi byæ liczb±, mo¿e byæ
+niepoprawne. Natomiast parametr aktualny nie musi być liczbą, może być
-funkcj±, np. w programie:
+funkcją, np. w programie:
 <math>
@@ Linia 403: / Linia 403: @@
 </math>
-który oblicza siê do warto¶ci <math>8</math>.
+który oblicza się do wartości <math>8</math>.
 </div></div>
@@ Linia 409: / Linia 409: @@
-{{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¶æ:
+Mechanizm ten stanowi leniwy odpowiednik przekazywania przez wartość:
-nie obliczamy wyra¿enia bêd±cego parametrem aktualnym, a zamiast
+nie obliczamy wyrażenia będącego parametrem aktualnym, a zamiast
-jego warto¶ci przekazujemy do funkcji to wyra¿enie wraz ze
+jego wartości przekazujemy do funkcji to wyrażenie wraz ze
-stanem z miejsca wywo³ania funkcji.
+stanem z miejsca wywołania funkcji.
-To ten stan bedzie brany pod uwagê, gdy obliczana bêdzie
+To ten stan bedzie brany pod uwagę, gdy obliczana będzie
-warto¶æ parametru, tzn. przy odwo³aniu w ciele funkcji do
+wartość parametru, tzn. przy odwołaniu w ciele funkcji do
-parametru formalnego. Oto przyk³ad programu:
+parametru formalnego. Oto przykład programu:
 <math>
@@ Linia 426: / Linia 426: @@
 </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ę.
 }}
@@ Linia 438: / Linia 438: @@
 <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>
+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.
+będzie taki sam jak w poprzednim zadaniu.
-Natomiast zbiór stanów taki sam jak w semantyce leniwej wyra¿eñ:
+Natomiast zbiór stanów taki sam jak w semantyce leniwej wyrażeń:
 <math>
@@ Linia 446: / Linia 446: @@
 </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± w³a¶ciwie
+i aplikacji -- wszystkie pozostałe reguły pozostają właściwie
 takie same jak w poprzednim zadaniu.
@@ Linia 466: / Linia 466: @@
 </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>.
-Zwróæmy te¿ uwagê na wyra¿enie
+Zwróćmy też uwagę na wyrażenie
 <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æ
+Stany, których potrzebowaliśmy dotychczas podczas poprzednich zajęć, miały zawsze postać
 <math>s[x \mapsto (e, s)</math>.
@@ Linia 482: / Linia 482: @@
 {{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 492: @@
 {{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
+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
+od nowa. Zmodyfikuj tę semantykę tak, aby wartość ta była obliczana
-''co najwy¿ej'' raz.
+''co najwyżej'' raz.
-Zatem po pierwszym odwo³aniu do zmiennej, jej obliczona warto¶æ
+Zatem po pierwszym odwołaniu do zmiennej, jej obliczona wartość
-powinna zostaæ umieszczona w stanie, zastêpuj±c parê (wyra¿enie, stan).
+powinna zostać umieszczona w stanie, zastępując parę (wyrażenie, stan).
 }}
@@ Linia 504: / Linia 504: @@
 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,
+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
+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>
+wartości <math>12</math>, a w dynamicznej do wartości <math>5</math>
-(parametr przekazywany przez warto¶æ):
+(parametr przekazywany przez wartość):
 <math>
@@ Linia 517: / Linia 517: @@
 </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,
-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,
+W momencie odwołania do parametru formalnego w ciele funkcji,
-wyra¿enie
+wyrażenie
-bêd±ce parametrem aktualnym jest obliczane w bie¿±cym stanie (a nie w
+będące parametrem aktualnym jest obliczane w bieżącym stanie (a nie w
-stanie z miejsca wywo³ania funkcji).
+stanie z miejsca wywołania funkcji).
-Jako przyk³ad pozwa¿my program:
+Jako przykład pozważmy program:
 <math>
@@ Linia 535: / Linia 535: @@
 </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
+Natomiast przy przekazywaniu przez nazwę, parametr aktualny będzie
-obliczany dopiero w momencie odwo³ania do parametru formalnego <math>z
+obliczany dopiero w momencie odwołania do parametru formalnego <math>z
-</math>, czyli w momencie obliczania warto¶ci wyra¿enia <math>z + z</math>.
+</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±
+W stanie tym zmienna <math>x</math> ma już wartość, a zatem wartością
-ca³ego programu bêdzie 21.
+całego programu będzie 21.
 }}