Semantyka i weryfikacja programów/Ćwiczenia 4: Różnice pomiędzy wersjami

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
następna edycja →
WizualnieWikikod
Sl (dyskusja | edycje)
101 edycji
Nie podano opisu zmian
 
Sl (dyskusja | edycje)
101 edycji
Nie podano opisu zmian
Linia 1: Linia 1:


== Treść ==
== Treść ==
Linia 47: Linia 48:
Oto reguły semantyki naturalnej.
Oto reguły semantyki naturalnej.


  <math>
  <center><math>
n, s \,\longrightarrow\, n
n, s \,\longrightarrow\, n
</math>
</math></center>


  <math>
  <center><math>
x, s \,\longrightarrow\, n \quad \mbox{ o ile } s(x) = n
x, s \,\longrightarrow\, n \quad \mbox{ o ile } s(x) = n
</math>
</math></center>


  <math>
  <center><math>
\frac{e_1, s \,\longrightarrow\, n_1 \quad e_2, s \,\longrightarrow\, n_2}
\frac{e_1, s \,\longrightarrow\, n_1 \quad e_2, s \,\longrightarrow\, n_2}
     {e_1 + e_2, s \,\longrightarrow\, n} \quad \mbox{ o ile } n = n_1 + n_2
     {e_1 + e_2, s \,\longrightarrow\, n} \quad \mbox{ o ile } n = n_1 + n_2
</math>
</math></center>


  <math>
  <center><math>
\frac{e_1, s \,\longrightarrow\, n_1 \quad e_2, s[x \mapsto n] \,\longrightarrow\, n_2}
\frac{e_1, s \,\longrightarrow\, n_1 \quad e_2, s[x \mapsto n] \,\longrightarrow\, n_2}
     {\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2, s \,\longrightarrow\, n_2}
     {\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2, s \,\longrightarrow\, n_2}
</math>
</math></center>


<math>
<center><math>
\frac{e_1, s \,\longrightarrow\, n_1 \quad n_1 \neq 0 \quad e_2, s \,\longrightarrow\, n_2}
\frac{e_1, s \,\longrightarrow\, n_1 \quad n_1 \neq 0 \quad e_2, s \,\longrightarrow\, n_2}
     {\mathbf{if}\, e_1 \,\mathbf{then}\, e_2 \,\mathbf{else}\, e_3, s \,\longrightarrow\, n_2}
     {\mathbf{if}\, e_1 \,\mathbf{then}\, e_2 \,\mathbf{else}\, e_3, s \,\longrightarrow\, n_2}
</math>
</math></center>


<math>
<center><math>
\frac{e_1, s \,\longrightarrow\, n_1 \quad n_1 = 0 \quad e_3, s \,\longrightarrow\, n_3}
\frac{e_1, s \,\longrightarrow\, n_1 \quad n_1 = 0 \quad e_3, s \,\longrightarrow\, n_3}
     {\mathbf{if}\, e_1 \,\mathbf{then}\, e_2 \,\mathbf{else}\, e_3, s \,\longrightarrow\, n_3}
     {\mathbf{if}\, e_1 \,\mathbf{then}\, e_2 \,\mathbf{else}\, e_3, s \,\longrightarrow\, n_3}
</math>
</math></center>


Zauważmy, że opisanie zasięgu deklaracji <math> x = e_1 </math> nie predstawia
Zauważmy, że opisanie zasięgu deklaracji <math> x = e_1 </math> nie predstawia
Linia 118: Linia 119:
Odpowiednia reguła dla wyrażenia <math> \mathbf{let}\, </math> to
Odpowiednia reguła dla wyrażenia <math> \mathbf{let}\, </math> to


<math>
<center><math>
\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2, s \,\Longrightarrow\, e_2, s[x \mapsto (e_1, s)].
\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2, s \,\Longrightarrow\, e_2, s[x \mapsto (e_1, s)].
</math>
</math></center>


Uważnego czytelnika zapewne zaniepokoił fakt, że <math> \mathbf{State} </math>
Uważnego czytelnika zapewne zaniepokoił fakt, że <math> \mathbf{State} </math>
Linia 160: Linia 161:
<math> \mathbf{let}\, </math>. Pozostałe reguły pozostają praktyczanie bez zmian.
<math> \mathbf{let}\, </math>. Pozostałe reguły pozostają praktyczanie bez zmian.


<math>
<center><math>
\frac{e, s' \,\longrightarrow\, n}
\frac{e, s' \,\longrightarrow\, n}
     {x, s \,\longrightarrow\, n} \quad \mbox{ o ile } s(x) = (e, s')
     {x, s \,\longrightarrow\, n} \quad \mbox{ o ile } s(x) = (e, s')
</math>
</math></center>


<math>
<center><math>
\frac{e_2, s[x \mapsto (e_1, s)] \,\longrightarrow\, n}
\frac{e_2, s[x \mapsto (e_1, s)] \,\longrightarrow\, n}
     {\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2, s \,\longrightarrow\, n}
     {\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2, s \,\longrightarrow\, n}
</math>  
</math></center>  




Linia 219: Linia 220:
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>
<center><math>
\frac{e, s \,\longrightarrow\, n}
\frac{e, s \,\longrightarrow\, n}
     {x, s \,\longrightarrow\, n} \quad \mbox{ o ile } s(x) = e
     {x, s \,\longrightarrow\, n} \quad \mbox{ o ile } s(x) = e
</math>  
</math></center>  


<math>
<center><math>
\frac{e_2, s[x \mapsto e_1] \,\longrightarrow\, n}
\frac{e_2, s[x \mapsto e_1] \,\longrightarrow\, n}
     {\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2, s \,\longrightarrow\, n}
     {\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2, s \,\longrightarrow\, n}
</math>
</math></center>




Wersja z 17:11, 27 lip 2006


Treść

Napiszemy semantykę naturalną języka wyrażeń (z 𝐥𝐞𝐭x=e1𝐢𝐧e2), 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|…

x::=…(identyfikatory)…

e::=n|x|e1+e2|𝐢𝐟e1𝐭𝐡𝐞𝐧e2𝐞𝐥𝐬𝐞e3|𝐥𝐞𝐭x=e1𝐢𝐧e2

Rozwiązanie

Przypomnijmy, że zbiór stanów to 𝐒𝐭𝐚𝐭𝐞=𝐕𝐚𝐫→fin𝐍𝐮𝐦

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

n,s⟶n
x,s⟶n o ile s(x)=n
e1,s⟶n1e2,s⟶n2e1+e2,s⟶n o ile n=n1+n2
e1,s⟶n1e2,s[x↦n]⟶n2𝐥𝐞𝐭x=e1𝐢𝐧e2,s⟶n2
e1,s⟶n1n1≠0e2,s⟶n2𝐢𝐟e1𝐭𝐡𝐞𝐧e2𝐞𝐥𝐬𝐞e3,s⟶n2
e1,s⟶n1n1=0e3,s⟶n3𝐢𝐟e1𝐭𝐡𝐞𝐧e2𝐞𝐥𝐬𝐞e3,s⟶n3

Zauważmy, że opisanie zasięgu deklaracji x=e1 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)∈𝐍𝐮𝐦, gdyż podwyrażenie e w 𝐥𝐞𝐭x=e𝐢𝐧… 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

𝐒𝐭𝐚𝐭𝐞=𝐕𝐚𝐫→fin𝐄𝐱𝐩×𝐒𝐭𝐚𝐭𝐞.

Odpowiednia reguła dla wyrażenia 𝐥𝐞𝐭 to

𝐥𝐞𝐭x=e1𝐢𝐧e2,s⟹e2,s[x↦(e1,s)].

Uważnego czytelnika zapewne zaniepokoił fakt, że 𝐒𝐭𝐚𝐭𝐞 stoi zarówno po lewej jak i po prawej stronie równania 𝐒𝐭𝐚𝐭𝐞=𝐕𝐚𝐫→fin𝐄𝐱𝐩×𝐒𝐭𝐚𝐭𝐞. Również zapis s[x↦(e1,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 𝐒𝐭𝐚𝐭𝐞=𝐕𝐚𝐫→fin𝐄𝐱𝐩×𝐒𝐭𝐚𝐭𝐞 stanowi skrótowy zapis następującej definicji. Zdefiniujmy 𝐒𝐭𝐚𝐭𝐞0,𝐒𝐭𝐚𝐭𝐞1,… następująco:

𝐒𝐭𝐚𝐭𝐞0={∅}

𝐒𝐭𝐚𝐭𝐞n+1=𝐕𝐚𝐫→fin𝐄𝐱𝐩×𝐒𝐭𝐚𝐭𝐞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 𝐥𝐞𝐭. Pozostałe reguły pozostają praktyczanie bez zmian.

e,s′⟶nx,s⟶n o ile s(x)=(e,s′)
e2,s[x↦(e1,s)]⟶n𝐥𝐞𝐭x=e1𝐢𝐧e2,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 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:

𝐒𝐭𝐚𝐭𝐞=𝐕𝐚𝐫→fin𝐄𝐱𝐩.

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

e,s⟶nx,s⟶n o ile s(x)=e
e2,s[x↦e1]⟶n𝐥𝐞𝐭x=e1𝐢𝐧e2,s⟶n


Prosty język funkcyjny

Zadanie 1

....


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
Źródło: „https://wazniak.mimuw.edu.pl/index.php?title=Semantyka_i_weryfikacja_programów/Ćwiczenia_4&oldid=6949”