Semantyka i weryfikacja programów/Ćwiczenia 4

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 (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

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

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

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

$\mathbf{𝐥}\mathbf{𝐞}\mathbf{𝐭}y=x+1\mathbf{𝐢}\mathbf{𝐧}\mathbf{𝐥}\mathbf{𝐞}\mathbf{𝐭}x=10\mathbf{𝐢}\mathbf{𝐧}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 |\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.

$(\lambda 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:

$\mathbf{𝐥}\mathbf{𝐞}\mathbf{𝐭}f=\lambda x.7\mathbf{𝐢}\mathbf{𝐧}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¶æ):

$\mathbf{𝐥}\mathbf{𝐞}\mathbf{𝐭}x=7\mathbf{𝐢}\mathbf{𝐧}\mathbf{𝐥}\mathbf{𝐞}\mathbf{𝐭}f=\lambda z.z+x\mathbf{𝐢}\mathbf{𝐧}\mathbf{𝐥}\mathbf{𝐞}\mathbf{𝐭}x=0\mathbf{𝐢}\mathbf{𝐧}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:

$(\lambda z.\mathbf{𝐥}\mathbf{𝐞}\mathbf{𝐭}x=10\mathbf{𝐢}\mathbf{𝐧}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.