Semantica operazioanle
Ciao, sto studiando la semantica operazionale dei linguaggi di programmazione, definita con premessa/conseguenza però non riesco a trovare appunti che utilizzino stati complessi (ambiente, scope statico, scope dinamico).
dove posso cercare?
dove posso cercare?
Risposte
Ciao,
intendi studiata con la classica induzione strutturale e sulle derivazioni?
comunque:
- semantica operazionale strutturale (SOS: Structural Operational Semantic) dispense di Plotkin: post456058.html#p456058
- vari appunti e dispense sulla semantica dei linguaggi: post479143.html#p479143
se avrai dubbi su questi argomenti posta pure qua sul forum, è un argomento molto affascinate
PS: studi scienze informatiche per curiosità?
premessa/conseguenza
intendi studiata con la classica induzione strutturale e sulle derivazioni?
comunque:
- semantica operazionale strutturale (SOS: Structural Operational Semantic) dispense di Plotkin: post456058.html#p456058
- vari appunti e dispense sulla semantica dei linguaggi: post479143.html#p479143
se avrai dubbi su questi argomenti posta pure qua sul forum, è un argomento molto affascinate
PS: studi scienze informatiche per curiosità?
Allora provo a riassumere, per Semantica Operazionale si intende la formalizzazione della semantica di un linguaggio (quindi del suo interprete).
È costituita da: Stato (descrizione complessiva del sistema), Transizione ( passo della computazione che modifica lo stato e/o programma), Computazione(sequenza di transizioni).
Possiamo definirla in modo Formale o con la Semantica Operazionale Strutturata.
Inoltre abbiamo due approcci diversi, uno per linguaggi puramente imperativi dove specifichiamo lo Stato quindi Ambiente, Memoria, Heap ecc; oppure per linguaggi funzionali dove descriviamo solo l'ambiente.
Caso Imperativo: $$$->$$sigma'$
Caso Funzionale: $$$->$$v$
Alcune regole:
In questo caso l'ambiente è rappresentato in modo semplicistico potremmo aggiungere assegnamento (PREMESSA:$$$->$$n$ CONSEGUENZA: $$$->$$sigma[n-X]$) sequenza, costrutti condizionali, cicli ecc ecc
Però non riesco a trovare come viene gestito lo scope.
Comunque, si studio Informatica.
È costituita da: Stato (descrizione complessiva del sistema), Transizione ( passo della computazione che modifica lo stato e/o programma), Computazione(sequenza di transizioni).
Possiamo definirla in modo Formale o con la Semantica Operazionale Strutturata.
Inoltre abbiamo due approcci diversi, uno per linguaggi puramente imperativi dove specifichiamo lo Stato quindi Ambiente, Memoria, Heap ecc; oppure per linguaggi funzionali dove descriviamo solo l'ambiente.
Caso Imperativo: $
Caso Funzionale: $
Alcune regole:
In questo caso l'ambiente è rappresentato in modo semplicistico potremmo aggiungere assegnamento (PREMESSA:$
Però non riesco a trovare come viene gestito lo scope.
Comunque, si studio Informatica.
quella che mostri è una semantica dinamica (perciò basata sull'induzione sulle derivazioni delle regole).
Mancherebbe una semantica statica, cioè induzione sui tipi.
Comunque a te interessa la semantica dinamica delle procedure in caso di IMP (transizioni tra stati e memorie) e semantica delle funzioni in caso di FUN (transizioni tra ambienti)? e in questi casi lo scoping statico (valutazione a tempo di compilazione) e lo scoping dinamico (valutazione a tempo di esecuzione)?
attento che il significato di "scope" può variare e di molto a seconda del contesto.
Se non è il caso sopra, "scope" lo intendi come l'ambiente attuale, cioè l'insieme degli identificatori legati (bound) e liberi (free)?
In quelle regole che mostri manca l'ambiente cioè che identificatori sono attualmente legati ad una cella di memoria.
Di solito (Plotkin usava questa notazione) si utilizza $\rho$ per annotare l'ambiente attuale.
Ad esempio se tipo dopo quache riga di codice valutata incontriamo un'assegnamento con un identificatore $x$, avremo un insieme \(\rho=\{[x=l_1]\}\) con annotato un identificatore valutato con la corrispondente locazione di memoria \(\sigma=\{[l_1=\bot]\}\) (in IMP in questo caso) in FUN è costruito diversamente.
in simboli nell'induzione si avrà una scrittura di questo genere (siamo nei comandi):
\(\rho_x\ \vdash\ .....\)
____________________
\(\rho_x\ \vdash\\ \longrightarrow\ \sigma'\)
dove \(\rho_x=\{[x=l_1]\}\) e \(\sigma=\{[l_1=\bot]\}\)
Dimmi cosa intendi e vediamo
Mancherebbe una semantica statica, cioè induzione sui tipi.
Comunque a te interessa la semantica dinamica delle procedure in caso di IMP (transizioni tra stati e memorie) e semantica delle funzioni in caso di FUN (transizioni tra ambienti)? e in questi casi lo scoping statico (valutazione a tempo di compilazione) e lo scoping dinamico (valutazione a tempo di esecuzione)?
attento che il significato di "scope" può variare e di molto a seconda del contesto.
Se non è il caso sopra, "scope" lo intendi come l'ambiente attuale, cioè l'insieme degli identificatori legati (bound) e liberi (free)?
In quelle regole che mostri manca l'ambiente cioè che identificatori sono attualmente legati ad una cella di memoria.
Di solito (Plotkin usava questa notazione) si utilizza $\rho$ per annotare l'ambiente attuale.
Ad esempio se tipo dopo quache riga di codice valutata incontriamo un'assegnamento con un identificatore $x$, avremo un insieme \(\rho=\{[x=l_1]\}\) con annotato un identificatore valutato con la corrispondente locazione di memoria \(\sigma=\{[l_1=\bot]\}\) (in IMP in questo caso) in FUN è costruito diversamente.
in simboli nell'induzione si avrà una scrittura di questo genere (siamo nei comandi):
\(\rho_x\ \vdash\ .....\)
____________________
\(\rho_x\ \vdash\
dove \(\rho_x=\{[x=l_1]\}\) e \(\sigma=\{[l_1=\bot]\}\)
Dimmi cosa intendi e vediamo
Allora definiamo aritmetiche e booleane così:
a ::= n|X|più($a_0,a_1$)|per($a_0,a_1$)|meno($a_0,a_1$)
b ::= true|false|or($b_0,b_1$)|and($b_0,b_1$)|not($b_0$)|uguale($a_0,a_1$)|minore($a_0,a_1$)
Per ora mi interessa la semantica del linguaggio funzionale, definiamo uno scope statico:
Scope Statico: Ci sono due ambienti uno locale, (cioè il blocco in cui ci troviamo + l'ambiente globale) e uno non locale, cioè tutti i blocchi esterni.
Abbiamo due tipi di dichiarazioni: Variabili, funzioni.
1)Quando troviamo una dichiarazione di Variabile o funzione, controlliamo se è presente nell'ambiente non globale, se non è presente la aggiungiamo all'ambiente; se la variabile o la funzione è presente nell'ambiente non locale, dobbiamo disattivare il binding precedente e inserirla.
2)quando lasciamo il blocco quindi chiudiamo quel preciso ambiente locale, leviamo il "frame" dalla pila degli ambienti e tutti i binding vengono persi e devono essere esplicitamente distrutti.
3)Nel momento in cui chiudiamo un ambiente locale e ritorniamo in un ambiente precedentemente visitato dobbiamo riattivare tutti i binding che avevamo disattivato prima.
Credo ci sia tutto per implementare lo scope statico.
a ::= n|X|più($a_0,a_1$)|per($a_0,a_1$)|meno($a_0,a_1$)
b ::= true|false|or($b_0,b_1$)|and($b_0,b_1$)|not($b_0$)|uguale($a_0,a_1$)|minore($a_0,a_1$)
Per ora mi interessa la semantica del linguaggio funzionale, definiamo uno scope statico:
Scope Statico: Ci sono due ambienti uno locale, (cioè il blocco in cui ci troviamo + l'ambiente globale) e uno non locale, cioè tutti i blocchi esterni.
Abbiamo due tipi di dichiarazioni: Variabili, funzioni.
1)Quando troviamo una dichiarazione di Variabile o funzione, controlliamo se è presente nell'ambiente non globale, se non è presente la aggiungiamo all'ambiente; se la variabile o la funzione è presente nell'ambiente non locale, dobbiamo disattivare il binding precedente e inserirla.
2)quando lasciamo il blocco quindi chiudiamo quel preciso ambiente locale, leviamo il "frame" dalla pila degli ambienti e tutti i binding vengono persi e devono essere esplicitamente distrutti.
3)Nel momento in cui chiudiamo un ambiente locale e ritorniamo in un ambiente precedentemente visitato dobbiamo riattivare tutti i binding che avevamo disattivato prima.
Credo ci sia tutto per implementare lo scope statico.
ok ho capito cosa devi fare, ma lo scoping (scoping statico e dinamico) è sensato definirlo SOLO nella semantica delle funzioni (function) di FUN, nel resto delle regole non c'è questa differenza perchè il codice è una sequenza di istruzioni (definizioni).
Quello che chiami "scope" è l'ambiente di valutazione, cioè quello nella semantica operazionale standard (quella di Plotkin) viene definito come ambiente dinamico $\rho$ invece nella tua semantica definisci come $\delta$ ($ -> n$).
definisimi anche "scope dinamico" come lo intendi te.
Quello che vuoi definire comunque si può intendere come la composizionalità delle regole e la strutturazione a stack degli ambienti.
Se le tue regole lo permettono, puoi definire una cosa tipo:
x : int = 2
y : int = 3
x : int = 1
x + y
l'ambiente sarà valutato in ordine di inserimento: $\delta = \{[x=2],[y=3],[x=1]\}$
x+y = 1+3 = 4
un esempio invece di differenza di scoping e SOLO qua si può parlarne:
x : int = 2
function f(y:int) : int = x+y
___
x : int = 1
f(3)
scoping statico (valutazione sul codice):
$\delta = \{[x=2],[\lambda(y:\text{int});[x=2].x+y],[x=1]\}$
x+y = 2+3 = 5
ovviamente a diversi step l'ambiente elimina le variabili non necessarie. Se vedi l'ambiente si porta dietre le informazioni delle variabili al momento della sua dichiarazione.
scoping dinamico (valutazione a tempo di chiamata):
$\delta = \{[x=2],[\lambda(y : \text{int}).x+y],[x=1]\}$
qua invece non si porta dietro nessuna informazione, le variabili del corpo della funzione saranno valutate alla chiamata
x+y = 1+3 = 4
questi sono esempi, ma per fare tutto ciò servono regole ben definite.
Te cosa devi fare, le devi definire o ne vuoi già strutturare per studiarle? non me lo hai ancora detto.
Quello che chiami "scope" è l'ambiente di valutazione, cioè quello nella semantica operazionale standard (quella di Plotkin) viene definito come ambiente dinamico $\rho$ invece nella tua semantica definisci come $\delta$ ($
definisimi anche "scope dinamico" come lo intendi te.
Quello che vuoi definire comunque si può intendere come la composizionalità delle regole e la strutturazione a stack degli ambienti.
Se le tue regole lo permettono, puoi definire una cosa tipo:
x : int = 2
y : int = 3
x : int = 1
x + y
l'ambiente sarà valutato in ordine di inserimento: $\delta = \{[x=2],[y=3],[x=1]\}$
x+y = 1+3 = 4
un esempio invece di differenza di scoping e SOLO qua si può parlarne:
x : int = 2
function f(y:int) : int = x+y
___
x : int = 1
f(3)
scoping statico (valutazione sul codice):
$\delta = \{[x=2],[\lambda(y:\text{int});[x=2].x+y],[x=1]\}$
x+y = 2+3 = 5
ovviamente a diversi step l'ambiente elimina le variabili non necessarie. Se vedi l'ambiente si porta dietre le informazioni delle variabili al momento della sua dichiarazione.
scoping dinamico (valutazione a tempo di chiamata):
$\delta = \{[x=2],[\lambda(y : \text{int}).x+y],[x=1]\}$
qua invece non si porta dietro nessuna informazione, le variabili del corpo della funzione saranno valutate alla chiamata
x+y = 1+3 = 4
questi sono esempi, ma per fare tutto ciò servono regole ben definite.
Te cosa devi fare, le devi definire o ne vuoi già strutturare per studiarle? non me lo hai ancora detto.
No no devo definirle, cioè l'intento e di avere l'interprete completo, per ora ho regole per : valutazione delle espressioni e booleani, operazioni su valori/espressioni, costrutti condizionali, cicli, assegnamento.
Ma le implemento in modo semplicistico, cioè senza tenere conto dello scope, quello che mi serve è istanziare queste regole di scoping per poter aumentare la "complessità" del linguaggio compreso dall'interprete.
Ma le implemento in modo semplicistico, cioè senza tenere conto dello scope, quello che mi serve è istanziare queste regole di scoping per poter aumentare la "complessità" del linguaggio compreso dall'interprete.
"BHK":
No no devo definirle, cioè l'intento e di avere l'interprete completo, per ora ho regole per : valutazione delle espressioni e booleani, operazioni su valori/espressioni, costrutti condizionali, cicli, assegnamento.
Ma le implemento in modo semplicistico, cioè senza tenere conto dello scope, quello che mi serve è istanziare queste regole di scoping per poter aumentare la "complessità" del linguaggio compreso dall'interprete.
mi faresti vedere le regole del ciclo (che penso tu abbia definito solo in IMP, spero). Lo hai costruito basandoti sulla definizione di punto fisso (la più semplice delle semantiche) o su cosa?
Gli unici casi che puoi parlare di "scoping" al di fuori della semantica delle procedure/funzioni è nella semantica dei comandi tipo il costrutto condizionale (o il ciclo while, ma bisogna stare parecchio attenti a definirlo bene), o anche il costrutto di blocco (quello che in FUN è di solito let d into e) ma bisogna aver costruito la semantica delle dichiarazioni in modo appropriato.
Ma voglio che tu comprenda che la definzione di scoping è valida nella semantica delle procedure/funzioni, cioè la separazione di blocchi astratti di codice (se fossi in multi-thread in "main" differenti). Il resto è uno scoping forzato, con delle restrizioni (tipo non hai la dichiarazione, ma solo l'assegnamento ad una variabile).
Allora si, ho fatto un po di confusione, assegnazione, sequenza, costrutti condizionali, cicli sono definiti solo per un linguaggio imperativo. es while
Ora lasciando stare i costrutti per i linguaggi imperativi, mi serve definire le regole di scope statico per la semantica del linguaggio funzionale, sono state formalizzate? dove posso trovarne di sempre valide?
Ora lasciando stare i costrutti per i linguaggi imperativi, mi serve definire le regole di scope statico per la semantica del linguaggio funzionale, sono state formalizzate? dove posso trovarne di sempre valide?
vedi le dispense di Plotkin, pag 65 c'è la definizione di ambiente statico/dinamico e le sue regole.
Ma l'implementazione è tutt'altra storia. Questo NON è lo scoping dove ci deve essere una strutturazione a blocchi dove la tua semantica non prevede, cioè separazioni logiche del codice, ma è un'idea di ambiente locale e globale (formulazione a stack).
(il ciclio while, sì te valuti subito il comando $c$, io ho ancora visto che si valuta in step successivi, ma va bene).
PS: due cose, che libro stai usando e dove hai preso questo regole semantiche, per curiosità?
EDIT:
ovviamente se vuoi che abbia senso ciò che stai creando devi ampliare la tua semantica di un nuovo costrutto di "blocco". Se no è inutile parlare di tutto ciò
Es. lo scoping nel costrutto condizionale:
questo è possibile farlo e si può parlere di scoping, ma ssse la tua semanca prevede la dichiarazione nei rami dell'if. Spero ti sia chiaro ciò che stai cercando di fare, se no ne discutiamo
Ma l'implementazione è tutt'altra storia. Questo NON è lo scoping dove ci deve essere una strutturazione a blocchi dove la tua semantica non prevede, cioè separazioni logiche del codice, ma è un'idea di ambiente locale e globale (formulazione a stack).
(il ciclio while, sì te valuti subito il comando $c$, io ho ancora visto che si valuta in step successivi, ma va bene).
PS: due cose, che libro stai usando e dove hai preso questo regole semantiche, per curiosità?
EDIT:
ovviamente se vuoi che abbia senso ciò che stai creando devi ampliare la tua semantica di un nuovo costrutto di "blocco". Se no è inutile parlare di tutto ciò
Es. lo scoping nel costrutto condizionale:
if true then x: int = 3
questo è possibile farlo e si può parlere di scoping, ma ssse la tua semanca prevede la dichiarazione nei rami dell'if. Spero ti sia chiaro ciò che stai cercando di fare, se no ne discutiamo
Allora ho trovato come si può implementare lo scope statico, inanzi tutto facciamo una distinzione fra ambiente locale $delta_l$ e non locale $delta_(nl)$, questo è un esempio:
Ciao,
una cosa non mi hai ancora detto il costrutto di blocco lo hai nella tua semantica? Lo inserirai?
quello che viene scrito come
scusa se insisto, ma definire gli ambienti, le regole, senza inserire il costrutto di blocco non serve a nulla. Il tuo linguaggio è puramente imperativo e gli ambienti non servono a nulla basta la memoria (gli stati), se aggiungi solo il blocco (senza procedure) puoi parlare di linguaggio applicativo, di scope ed ambienti.
una cosa non mi hai ancora detto il costrutto di blocco lo hai nella tua semantica? Lo inserirai?
quello che viene scrito come
let d into eoppure
dic;com
scusa se insisto, ma definire gli ambienti, le regole, senza inserire il costrutto di blocco non serve a nulla. Il tuo linguaggio è puramente imperativo e gli ambienti non servono a nulla basta la memoria (gli stati), se aggiungi solo il blocco (senza procedure) puoi parlare di linguaggio applicativo, di scope ed ambienti.
Accedi a tutti gli appunti
Tutor AI: studia meglio e in meno tempo