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

Wersja z 08:00, 9 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:00, 9 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ń (z <math>\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2</math>),
+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 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 191: / Linia 191: @@
-{{cwiczenie|3 y|cw3|
+{{cwiczenie|3 (semantyka dynamiczna)|cw3|
-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|
-Zaproponyj ''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 480: / Linia 480: @@
-==== Zadanie 1 ====
+{{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.
+}}
-==== Zadanie 2 ====
+{{cwiczenie|2|cw2.dom|
-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. Zmoddyfikuj tę semantykę tak, aby po pierwszym odwołaniu
-do zmiennej, obliczona wartość tej zmiennej była umieszczana w stanie,
-zastępując parę (wyrażenie, stan).
+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).
+}}
-==== Zadanie 3 ====
+{{cwiczenie|3|cw3.dom|
 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 515: / 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 533: / 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.
+}}