Semantyka i weryfikacja programów/Ćwiczenia 4

Treść

Napiszemy semantykę naturalną języka wyrażeń (z $\mathbf{𝐥}\mathbf{𝐞}\mathbf{𝐭}x=e_1\mathbf{𝐢}\mathbf{𝐧}{e}_2$), rozważymy strategię gorliwą (jak na wcześniejszych zajęciach) 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ń

Zadanie 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 (identyfikatory)\dots$

$e::=n|x|e_1+e_2|\mathbf{𝐢}\mathbf{𝐟}{e}_1\mathbf{𝐭}\mathbf{𝐡}\mathbf{𝐞}\mathbf{𝐧}{e}_2\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{e}_3|\mathbf{𝐥}\mathbf{𝐞}\mathbf{𝐭}x=e_1\mathbf{𝐢}\mathbf{𝐧}{e}_2$

Rozwiązanie

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

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

$n,s⟶n$

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

$\frac{e_1,s⟶n_1{e}_2,s⟶n_2}{e_1+e_2,s⟶n}\text{ o ile }n=n_1+n_2$

$\frac{e_1,s⟶n_1{e}_2,s[x\mapsto n]⟶n_2}{\mathbf{𝐥}\mathbf{𝐞}\mathbf{𝐭}x=e_1\mathbf{𝐢}\mathbf{𝐧}{e}_2,s⟶n_2}$

$\frac{e_1,s⟶n_1{n}_1\ne 0e_2,s⟶n_2}{\mathbf{𝐢}\mathbf{𝐟}{e}_1\mathbf{𝐭}\mathbf{𝐡}\mathbf{𝐞}\mathbf{𝐧}{e}_2\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{e}_3,s⟶n_2}$

$\frac{e_1,s⟶n_1{n}_1=0e_3,s⟶n_3}{\mathbf{𝐢}\mathbf{𝐟}{e}_1\mathbf{𝐭}\mathbf{𝐡}\mathbf{𝐞}\mathbf{𝐧}{e}_2\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{e}_3,s⟶n_3}$

Zauważmy, że opisanie zasięgu deklaracji $x=e_1$ nie predstawia w semantyce naturalnej żadnych trudności, w przeciwieństwie do semantyki małych kroków.

Zadanie 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:

$\mathbf{𝐥}\mathbf{𝐞}\mathbf{𝐭}x=7\mathbf{𝐢}\mathbf{𝐧}\mathbf{𝐥}\mathbf{𝐞}\mathbf{𝐭}y=y+y\mathbf{𝐢}\mathbf{𝐧}x+x$

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

Rozwiązanie

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

$\mathbf{𝐒}\mathbf{𝐭}\mathbf{𝐚}\mathbf{𝐭}\mathbf{𝐞}=\mathbf{𝐕}\mathbf{𝐚}\mathbf{𝐫}{\to }_{\mathrm{f}\mathrm{i}\mathrm{n}}\mathbf{𝐄}\mathbf{𝐱}\mathbf{𝐩}\times \mathbf{𝐒}\mathbf{𝐭}\mathbf{𝐚}\mathbf{𝐭}\mathbf{𝐞}.$

Odpowiednia reguła dla wyrażenia $\mathbf{𝐥}\mathbf{𝐞}\mathbf{𝐭}$ to

$\mathbf{𝐥}\mathbf{𝐞}\mathbf{𝐭}x=e_1\mathbf{𝐢}\mathbf{𝐧}{e}_2,s⟹e_2,s[x\mapsto (e_1,s)].$

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

${\mathbf{𝐒}\mathbf{𝐭}\mathbf{𝐚}\mathbf{𝐭}\mathbf{𝐞}}_0=\{\mathrm{\varnothing }\}$

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

i przyjmijmy, że

Parser nie mógł rozpoznać (nieznana funkcja „\nat”): {\displaystyle \mathbf{State} = \bigcup_{n \in \nat} \mathbf{State}_{n} }

Tranzycje będą znów postaci: $e,s⟶n.$ Podamy tylko reguły dla wystąpienia zmiennej i dla wyrażenia $\mathbf{𝐥}\mathbf{𝐞}\mathbf{𝐭}$. Pozostałe reguły pozostają praktyczanie bez zmian.

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

$\frac{e_2,s[x\mapsto (e_1,s)]⟶n}{\mathbf{𝐥}\mathbf{𝐞}\mathbf{𝐭}x=e_1\mathbf{𝐢}\mathbf{𝐧}{e}_2,s⟶n}$

Zadanie 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:

$\mathbf{𝐥}\mathbf{𝐞}\mathbf{𝐭}y=x+1\mathbf{𝐢}\mathbf{𝐧}\mathbf{𝐥}\mathbf{𝐞}\mathbf{𝐭}x=10\mathbf{𝐢}\mathbf{𝐧}y$

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

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

Napisz semantykę naturalną dla wiązania dynamicznego.

Rozwiązanie

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

$\mathbf{𝐒}\mathbf{𝐭}\mathbf{𝐚}\mathbf{𝐭}\mathbf{𝐞}=\mathbf{𝐕}\mathbf{𝐚}\mathbf{𝐫}{\to }_{\mathrm{f}\mathrm{i}\mathrm{n}}\mathbf{𝐄}\mathbf{𝐱}\mathbf{𝐩}.$

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

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

$\frac{e_2,s[x\mapsto e_1]⟶n}{\mathbf{𝐥}\mathbf{𝐞}\mathbf{𝐭}x=e_1\mathbf{𝐢}\mathbf{𝐧}{e}_2,s⟶n}$

Prosty język funkcyjny

Zadanie 1

....

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