Semantica operazionale deilinguaggi di Programmazione
Sistemi di transizioni (1)
Rosario Culmone, Luca Tesei
Lucidi tratti dalla dispensa
“Elementi di Semantica Operazionale”
R. Barbuti, P. Mancarella e F. Turini
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.1/78
Introduzione
Presenteremo una tecnica per definire in manieraformale la semantica di un linguaggio diprogrammazione
Formalismo: sistemi di transizioni basati sugli alberi diderivazione dei programmi
Linguaggio di riferimento: una versione semplificata diJava
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.2/78
Semantica di un linguaggio formale
È il significato attribuito ad ogni stringa
Le stringhe di un linguaggio di per sé non hanno unparticolare significato
L’attribuzione del significato è un passo successivo eindipendente dalla definizione del linguaggio
Ad uno stesso linguaggio possono essere attribuite piùsemantiche
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.3/78
Come attribuire la semantica
La scelta del metodo è fondamentale:
“A parole”, con una prosa, informalmente
Semiformalmente utilizzando la prosa con l’aiuto dialcuni strumenti formali
In maniera rigorosa e formale, basandosi su unacaratterizzazione formale della sintassi
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.4/78
Linguaggi di programmazione
Attualmente la caratterizzazione sintattica dei linguaggidi programmazione è quasi sempre formale(Grammatica)
Su questa base si poggerebbe in maniera naturale unadefinizione rigorosa della semantica
Nei manuali invece la semantica risulta sempre definitain maniera informale
Ciò a scapito della chiarezza, della precisione delladefinizione e della possibilità di ragionarematematicamente sulla correttezza dei programmi
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.5/78
Strumenti
In questa parte descriveremo un modo percaratterizzare formalmente la semantica di un certolinguaggio
Lo strumento che useremo sono i Sistemi di Transizioni
Obiettivo finale: dare un sistema di transizioni in gradodi legare ogni programma ben formato di un linguaggioJava semplificato ad un significato preciso
Il significato sarà un certo elemento di un dominiosemantico definito formalmente
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.6/78
Sistemi di transizioni
Sono oggetti matematici molto versatili
Possono modellare il concetto di calcolo
Possono rappresentare sistemi di dimostrazione
Possono modellare processi, ambienti, sistemicomplessi
Permettono di dare la semantica operazionale di unlinguaggio di programmazione
...
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.7/78
Sistemi di transizioni
Possiamo per il momento considerarli come “automievoluti”
Esprimono una sequenza di azioni che portano ad unrisultato
Le azioni sono chiamate transizioni
Ogni passo ha una configurazione (stato) di partenza euna di arrivo
Le configurazioni (stati) possono essere infinite
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.8/78
Un primo approccio
Vediamo un semplice sistema di transizioni che modellail calcolo di una somma semplice
Il sistema, date due cifre e un riporto, deve calcolare laloro somma come cifra risultato e relativo riporto
Ad esempio: 3 + 5, 0 = 8, 0 (si legge “3 + 5 con riporto di0 è uguale a 8 con riporto di 0”)
Ad esempio: 8 + 7, 1 = 6, 1 (si legge “8 + 7 con riporto di1 è uguale a 6 con riporto di 1”)
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.9/78
Modello del calcolo
Possiamo pensare a questo calcolo come a unatransizione da una configurazione ad un’altra
Ad esempio 3 + 5, 0 è una configurazione da cuipossiamo fare un passo di calcolo e arrivare nellaconfigurazione 8, 0
Nella configurazione 8, 0 non possiamo fare nessunulteriore calcolo
Una configurazione del genere è detta terminale
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.10/78
Modello del calcolo
Rappresentiamo le configurazioni in questo modo:〈3, 5, 0〉 sta per 3 + 5, 0
〈8, 0〉 sta per 8, 0
Configurazioni del tipo 〈10, 0〉 o 〈3, 5, 2〉 non sonocontemplate perché non è possibile nel calcolo chestiamo modellando
Da una configurazione contemplata che non èterminale è possibile fare, in generale, zero o piu passi dicalcolo (il sistema può essere non deterministico)
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.11/78
Passi di transizione
Un passo di calcolo è modellato come un’associazionetra una configurazione e un’altra
Si scrive così: 〈3, 7, 1〉 → 〈1, 1〉
Non tutte le configurazioni sono associate!
Ad esempio: 〈3, 7, 1〉 6→ 〈2, 1〉
Se lo fosse il sistema potrebbe fare dei calcoli sbagliati
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.12/78
Passi di transizione
La logica del sistema di transizioni, il suo modo difunzionare, è data da tutte le associazioni
Ogni associazione modella un possibile passo ditransizione
Le associazioni, in generale, possono essere infinite
Nel nostro esempio sono un numero finito
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.13/78
Formalizziamo
Un sistema di transizioni S è una tripla 〈Γ, T,→〉
Γ è l’insieme delle configurazioni
T ⊆ Γ è un sottoinsieme di Γ contenente leconfigurazioni terminali
→ è un insieme di coppie 〈γ, γ′〉 di configurazioni eviene detta relazione di transizione
L’appartenenza della coppia 〈γ, γ′〉 alla relazione →si indica così: γ → γ′
Tali coppie sono chiamate transizioni
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.14/78
Definizione delle configurazioni
In genere le configurazioni sono tuple (sequenze dielementi delimitate da 〈 e 〉)
Ogni elemento della tupla è un oggetto definitomatematicamente
Ad esempio: insieme, funzione, relazione, elemento diun insieme, stringa, simbolo di alfabeto, . . .
Nei sistemi che definiremo per dare la semanticaoperazionale dei linguaggi di programmazione glielementi saranno spesso alberi di derivazione o alberisintattici
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.15/78
Convenzione
In questa prima parte sui sistemi di transizioniadotteremo la seguente convenzione:
Se S è un simbolo non terminale di una certagrammatica data
allora l’espressione x ∈ S indica che x è una stringaassociata ad un albero di derivazione la cui radice è S
Nel seguito vedremo invece che x sarà spesso unalbero sintattico astratto la cui radice è S
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.16/78
Nell’esempio
Consideriamo questa semplice grammatica:
Cif ::= 0 | 1 | 2 | ... | 9
Definiamo formalmente il sistema dell’esempio
Diamo un nome al sistema e alle sue componenti:Scr = 〈Γcr , Tcr ,→cr 〉
Γcr è l’insieme di tutte le configurazioni possibili
Tcr è l’insieme delle configurazioni terminali
→cr è l’insieme delle associazioni (transizioni) cheesprimono i calcoli possibili
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.17/78
Configurazioni
Γcr = {〈c, c′, r〉 | r ∈ {0, 1} e c, c′ ∈ Cif} ∪
{〈c, r〉 | r ∈ {0, 1} e c ∈ Cif}
Tcr = {〈c, r〉 | r ∈ {0, 1} e c ∈ Cif}.
Per esprimere tutte le associazioni tra le configurazioniche modellano il calcolo in questo caso semplicepossiamo elencarle:
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.18/78
Transizioni
〈0, 0, 0〉 →cr 〈0, 0〉 〈0, 0, 1〉 →cr 〈1, 0〉
〈0, 1, 0〉 →cr 〈1, 0〉 〈0, 1, 1〉 →cr 〈2, 0〉
〈0, 2, 0〉 →cr 〈2, 0〉 〈0, 2, 1〉 →cr 〈3, 0〉
. . . . . . . . . . . .〈9, 8, 0〉 →cr 〈7, 1〉 〈9, 8, 1〉 →cr 〈8, 1〉
〈9, 9, 0〉 →cr 〈8, 1〉 〈9, 9, 1〉 →cr 〈9, 1〉
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.19/78
Un sistema più complesso
Consideriamo la seguente grammaticaNum ::= Cif | Num CifCif ::= 0 | 1 | 2 | ... | 9
Una qualsiasi stringa n ∈ Num è la rappresentazione diun numero naturale in base dieci
Definiamo un sistema di transizioni cheprese due stringhe n e n’
calcoli una stringa m che rappresenta il numeroottenuto sommando n e n’
Diamo un nome al sistema: Sn+ = 〈Γn+, Tn+,→n+〉
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.20/78
Configurazioni
Sicuramente dobbiamo mettere nel sistema delleconfigurazioni 〈n, n′〉
Rappresentano lo stato in cui il sistema si appresta acalcolare la somma tra n e n′
Potremmo chiamarle configurazioni “iniziali”
Le configurazioni terminali che ci aspettiamo sono irisultati, cioè rappresentazioni (m) di un numeronaturale che sarà la somma
Sono sufficienti?
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.21/78
Strategia
Prima di poter rispondere a questa domanda dobbiamodecidere in quale modo fare operare il sistema perottenere quello che vogliamo
Nel sistema precedente il calcolo poteva essere fattocon un solo passo di transizione
Un sistema di transizioni in generale può operarefacendo diversi passi di transizione in sequenza
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.22/78
Funzionamento di un sistema
È elementare:
In ogni momento il sistema si trova o viene posto in unadelle sue possibili configurazioni, diciamo γ
Il suo compito consiste nel fare un passo di derivazione,se possibile
Il sistema determina se c’è una configurazione γ′
associata con γ: cioè vale γ → γ′
Se esiste una (o più) γ′ di questo tipo allora il sistemacompie il passo di derivazione e si porta in γ′ (unaqualsiasi delle possibili, se più di una)
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.23/78
Funzionamento del sistema
La configurazione γ′ diventa la configurazione correntee il sistema si ritrova nella situazione iniziale in cui devecercare di fare un altro passo di derivazione
Continuando questo processo si possono verificare tresituazioni:
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.24/78
Funzionamento del sistema
1. Il sistema raggiunge una configurazione terminale(dalle quali in genere non è possibile nessun passo diderivazione) e conclude quindi il suo compito
2. Il sistema raggiunge una configurazione non terminaledalla quale non è possibile nessun passo diderivazione. In questo caso la configurazione si dicebloccata . Il sistema ha fallito nel portare a termine il suocompito
3. Il sistema continua a fare passi di derivazione all’infinito.Anche in questo caso consideriamo il compito fallito
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.25/78
Formalizziamo
Dato un sistema di transizioni S = 〈Γ, T,→〉
Una derivazione in S è una sequenza (eventualmenteinfinita) di configurazioni γ0, γ1, . . . , γi−1, γi, . . . tale cheper ogni k ≥ 1 γk−1 → γk
Una derivazione in S è indicata con γ0 → γ1 → . . . → γi
Indicheremo con γ∗
→ γ′ l’esistenza di una derivazioneγ0 → γ1 → . . . → γi in cui γ0 = γ e γi = γ′
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.26/78
Strategia
Una strategia per risovere il problema della somma dinumeri naturali si basa sul concetto di derivazione
L’idea è di svolgere il calcolo per fasi successiveseguendo il semplice algoritmo delle addizioni incolonna che abbiamo imparato alle scuole elementari
Facciamo un esempio. Supponiamo di voler sommare54 e 38. Lo stadio iniziale del calcolo lo possiamorappresentare così:
5438
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.27/78
Strategia
Il calcolo procede effettuando una somma semplice tradue cifre e calcolando un riporto:
15438----2
poiché 4+8=2 con riporto 1
Il calcolo ha prodotto un risultato parziale, 2, ed unriporto, 1
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.28/78
Modelliamo
Possiamo pensare di rappresentare lo stadio iniziale delcalcolo, nel sistema di transizioni, con la configurazione〈54, 38〉
Il primo passo di calcolo che abbiamo fatto può esseremodellato con una transizione da 〈54, 38〉 ad unaconfigurazione intermedia di questo tipo:〈5, 3, 2, 1〉
5 e 3 rappresentano i numeri ancora da sommare, 2 ilrisultato intermedio e 1 il riporto
A questo punto il sistema si trova in questaconfigurazione e deve continuare con un altro passo diderivazione
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.29/78
Strategia
Procedendo nell’algoritmo di somma in colonna siottiene:
05438----92
poiché 5+3+1=9 con riporto 0
A questa situazione corrisponde, nel sistema, latransizione da 〈5, 3, 2, 1〉 a 〈0, 0, 92, 0〉
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.30/78
Strategia
Non essendoci più cifre da sommare, il risultato è 92
A questa situazione corrisponde, nel sistema, latransizione da 〈0, 0, 92, 0〉 a 92
Il sistema, in questo caso, ha quindi eseguito laseguente derivazione:〈54, 38〉 →n+ 〈5, 3, 2, 1〉 →n+ 〈0, 0, 92, 0〉 →n+ 92
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.31/78
Configurazioni
Se vogliamo che il sistema usi questa strategia percalcolare il risultato dobbiamo definire le relativeconfigurazioni possibili:
Γn+ = {〈n, n′〉 | n, n′ ∈ Num} ∪
{〈n, n′, m, r〉 | r ∈ {0, 1} e n, n′, m ∈ Num} ∪
{n | n ∈ Num}
Tn+ = {n | n ∈ Num}
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.32/78
Attenzione
In questo sistema abbiamo un numero infinito diconfigurazioni possibili
In questo sistema abbiamo un numero infinito diassociazioni fra configurazioni da definire affinché ilcalcolo che abbiamo visto possa avvenire fra duenumeri qualsiasi
Come fare per definire →n+, che è infinita, usando unadescrizione finita?
Ci vengono in aiuto le regole condizionali
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.33/78
Regole condizionali
Sono regole scritte in questa forma:
π1 π2 . . . πn
γ → γ′
π1, π2 . . . πn sono formule dette precondizioni o premessedella regola
γ → γ′ è la conclusione della regola
La transizione indicata nella conclusione può esserefatta solo se tutte le premesse πi sono verificate
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.34/78
Regole condizionali
In generale una regola contiene, sia nelle premesseche nella conclusione, variabili che possono assumerevalori in un certo dominio del discorso definito a priori
In realtà quindi una regola rappresenta un insieme,spesso infinito, di regole che si ottengono sostituendoopportunamente le variabili della regola
Formalmente dovremmo quindi parlare di schemi diregole
Che tipo di formule possono essere le premesse?
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.35/78
Premesse
Nel seguito saranno di un tipo tra questi:
un’uguaglianza del tipo x = t, dove x è una variabile e tè una espressione (termine) costruita a partire dacostanti, variabili e operatori elementari
un predicato del tipo t rel t′, dove t, t′ sono termini e relè un operatore di relazione elementare
una transizione del tipo δ → δ′, dove δ, δ′ sonoconfigurazioni e → è la relazione di transizione di unsistema di transizioni (può anche essere il sistema chesi sta definendo, che sarà quindi ricorsivo)
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.36/78
Lettura delle regole
Le regole possono essere lette in maniera logica odichiarativa: la conclusione è vera se e solo se tutte lepremesse sono vere
Esiste però anche un tipo di lettura operazionale
Noi scriveremo sempre regole che possono avere unacorretta lettura operazionale
Illustriamo questo modo di procedere scrivendo leregole per il sistema Sn+
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.37/78
Scrittura di una regola
In generale dobbiamo scrivere un insieme di regole inmodo da coprire tutte le possibili configurazioni nonterminali
In questo modo definiamo cosa fa il sistema in ognipossibile configurazione in cui si può trovare
Naturalmente alcune configurazioni potranno esserecomunque bloccate se non soddisfano le premessedelle regole
Ogni regola gestirà un insieme di configurazioni,mediante l’uso di variabili
La configurazione γ prima della freccia nellaconclusione della regola è il punto di inizio dellascrittura
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.38/78
Le regole diSn+
Partiamo con il considerare le configurazioni “iniziali”{〈n, n′〉 | n, n′ ∈ Num}
Ci aiuteremo sempre con la definizione della relativagrammatica se nelle configurazioni ci sono stringhe
Questo modo di scrivere le regole si chiama guidatodalla sintassi
Il caso più semplice di un Num è il caso base dellagrammatica Cif
Consideriamo quindi il caso più semplice di una coppiadi Num: {〈c, c′〉 | c, c′ ∈ Cif}
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.39/78
Le regole diSn+
c ∈ Cif, c′ ∈ Cif, ?
〈c, c′〉 →n+ ?
Per evitare di inserire sempre le premesse del tipo c ∈ Ciffissiamo delle metavariabili:
c, c′, c′′, . . . stanno per generiche cifre decimali, ovveroelementi della categoria sintattica Cif
r, r′, r′′, . . . stanno per elementi dell’insieme {0,1}, iriporti derivanti dalla somma tra due cifre
n, n′, m, . . . stanno per generici numeri decimali, ovveroelementi della categoria sintattica Num
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.40/78
Le regole diSn+
πi?
〈c, c′〉 →n+ γ′?
Chiamiamo questa regola (i). A questo stadio la letturaoperazionale è la seguente:
se il sistema Sn+ si trova in una configurazione che famatch con 〈c,c′〉allora
se si possono rendere vere tutte le premesse πi
allora il sistema può effettuare un passo ditransizione verso la configurazione γ′
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.41/78
Lettura operazionale: copertura
Le variabili c e c’ possono essere viste come deiparametri di input
Attraverso il pattern matching con la configurazioneattuale del sistema, quando la regola verrà usata, esseassumeranno un certo valore
Questi valori, tramite il nome delle variabili, possonoessere usati nelle premesse per effettuare calcoli etrovare dei valori intermedi legati a nuove variabili
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.42/78
Lettura operazionale: copertura
La struttura della configurazione di arrivo γ′ (l’“output”)potrà essere specificata solamente tramite:
costanti
le variabili di “input” in γ
le variabili inserite nelle premesse per il calcolo deivalori intermedi
combinazione di queste con operatori noti
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.43/78
Le regole diSn+
〈c, c′, 0〉 →cr 〈c′′, r〉
〈c, c′〉 →n+ γ′?
Ad esempio rappresenta il seguente calcolo intermedio:0 14 ---> 48 8---- ------
2con c = 5, c′ = 5, c′′ = 1, r = 1
Siccome siamo all’inizio del calcolo poniamo il riporto iniziale
uguale a 0
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.44/78
Le regole diSn+
〈c, c′, 0〉 →cr 〈c′′, r〉
〈c, c′〉 →n+ γ′?
La premessa è una transizione del sistema Scr
La configurazione di partenza della transizione ècostruita con i valori delle variabili di “input”, cheavranno un valore definito quando la regola verràapplicata
La configurazione di arrivo contiene le nuove variabilic′′e r
Il loro valore dipende dal comportamento di Scr
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.45/78
Transizioni nelle premesse
Se una premessa è una transizione di un sistema ditransizioni (anche lo stesso):
La configurazione di partenza deve esserecompletamente specificata con costantim variabili di“input”, o comunque variabili “coperte”, e applicazioni dioperatori noti a queste
La premessa è soddisfatta se il sistema richiamato (siindividua dal nome della freccia), posto nellaconfigurazione specificata può effettuare unatransizione
Nella lettura operazionale il processo può essere vistocome una chiamata di funzione/procedura dell’altrosistema (ricorsiva se è lo stesso)
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.46/78
Transizioni nelle premesse
Se il sistema interpellato può effettuare la transizioneallora le nuove variabili nella configurazione di arrivoassumeranno un valore e risulteranno “coperte”
Le variabili coperte possono giocare lo stesso ruolodelle variabili di “input”
Nel caso non ricorsivo c’è una relazione gerarchica fra ilsistema chiamante e quello chiamato
Il sistema chiamato nelle premesse viene dettosottosistema
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.47/78
Le regole diSn+
〈c, c′, 0〉 →cr 〈c′′, r〉
〈c, c′〉 →n+ 〈0, 0, c′′, r〉
Costruiamo la configurazione di arrivo del sistema Sn+:
nei casi corrispondenti alla configurazione di partenzache fa match con 〈c, c′〉
in base ai valori calcolati dal sistema Scr incorrispondenza della relativa configurazione 〈c, c′, 0〉
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.48/78
Le regole diSn+
Abbiamo trattato, con la scrittura di questa regola, 100possibili configurazioni (2 cifre da 0 a 9) “iniziali” delsistema Sn+
Le possibili configurazioni sono infinite!
La prossima regola che scriviamo tratta infiniti casi
Seguendo sempre l’approccio guidato dalla sintassidobbiamo trattare ora il caso in cui il primo numerodella configurazione di Sn+ è del tipo nc, cioè sia unastringa composta da più di una cifra
Corrisponde al caso sintattico Num ::= Num Cif
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.49/78
Le regole diSn+
πi?
〈nc, c′〉 →n+ γ′?
Chiamiamo questa regola (ii). Deve trattare, ad esempio,questo caso:
0 134 ---> 347 07
--- ----1
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.50/78
Le regole diSn+
Basta di nuovo chiamare il sistema Scr per fare un passo dicalcolo elementare e scrivere la configurazione di arrivo diSn+ di conseguenza:
〈c, c′, 0〉 →cr 〈c′′, r〉
〈nc, c′〉 →n+ 〈n, 0, c′′, r〉
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.51/78
Le regole diSn+
Manca il caso sintattico simmetrico al precedente e quelloin cui entrambi i numeri di partenza sono formati da più diuna cifra:
〈c′, c, 0〉 →cr 〈c′′, r〉
〈c′, nc〉 →n+ 〈0, n, c′′, r〉
〈c, c′, 0〉 →cr 〈c′′, r〉
〈nc, n′c′〉 →n+ 〈n, n′, c′′, r〉
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.52/78
Le regole diSn+
Mettendo tutto insieme:〈c, c′, 0〉 →cr 〈c′′, r〉
〈c, c′〉 →n+ 〈0, 0, c′′, r〉
(i)
〈c, c′, 0〉 →cr 〈c′′, r〉
〈nc, c′〉 →n+ 〈n, 0, c′′, r〉
(ii)
〈c′, c, 0〉 →cr 〈c′′, r〉
〈c′, nc〉 →n+ 〈0, n, c′′, r〉
(iii)
〈c, c′, 0〉 →cr 〈c′′, r〉
〈nc, n′c′〉 →n+ 〈n, n′, c′′, r〉
(iv)
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.53/78
Le regole diSn+
Abbiamo trattato tutte le possibili configurazioni “iniziali”di Sn+
La prova sta nel fatto che abbiamo trattato tutti i casisintattici della grammatica
Le stringhe nelle configurazioni sono tutte e sole quellegenerate dalla grammatica
Dobbiamo ora occuparci delle configurazioni intermediedel tipo 〈n, n′, m, r〉
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.54/78
Configurazioni intermedie
Nelle configurazioni intermedie ci troviamo nella stessasituazione di quelle iniziali
Abbiamo due stringhe n e n′ di Num, una terza stringa m
e una cifra di riporto
Le variabili che guidano il calcolo sono sempre n e n′,
mentre m e il resto sono accumulatori di comodo per ivalori intermedi
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.55/78
Le regole diSn+
〈c, c′, r〉 →cr 〈c′′, r′〉
〈c, c′, m, r〉 →n+ 〈0, 0, c′′m, r′〉
Gestisce il calcolo intermedio in cui sono rimaste due cifreda sommare:r r’0c ---> 00c’ 0----- -------m c’’m
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.56/78
Le regole diSn+
Gli altri casi sintattici si ripetono in maniera analoga:
〈c, c′, r〉 →cr 〈c′′, r′〉
〈nc, c′, m, r〉 →n+ 〈n, 0, c′′m, r′〉
〈c′, c, r〉 →cr 〈c′′, r′〉
〈c′, nc, m, r〉 →n+ 〈0, n, c′′m, r′〉
〈c, c′, r〉 →cr 〈c′′, r′〉
〈nc, n′c′, m, r〉 →n+ 〈n, n′, c′′m, r′〉
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.57/78
Terminazione
A questo punto abbiamo trattato tutte le possibiliconfigurazioni, ma...
In nessun caso il sistema va a finire in unaconfigurazione terminale!
Con le regole attuali il sistema continua a fare passiintermedi all’infinito aggiungendo delle cifre 0 allasinistra del risultato:
0 0 00 ---> 0 ---> 0 ---> ...0 0 0---- ----- -----m 0m 00m
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.58/78
Terminazione
Dobbiamo fare in modo che quando il sistema haconcluso il calcolo faccia una transizione verso laconfigurazione che contiene solo la stringa risultato
Tutte le configurazioni in cui questo deve accaderesono della forma 〈0, 0, m, 0〉
Aggiungiamo quindi questa regola, che non hapremesse:
〈0, 0, m, 0〉 →n+ m
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.59/78
Terminazione
Con questa nuova regola il sistema può decidere, inuna configurazione 〈0, 0, m, 0〉, di fermarsi
Tuttavia, nella stessa configurazione è ancoraapplicabile la regola:
〈c, c′, r〉 →cr 〈c′′, r′〉
〈c, c′, m, r〉 →n+ 〈0, 0, c′′m, r′〉
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.60/78
Non determinismo
Quando ci sono più regole applicabili il sistema puòsceglierne una qualsiasi
In altre parole i sistemi di transizioni possono esserenon deterministici
Per i nostri scopi cercheremo sempre di definire sistemideterministici
Se le grammatiche che usiamo non sono ambigue e setrattiamo ogni configurazione in un’unica regola ilsistema sarà deterministico
In casi come questo ci può essere la necessità di porredelle condizioni per ottenere il determinismo
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.61/78
Condizioni di applicazione
Vogliamo escludere la possibilità che il sistema applichila regola che fa un passo intermedio nellaconfigurazione 〈0, 0, m, 0〉
Per far questo basta aggiungere una condizione logicao nelle premesse o a destra della regola
In questo caso poniamola a destra per mettere inevidenza che si tratta di una condizione di applicabilitàsulla configurazione:
〈c, c′, r〉 →cr 〈c′′, r′〉
〈c, c′, m, r〉 →n+ 〈0, 0, c′′m, r′〉
se 〈c, c′, r〉 6= 〈0, 0, 0〉
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.62/78
Sn+ completato
〈c, c′, 0〉 →cr 〈c′′, r〉
〈c, c′〉 →n+ 〈0, 0, c′′, r〉
(i)
〈c, c′, 0〉 →cr 〈c′′, r〉
〈nc, c′〉 →n+ 〈n, 0, c′′, r〉
(ii)
〈c′, c, 0〉 →cr 〈c′′, r〉
〈c′, nc〉 →n+ 〈0, n, c′′, r〉
(iii)
〈c, c′, 0〉 →cr 〈c′′, r〉
〈nc, n′c′〉 →n+ 〈n, n′, c′′, r〉
(iv)
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.63/78
Sn+ completato
〈0, 0, m, 0〉 →n+ m (v)
〈c, c′, r〉 →cr 〈c′′, r′〉
〈c, c′, m, r〉 →n+ 〈0, 0, c′′m, r′〉
se 〈c, c′, r〉 6= 〈0, 0, 0〉 (vi)
〈c, c′, r〉 →cr 〈c′′, r′〉
〈nc, c′, m, r〉 →n+ 〈n, 0, c′′m, r′〉
(vii)
〈c′, c, r〉 →cr 〈c′′, r′〉
〈c′, nc, m, r〉 →n+ 〈0, n, c′′m, r′〉
(viii)
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.64/78
Sn+ completato
〈c, c′, r〉 →cr 〈c′′, r′〉
〈nc, n′c′, m, r〉 →n+ 〈n, n′, c′′m, r′〉
(ix)
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.65/78
Derivazioni
Proviamo adesso a porre il sistema in una certaconfigurazione e ad applicare le regole
Eseguiamo tutte le transizioni passo dopo passocostruendo una derivazione
Alla fine il sistema si troverà in una configurazioneterminale
Per operare dobbiamo istanziare le regole che abbiamoscritto e fare delle sostituzioni
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.66/78
Esempio di derivazione
Supponiamo di porre il sistema Sn+ nella configurazione〈927, 346〉 e facciamo il primo passo di transizione:
〈927, 346〉
→n+ {(iv), 〈7, 6, 0〉 →cr 〈3, 1〉 }
〈92, 34, 3, 1〉
È stata applicata la regola (iv)
Il matching con la configurazione implica:n = 92, c = 7, n′ = 34, c′ = 6
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.67/78
Sostituzione
Sostituendo i valori nella configurazione della premessaotteniamo:〈7, 6, 0〉 →cr 〈c′′, r〉
Il sistema Scr associa a quella configurazione dipartenza la configurazione di arrivo 〈3, 1〉
Quindi, per rendere vera la premessa della regola(iv), dobbiamo porre c
′′ = 3 e r = 1
In questo modo c′′ e r divengono coperte, cioè
vengono associate a valori intermedi del calcolo
Otteniamo quindi la configurazione risultato sostituendoi valori alle variabili nella configurazione di arrivo dellaregola (iv)
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.68/78
Istanza della regola
La regola che abbiamo applicato è la (iv):
〈c, c′, 0〉 →cr 〈c′′, r〉
〈nc, n′c′〉 →n+ 〈n, n′, c′′, r〉
La sua istanza effettivamente applicata si ottienesostituendo alle variabili tutti i valori che abbiamo loroassociato:
〈7, 6, 0〉 →cr 〈3, 1〉
〈92 7, 34 6〉 →n+ 〈92, 7, 3, 1〉
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.69/78
Derivazione
La configurazione in cui siamo arrivati non è terminale,continuiamo con altri passi:
〈92, 34, 3, 1〉
→n+ {(ix), 〈2, 4, 1〉 →cr 〈7, 0〉 }
〈9, 3, 73, 0〉
→n+ {(vi), 〈9, 3, 0〉 →cr 〈2, 1〉 }
〈0, 0, 273, 1〉
→n+ {(vi), 〈0, 0, 1〉 →cr 〈1, 0〉 }
〈0, 0, 1273, 0〉
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.70/78
Derivazione
Siamo nella configurazione immediatamente precedente aquella terminale:
〈0, 0, 1273, 0〉
→n+ {(v)}
1273
Il sistema, dopo la derivazione, si trova nella configurazione
terminale 1273
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.71/78
Copertura: definizione formale
Data una configurazione γ di un sistema di transizioni oun termine t costruito usando costanti, variabili eoperatori:V ars(γ) (risp. V ars(t)) indica l’insieme di tutte e sole levariabili che compaiono γ (risp. t)
Data una regola condizionale R:V ars(R) è l’insieme di tutte e sole le variabili checompaiono in R
Data una R:π1 π2 . . . πn
γ → γ′
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.72/78
Copertura: definizione formale
Sia x ∈ V ars(R). Diciamo allora che x è coperta in R se esolo se vale una delle seguenti condizioni:
(1) x occorre in γ
(2) esiste in R una premessa πi del tipo y = t tale che y ècoperta in R e x ∈ V ars(t)
(3) esiste in R una premessa πi del tipo x = t tale che tuttele variabili in V ars(t) sono coperte
(4) esiste in R una premessa πi del tipo δ →′ δ′ tale chetutte le variabili in δ sono coperte in R e x ∈ V ars(δ′)
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.73/78
Copertura
Se in una regola ci sono variabili non coperte allora laregola può essere priva di significato operazionale:
〈c, c′, 0〉 →cr 〈c′′, r〉, p, k > 0, p = k + 1
〈nc, n′c′〉 →n+ 〈n, n′, c′′, r〉
Le variabili p e k non sono coperte e difatti non sonologicamente legate al significato della regola
Noi considereremo solo regole in cui le variabili che
appaiono sono tutte coperte
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.74/78
Sostituzione: definizione formale
Sia V = {x1, . . . , xn} un insieme di variabili distinte e siac1, . . . , cn una sequenza di costanti
L’insieme di associazioni ϑ = {c1/x1, . . . , cn/xn} è dettasostituzione per le variabili in V
Esempio: ϑ1 = {92/n, 7/c, 34/n′, 6/c′, 3/c′′, 1/r}
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.75/78
Applicazione di sostituzione
Sia X un termine o una configurazione e siaV = V ars(X) l’insieme delle variabili che vi compaiono
Sia inoltre ϑ una sostituzione per le variabili in V
L’applicazione di ϑ a X, denotata da (X)ϑ, è il termine ola configurazione che si ottiene rimpiazzando in X ognivariabile x con la costante c tale che c/x ∈ ϑ
Il termine o configurazione (X)ϑ verrà detto istanza di Xvia ϑ
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.76/78
Applicazione di sostituzione
Sia R una regola condizionale, sia V = V ars(R)l’insieme di tutte e sole le variabili che occorrono in R esia ϑ una sostituzione per le variabili in V
L’istanza di R via ϑ è la regola condizionale che si ottieneapplicando ϑ a tutti i termini e a tutte le configurazioniche occorrono in R
Esempio: applicando alla regola (iv) la sostituzione ϑ1 siottiene
〈7, 6, 0〉 →cr 〈3, 1〉
〈92 7, 34 6〉 →n+ 〈92, 7, 3, 1〉
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.77/78
Regole e relazione di transizione
Sia S = 〈Γ, T,→〉 un sistema di transizioni la cui relazione ditransizione → è definita mediante un insieme finito di regolecondizionali (r1), . . . , (rn)
Date due configurazioni γ, γ′ ∈ Γ, la coppia (γ, γ′)appartiene alla relazione → se e soltanto se esiste unasostituzione ϑ per le variabili in V ars(ri), con 1 ≤ i ≤ n, taleche:
tutte le premesse di (ri)ϑ sono soddisfatte
la conclusione di (ri)ϑ è γ → γ′
Universita degli Studi di Camerino - Corso di Laurea in Informatica - Programmazione - Semantica - Sistemi di Transizioni (1) – p.78/78