Semantyka i weryfikacja programów/Ćwiczenia 4

Zawartość

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}$

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

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)$ nalażał do zbioru $\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{𝐞}.$

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

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

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

Uważnego czytelnika zapewne zaniepokoił fakt, że $\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}$

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

Prosty język funkcyjny

Zadanie 1

Rozszerzmy język wyrażeń następująco:

$e::=\dots |\lambda x.e|e_1(e_2)$

Lambda-abstrakcja $\lambda 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. $(lambdax.x+3)(2)⟶5.$

Przyjmijmy statyczną widoczność identyfikatorów. Możliwe są różne mechanizmy przekazywania parametrów. Rozważmy dwa:

• przez wartość
• przez nazwę

Pierwszy z nich jest 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. Drugi stanowi jakby 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.

Zaproponuj semantykę naturalną dla tego języka dla obydwu mechanizmów przekazywania parametrów (w dwóch wariantach).

Rozwiązanie

....

Zadanie 2

Zaproponuj dynamiczne odpowiedniki obydwu semantyk z poprzedniego zadania.

Rozwiązanie

....

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).