Semantyka i weryfikacja programów/Ćwiczenia 4

Zawartość

Napiszemy semantykę naturalną języka wyrażeń (z $𝐥 𝐞 𝐭 x = e_{1} 𝐢 𝐧 e_{2}$ ), 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ń

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

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

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

$n, s ⟶ n$

$x, s ⟶ n o ile s (x) = n$

$\frac{e_{1}, s ⟶ n_{1} e_{2}, s ⟶ n_{2}}{e_{1} + e_{2}, s ⟶ n} o ile n = n_{1} + n_{2}$

$\frac{e_{1}, s ⟶ n_{1} e_{2}, s [x \mapsto n_{1}] ⟶ n_{2}}{𝐥 𝐞 𝐭 x = e_{1} 𝐢 𝐧 e_{2}, s ⟶ n_{2}}$

$\frac{e_{1}, s ⟶ n_{1} n_{1} \neq 0 e_{2}, s ⟶ n_{2}}{𝐢 𝐟 e_{1} 𝐭 𝐡 𝐞 𝐧 e_{2} 𝐞 𝐥 𝐬 𝐞 e_{3}, s ⟶ n_{2}}$

$\frac{e_{1}, s ⟶ n_{1} n_{1} = 0 e_{3}, s ⟶ n_{3}}{𝐢 𝐟 e_{1} 𝐭 𝐡 𝐞 𝐧 e_{2} 𝐞 𝐥 𝐬 𝐞 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:

$𝐥 𝐞 𝐭 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

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 𝐍 𝐮 𝐦$ , gdyż podwyrażenie $e$ w $𝐥 𝐞 𝐭 x = e 𝐢 𝐧 \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

$𝐒 𝐭 𝐚 𝐭 𝐞 = 𝐕 𝐚 𝐫 \to_{f i n} 𝐄 𝐱 𝐩 \times 𝐒 𝐭 𝐚 𝐭 𝐞 .$

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

$𝐥 𝐞 𝐭 x = e_{1} 𝐢 𝐧 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 $𝐒 𝐭 𝐚 𝐭 𝐞$ stoi zarówno po lewej jak i po prawej stronie równania $𝐒 𝐭 𝐚 𝐭 𝐞 = 𝐕 𝐚 𝐫 \to_{f i n} 𝐄 𝐱 𝐩 \times 𝐒 𝐭 𝐚 𝐭 𝐞 .$ 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 $𝐒 𝐭 𝐚 𝐭 𝐞 = 𝐕 𝐚 𝐫 \to_{f i n} 𝐄 𝐱 𝐩 \times 𝐒 𝐭 𝐚 𝐭 𝐞$ stanowi skrótowy zapis następującej definicji. Zdefiniujmy ${𝐒 𝐭 𝐚 𝐭 𝐞}_{0}, {𝐒 𝐭 𝐚 𝐭 𝐞}_{1}, \dots$ następująco:

${𝐒 𝐭 𝐚 𝐭 𝐞}_{0} = {\emptyset}$

${𝐒 𝐭 𝐚 𝐭 𝐞}_{n + 1} = 𝐕 𝐚 𝐫 \to_{f i n} 𝐄 𝐱 𝐩 \times {𝐒 𝐭 𝐚 𝐭 𝐞}_{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 $𝐥 𝐞 𝐭$ . Reguły dla pozostałych konstrukcji języka pozostają praktycznie bez zmian.

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

$\frac{e_{2}, s [x \mapsto (e_{1}, s)] ⟶ n}{𝐥 𝐞 𝐭 x = e_{1} 𝐢 𝐧 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:

$𝐥 𝐞 𝐭 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

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

$𝐒 𝐭 𝐚 𝐭 𝐞 = 𝐕 𝐚 𝐫 \to_{f i n} 𝐄 𝐱 𝐩 .$

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 $𝐥 𝐞 𝐭$ , gdyż pozostałe reguły pozostają bez zmian

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

$\frac{e_{2}, s [x \mapsto e_{1}] ⟶ n}{𝐥 𝐞 𝐭 x = e_{1} 𝐢 𝐧 e_{2}, s ⟶ n}$

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

Prosty język funkcyjny

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

Zauważmy, że oprócz deklaracji zmiennych, również machanizm przekazywania parametru do funkcji wymaga zmiany stanu.

Tranzycje będą postaci

$e, s ⟶ v$

gdzie $v$ reprezentuje wartość, do której oblicza się program $e$ . Z tym, że wartościami będą nie tylko wartości liczbowe. Na przykład $λ x . x$ oblicza się również do pewnej wartość, która w tym przypadku powinna reprezentować jakoś funkcję iudentycznościową. Wystarczającą reprezentacją funkcji będzie trójka:

$⟨ x, e, s ⟩$ ,

gdzie $x$ jest nazwą parametru formalnego, $e$ jest ciałem funkcji a $s$ jest stanem, w którym należy obliczać wartość funkcji po zaaplikowaniu do jakiegoś parametru aktualnego. Oto prosty przykład pokazujący, dlaczego powinniśmy pamiętać stan:

$𝐥 𝐞 𝐭 x = 7 𝐢 𝐧 𝐥 𝐞 𝐭 f = λ z . x + z I 𝐥 𝐞 𝐭 x = f (1) 𝐢 𝐧 f (10) .$

Funkcja $f$ zwiększa parametr aktualny o $x$ . Program oblicza się do wartości $17$ , gdyż wystąpienie zmiennej $x$ w ciele funkcji $f$ wiąże statycznie a zatem odnosi się zawsze do deklaracji $x = 7$ , mimo tego, że w momewncie wywołania tej funkcji wartość zmiennej $x$ wynosi $8$ .

Oto jedyna reguła, jakiej będziemy potrzebować dla lambda-abstrakcji:

$λ x . e, s ⟶ ⟨ x, e, s ⟩$

Nie potrafimy zrobić z funkcją $λ x . e$ nic innego jak zapamiętać informację niezbędną do obliczania jej wartości w przyszlości.

Zatem zbiór wartości bedzie następujący: $v \in 𝐕 𝐚 𝐥 𝐮 𝐞 𝐬 = 𝐍 𝐮 𝐦 \cup 𝐕 𝐚 𝐫 \times 𝐄 𝐱 𝐩 \times 𝐒 𝐭 𝐚 𝐭 𝐞$ a zbiór stanów $𝐒 𝐭 𝐚 𝐭 𝐞$ określony jest następującym równaniem:

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathbf{State} = \\mathbf{Var} \to_{\mathrm{fin}} \mathbf{Values} } . </math>

Zacznijmy od stałych, zmiennych i lambda-abstrakcji:

Parser nie mógł rozpoznać (nieznana funkcja „\n”): {\displaystyle \n, s \,\longrightarrow\, n \quad \quad x, s \,\longrightarrow\, v \quad \mbox{ o ile } s(x) = v \quad \quad \lambda x.e, s \,\longrightarrow\, \langle x, e, s \rangle }

W regule dla zmiennej, $v$ oznacza albo wartość liczbową albo funkcyjną. Pomijamy regułę dla dodawania, bo jest ona identyczna jak dla gorliwej semantyki wyrażeń w jednym z poprzednich zadań. Reguła dla $𝐥 𝐞 𝐭 x = e_{1} 𝐢 𝐧 e_{2}$ będzie prawie taka sama jak dla wyrażeń, z tą różnicą, że wyrażenie $e_{1}$ definiujące wartość zmiennej $x$ może się teraz obliczać do wartości funkcyjnej, np. $𝐥 𝐞 𝐭 x = (λ y . y + y) 𝐢 𝐧 x (0)$ .

$\frac{e_{1}, s ⟶ v_{1} e_{2}, s [x \mapsto v_{1}] ⟶ v_{2}}{𝐥 𝐞 𝐭 x = e_{1} 𝐢 𝐧 e_{2}, s ⟶ v_{2}}$

Pozostała nam już tylko reguła dla aplikacji: najpierw oblicz funkcję; następnie oblicz wartość parametru aktualnego; wreszcie przekaż ją do ciała funkcji (czyli oblicz ciało funkcji w zmodyfikowanym stanie):

$\frac{e_{1}, s ⟶ ⟨ x, e, s^{'} ⟩ e_{2}, s ⟶ v^{'} e, s^{'} [x \mapsto v^{'}] ⟶ v}{e_{1} (e_{2}), s ⟶ v}$

Zwróćmy uwagę na wymóg, że $e_{1}$ oblicza się do wartości funkcyjnej $⟨ x, e, s^{'} ⟩$ . W szczególności np. wyrażenie $7 (3 + 4)$ jest niepoprawne. Natomiast parametr aktualny nie musi być liczbą, może być funkcją, np. w programie:

$𝐥 𝐞 𝐭 g = λ f . λ x . f (x) 𝐢 𝐧 g (λ x . x + 1) (7)$

który oblicza się do wartości $8$ .

Zadanie 2 (przekazywanie parametru przez nazwę)

Zaproponyj 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

Zbiór wartości $𝐕 𝐚 𝐥 𝐮 𝐞 𝐬$ stojących po prawej stronie symbolu $⟶$ będzie taki sam jak w poprzednim zadaniu. Natomiast zbiór stanów taki sam jak w semantyce leniwej w jednym z poprzedniich zadań:

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathbf{State} = \mathbf{Var} \to_{\mathrm{fin}} \mathbf{Exp} \times \\mathbf{State}. }

Podamy tylko trzy reguły: dla wystąpienie zmiennej, deklaracji $𝐥 𝐞 𝐭$ i aplikacji -- wszystkie pozostałe reguły pozostają właściwie takie same jak w poprzednim zadaniu.

$\frac{e, s^{'} ⟶ v}{x, s ⟶ v} o ile s (x) = (e, s^{'})$

$\frac{e_{2}, s [x \mapsto (e, s)] ⟶ v}{𝐥 𝐞 𝐭 x = e_{1} 𝐢 𝐧 e_{2}, s ⟶ v}$

$\frac{e_{1}, s ⟶ ⟨ x, e, s^{'} ⟩ e, s^{'} [x \mapsto (e_{2}, s)] ⟶ v}{e_{1} (e_{2}), s ⟶ v}$

Podstawowa różnica w ostatnej regule w porównaniu do poprzedniego zadania to brak ewaluacji parametru aktualnego $e_{2}$ . Zwróćmy też uwagę na wyrażenie $s^{'} [x \mapsto (e_{2}, s)]$ , w którym $s \neq s^{'}$ . stany, których potrzebowaliśmy dotychczas, miały zawsze postać $s [x \mapsto (e, s)$ .

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

Spis treści

Zawartość

Różne semantyki wyrażeń

Zadanie 1 (semantyka gorliwa)

Rozwiązanie

Zadanie 2 (semantyka leniwa)

Rozwiązanie

Zadanie 3 (semantyka dynamiczna)

Rozwiązanie

Prosty język funkcyjny

Zadanie 1 (przekazywanie parametru przez wartość)

Rozwiązanie

Zadanie 2 (przekazywanie parametru przez nazwę)

Rozwiązanie

Zadania domowe

Zadanie 1

Zadanie 2

Zadanie 3

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia