Semantica Operazionale StrutturataSemantica per riscrittura o riduzione o semplificazione basata sulla struttura dei termini che voglio semplificare

Si individuano dei termini (del linguaggio) che rappresentano direttamente dei valori, cioè che non possono essere ulteriormente semplificati.

Si danno delle regole di semplificazione in modo tale che ogni termine corretto si riduca ad uno e uno solo di quei termini che rappresentano valori

In realtà come nel caso denotazionale abbiamo bisogno di ambienti e stati per poter eseguire le semplificazioni.Quindi la semplificazione agisce su configurazioni, che consistono di un termine e del contesto in cui si vuole valutare il termine.

SOS a grandi passi per LWMolto simile alla semantica denotazionale

Come configurazioni usiamoConf = L Env States

[T] è l’insieme dei valori sintattici di tipo

T: [int] = {0,1,2,..-1,-2….}, [bool] = {true,false}

L = sNLs(LW) *

Una configurazione (t,r,s) è finale set = (ho rielaborato tutto il termine in esame usandolo per modificare ambiente e/o stato) ot Value+ (ho raggiunto un termine che rappresenta un valore)

Definiamo la semplificazione come relazione binaria sulle configurazioni: Conf Conf

Gli stessi della denotazionale tranne che cambia Value

Siccome la maggior parte delle semplificazioni non modifica gli ambienti introduciamo una notazione semplificata:

(t,s) r (t’,s’) sse (t,r,s) (t’,r,s’)

A grandi passi vuol dire che se derivo (t,r,s) (t’,r,s’), allora (t’,r,s’) è finale (non vado mai in uno stato intermedio, ma direttamente alla fine)

Espressioni

[e es] (r,s) = (v lv,s”)

[e] (r,s) = (v,s’) [es] (r,s’) = (lv,s”)

(x,s) r (s(r(x)),s)r(x) LocT

[x = e](r,s) =

[e](r,s) = (v ,s’)

(v,s’[v/r(x)])

[f(es)](r,s) = r(f)(lv,s’)

[es](r,s) = (lv ,s’)

[e + e’] (r,s) = (a,s”)

[e] (r,s) = (v,s’) [e’] (r,s’) = (v’,s”)v + v’ =a

a è la rappresentazione sintattica del valore ottenuto sommando i valori rappresentati da v e v’

Denotazionale

(e es, s) r (v lv,s”)

(e,s) r (v,s’) (es,s’) r (lv,s”)

SOS a grandi passi

[x](r,s) = (s(r(x)),s)r(x) LocT

(x=e,s) r (v,s’[v/r(x)]))

(e,s) r (v,s’)

(f(es),s) r r(f)(lv,s’)

(es,s) r (lv,s’)

(e+e’,s) r (a,s”)

(e,s) r (v,s’) (e’,s’) r (v’,s”)v + v’ =a

Espressioni completamento

(x,s) r (s(r(x)),s)r(x) LocT

(e es, s) r (v lv,s”)

(e,s) r (v,s’) (es,s’) r (lv,s”)

In realtà bisogna anche aggiungere tutti i controlli di tipo

(x=e,s) r (v,s’[v/r(x)]))

(e,s) r (v,s’)

(f(es),s) r r(f)(lv,s’)

(es,s) r (lv,s’)

eLExp(LW)vValueesLExps(LW)lv Value+

xLId(LW)

eLExp(LW)vValuexLId(LW)

fLId(LW) esLExps(LW)lv Value+

Alcuni controlli si possono omettere in quanto derivano dalla grammatica CF

Altri esprimono proprio il fatto che stiamo dando una semantica a grandi passi

Dichiarazioni di variabili

[d ds (r,s) ] = (r”,s”)

[d] (r,s) = (r’,s’) [ds] (r’,s’) = (r”,s”)

[t x](r,s) = (r[l/x],s[/l])Nuova(l,r,s)

[t x = e](r,s) = (r[l/x],s’[v/l])

[e](r,s) = (v ,s’) Nuova(l,r,s’)

Denotazionale SOS a grandi passi

(t x,r,s) (, r[l/x],s[/l])Nuova(l,r,s)xLId(LW)tLType(LW)

(t x = e,r,s) (, r[l/x],s’[v/l])

(e,s) r (v,s’)Nuova(l,r,s’)eLExp(LW) xLId(LW)tLType(LW)

(d ds,r,s) (,r”,s”)

(d,r,s) (,r’,s’) (ds,r’,s’) (,r”,s”)dLDec(LW)dsLDecs(LW)

Dichiarazioni di funzioni ricorsive: void

Dove F : [T] States {*} States è definita induttivamente da tutte le regole della semantica più le seguenti due:

F(v,sc) = (*,s’-{l})

[sts] (r[/f,l/x],sc[v/l]) = s’

[f(e)] (r[/f],s1) = (*,s”)

F(u,s’) = (*,s”)[e](r[/f],s1) = (u ,s’)

[void f(T x) {sts}](r,s) = (r[F/f],s) (void f(T x) {sts},r,s) (, r[F/f],s)

F(v,sc) = (*,s’-{l})

(sts, sc[v/l]) r[/f,l/x] (, s’)

(f(e), s1) r[/f] (*,s”)

F(u,s’) = (*,s”)(e, s1) r[/f] (u, s’)

Nuova(l,r,sc)

Dichiarazioni di funzioni ricorsive: BType

Dove F : [T] States [RT] States è definita induttivamente da tutte le regole della semantica più le seguenti due:

[RT f(T x) {sts result e}](r,s) = (r[F/f],s) (RT f(T x) {sts result e},r,s) (, r[F/f],s)

(f(e), s1) r[/f] (a, s”)

F(u,s’) = (a,s”)(e, s1) r[/f] (u, s’)

[f(e)] (r[/f],s1) = (a ,s”)

F(u,s’) = (a ,s”)[e](r[/f],s1) = (u ,s’)

Nuova(l,r,sc)

F(v,sc) = (a,s”-{l})

[sts] (r[/f,l/x],sc[v/l]) = s’ [e](r[/f,l/x], s’)= (a ,s”)

F(v,sc) = (a,s”-{l})

(sts, sc[v/l]) r[/f,l/x] (, s’) (e, s’) r[/f,l/x] (a, s”)Nuova(l,r,sc)

Statements 1

[if (e) {sts} else {sts’}](r,s) = s”

[e](r,s) = (tt ,s’) [sts] (r,s’) = s”

[if (e) {sts} else {sts’}](r,s) = s”

[e](r,s) = (ff ,s’) [sts’] (r,s’) = s”

[st sts ] (r,s) =

[st] (r,s) = s’ [sts] (r,s’) = s”

s”

[e](r,s) = (v ,s’)

[e;](r,s) = s’

(if (e) {sts} else {sts’}, s) r (, s”)

(e, s) r (true, s’) (sts, s’) r (, s”)

(if (e) {sts} else {sts’}, s) r (, s”)

(e, s) r (false, s’) (sts’, s’) r (, s”)

(st sts, s) r (, s”)

(st, s) r (, s’) (sts, s’) r (, s”)

(e, s) r (v, s’)

(e;, s) r (, s’)

stLStat(LW) stsLstats(LW)

eLExp(LW)

Statements 2: while

[while (e) {sts}](r,s) = s0

[e](r,s) = (tt ,s’) [sts] (r,s’) = s” [while (e) {sts}](r,s”) = s0

[while (e) {sts}](r,s) =

[e](r,s) = (ff ,s’)

s’ (while (e) {sts}, s) r (, s’)

(e, s) r (false, s’)

(while (e) {sts}, s) r (, s0)

(e, s) r (true, s’) (sts, s’) r (, s”) (while (e) {sts}, s”) r (, s0)

Problema dei valoriConsideriamo la semantica dell’espressione 3 + 2.Per valutarne la semantica possiamo solo usare la regola della somma

(3+2,s) r (5,s”)

(3,s) r (v,s’) (2,s’) r (v’,s”)v + v’ =5

Non ci sono regole per completare alberi di questa forma.

In realtà in tutte le regole (che ce l’hanno) la valutazione di un’espressione dovrebbe essere opzionale, perché se l’espressione è già un valore non va ulteriormente elaborata.

Quindi, ad esempio, ci vorranno regole tipo

______?____?____?______ ______?____?____?______

(while (false) {sts}, s) r (, s)

(v;, s) r (, s)

(e+v’,s) r (a,s’)

(e,s) r (v,s’)v + v’ =a

(v+e’,s) r (a,s’)

(e’,s) r (v’,s’)v + v’ =a

(v+v’,s) r (a,s)v + v’ =a

(t x = v,r,s) (r[l/x],s[v/l])

Nuova(l,r,s’)eLExp(LW) xLId(LW)tLType(LW)

Le due semantiche coincidono, fatti i dovuti aggiustamenti tecnici, cioè adeguate le due notazioni:

Relazione con la semantica denotazionale

[d]Decs(r,s)=(r’,s’) se e solo se (d,r,s) (, r’, s’)

[st]Stats (r,s)=s’ se e solo se (st,s) r (, s’)

[e]Exps(r,s)=(v,s’) se e solo se (e,s) r (v, s’)

e modulo una traduzione fra i valori (usati nella semantica denotazionale) e le loro descrizioni sintattiche (usate nella semantica operazionale)Non sono necessarie prove, o meglio la prova è banale, perché le due semantiche sono descritte da regole “isomorfe” (a volta partizionate in modo diverso, a seconda che le espressioni coinvolte già rappresentino valori)Quindi i due approcci hanno gli stessi limiti.In particolare, non danno informazioni in caso di non terminazione. Questo può essere riduttivo in caso di sistemi che sono progettati in modo non terminante (e.g. sistemi operativi)