Semantyka i weryfikacja programów/Ćwiczenia 4: Różnice pomiędzy wersjami
Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| Linia 3: | Linia 3: | ||
== 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ń (z <math>\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2</math>), | ||
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ą. | ||
| Linia 14: | Linia 14: | ||
{{cwiczenie|1 (semantyka gorliwa)|cw1| | |||
Napisz semantykę dużych kroków | Napisz semantykę dużych kroków | ||
| Linia 36: | Linia 37: | ||
\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2 | \mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2 | ||
</math> | </math> | ||
}} | |||
{{rozwiazanie||roz1| | |||
==== | <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 | ||
| Linia 44: | Linia 49: | ||
</math> | </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. | ||
| Linia 76: | Linia 81: | ||
</math> | </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> | |||
}} | |||
{{cwiczenie|2 (semantyka leniwa)|cw2| | |||
Zmodyfikuj semantykę z poprzedniego zadania, aby uzyskać | Zmodyfikuj semantykę z poprzedniego zadania, aby uzyskać | ||
| Linia 94: | Linia 103: | ||
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. | 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>. | zmiennej <math>y</math>. | ||
}} | |||
==== | {{rozwiazanie||roz2| | ||
<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 | Czyli | ||
| Linia 117: | Linia 129: | ||
</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: | ||
| Linia 127: | Linia 139: | ||
(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> | <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, | 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>. | 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 | ||
| Linia 142: | Linia 154: | ||
</math> | </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> | <math> | ||
| Linia 163: | Linia 175: | ||
</math> | </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> | <math> | ||
| Linia 175: | Linia 187: | ||
</math> | </math> | ||
</div></div> | |||
}} | |||
{{cwiczenie|3 y|cw3| | |||
Rozważmy teraz zupełnie inny mechanizm wiązania identyfikatorów, | Rozważmy teraz zupełnie inny mechanizm wiązania identyfikatorów, | ||
| Linia 190: | Linia 206: | ||
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. | 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. | </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. | ||
}} | |||
==== | {{rozwiazanie||roz3| | ||
<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 | ||
| Linia 223: | Linia 242: | ||
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> | <math> | ||
| Linia 235: | Linia 254: | ||
</math> | </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 242: | Linia 264: | ||
{{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: | ||
| Linia 254: | Linia 277: | ||
</math> | </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. | Np. | ||
| Linia 273: | Linia 296: | ||
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"> | |||
Zauważmy, że oprócz deklaracji zmiennych, również | Zauważmy, że oprócz deklaracji zmiennych, również | ||
| Linia 286: | Linia 312: | ||
</math> | </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> | <math> | ||
| Linia 294: | Linia 320: | ||
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>, | |||
<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ść | |||
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 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> | <math> | ||
\mathbf{let}\, x = 7 \,\mathbf{in}\, \mathbf{let}\, f = \lambda z.x+z | \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 | 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 | że w momencie wywołania tej funkcji wartość zmiennej <math>x</math> | ||
wynosi <math> 8 </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: | ||
| Linia 319: | Linia 343: | ||
</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 | 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: | |||
<math> | |||
v \in \mathbf{Values} = \mathbf{Num} \cup (\mathbf{Var} \times \mathbf{Exp} \times \mathbf{State}) | |||
</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> | <math> | ||
\mathbf{State} = | \mathbf{State} = \mathbf{Var} \to_{\mathrm{fin}} \mathbf{Values}. | ||
</math> | </math> | ||
| Linia 334: | Linia 361: | ||
<math> | <math> | ||
n, s \,\longrightarrow\, n | |||
\quad \quad | \quad \quad | ||
x, s \,\longrightarrow\, v \quad \mbox{ o ile } s(x) = v | x, s \,\longrightarrow\, v \quad \mbox{ o ile } s(x) = v | ||
| Linia 341: | Linia 368: | ||
</math> | </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>. | <math>\mathbf{let}\, x = (\lambda y.y+y) \,\mathbf{in}\, x(0)</math>. | ||
<math> | <math> | ||
| Linia 365: | Linia 392: | ||
</math> | </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 | 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: | ||
| Linia 376: | Linia 403: | ||
</math> | </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| | |||
Zaproponyj ''leniwą'' semantykę języka <math> F </math> z mechnizmem | Zaproponyj ''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ść: | ||
| Linia 399: | Linia 428: | ||
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"><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 | Natomiast zbiór stanów taki sam jak w semantyce leniwej wyrażeń: | ||
<math> | <math> | ||
\mathbf{State} = \mathbf{Var} \to_{\mathrm{fin}} \mathbf{Exp} \times | \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ą właściwie | i aplikacji -- wszystkie pozostałe reguły pozostają właściwie | ||
takie same jak w poprzednim zadaniu. | takie same jak w poprzednim zadaniu. | ||
| Linia 438: | Linia 467: | ||
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 | Zwróćmy też uwagę na wyrażenie | ||
<math> s'[x \mapsto (e_2, s)] </math>, w którym <math> s \neq 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>. | <math>s[x \mapsto (e, s)</math>. | ||
</div></div> | |||
}} | |||
| Linia 470: | Linia 502: | ||
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, | Czyli zakładamy, że widoczność identyfikatorów, m.in. w ciele funkcji, | ||
jest dynamiczna. | 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ść): | ||
| Linia 502: | Linia 534: | ||
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. | ||
Wersja z 08:20, 8 sie 2006
Zawartość
Napiszemy semantykę naturalną języka wyrażeń (z ), 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 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ń:
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:
Według semantyki z poprzedniego zadania wyrażnie to nie ma wartości, bo w deklaracji jest odwołanie do niezainicjowanej zmiennej. Natomiast w semantyce leniwej wyrażenie to obliczy się do wartości , gdyż wyrażenie nie będzie wogóle obliczane. Będzie tak dlatego, że w wyrażeniu nie ma odwołań do zmiennej .
Rozwiązanie
{{{3}}}
Ćwiczenie 3 y
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:
które nie ma wartości w pustym stanie początkowym, według semantyk z poprzednich zadań, ponieważ odwołanie do zmiennej w deklaracji jest niepoprawne. Tak samo jest nawet w semantyce leniwej, gdyż wartość zmiennej będzie w końcu policzona, i będzie wymagała odwołania do w stanie pustym.
Natomiast wyobrażmy sobie, że zmieniamy semantykę leniwą następująco: odwołanie do zmiennej podczas obliczania wartości będzie odnosiło się nie do stanu w momencie deklaracji , ale do stanu w momencie odwołania do . 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 przypisuje zmiennej 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 rozszerzający
język wyrażeń z poprzednich zadań następująco:
Lambda-abstrakcja reprezentuje anonimową (nienazwaną) funkcję jednoargumentową, natomiast wyrażenie to aplikacja do (wyrażenie powinno zatem obliczać się do funkcji). Np.
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ę)
Zaproponyj leniwą semantykę języka 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:
który w stanie pustym (wszystkie zmienne nieokreślone) nie ma wartości przy przekazywaniu parametru przez wartość (bo odwołanie do zmiennej jest niepoprawne) a oblicza się do wartości jeśli wybierzemy mechanizm przekazywania przez nazwę.
Rozwiązanie
{{{3}}}
Zadania domowe
Zadanie 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
Zadanie 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. 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).
Zadanie 3
Zaproponuj dynamiczne odpowiedniki obydwu statycznych semantyk dla języka funkcyjnego . 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 , a w dynamicznej do wartości (parametr przekazywany przez wartość):
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:
Przy przekazywaniu przez wartość, w stanie pustym program się nie obliczy, ponieważ nie da się obliczyć parametru aktualnego . Natomiast przy przekazywaniu przez nazwę, parametr aktualny będzie obliczany dopiero w momencie odwołania do parametru formalnego , czyli w momencie obliczania wartości wyrażenia . W stanie tym zmienna ma już wartość, a zatem wartością całego programu będzie 21.
