UNIVERSITA’ DEGLI STUDI DI
PADOVA
Facoltà di Scienze Matematiche Fisiche Naturali
Corso di laurea specialistica in Informatica
TESI DI LAUREA
Strutture ad eventi e strategie:
un ponte fra teoria della
concorrenza e semantica dei
giochi
Laureando: Mauro Piccolo
Relatore: prof. Claudia Faggian
Co-relatore: prof. Daniele Varacca
2
Indice
1 Introduzione
1.1 Gli ambiti studiati . . . . . . . .
1.1.1 Teoria della concorrenza .
1.1.2 Semantica dei giochi . . .
1.1.3 Teoria della dimostrazione
1.2 Strutture con ordine parziale . . .
1.2.1 Strutture di eventi . . . .
1.2.2 Strategie lineari: . . . . .
1.3 Scopi, contributi e risultati . . . .
1.4 Struttura della tesi . . . . . . . .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
7
8
8
8
9
9
10
10
11
12
2 Modelli per la concorrenza
2.1 Modelli ad interleaving vs modelli causali . . . . . . . . . . .
2.2 Strutture di eventi . . . . . . . . . . . . . . . . . . . . . . .
2.2.1 Deﬁnizioni . . . . . . . . . . . . . . . . . . . . . . . .
2.2.2 Strutture di eventi senza conﬂitto e senza confusione
2.2.3 Operazioni con le event structure . . . . . . . . . . .
2.2.4 Composizione parallela di strutture di eventi . . . . .
2.3 Discussione . . . . . . . . . . . . . . . . . . . . . . . . . . .
.
.
.
.
.
.
.
15
15
17
18
22
24
26
33
3 Semantica dei giochi
3.1 Introduzione informale alle
3.2 Modello HO . . . . . . . .
3.2.1 Arene . . . . . . .
3.2.2 Partite . . . . . . .
3.2.3 Strategie . . . . . .
3.3 Strategie lineari . . . . . .
3.3.1 L-nets . . . . . . .
3.3.2 Composizione . . .
3.4 Da MALL alle L-nets . .
3.4.1 Logica lineare . . .
.
.
.
.
.
.
.
.
.
.
35
36
39
39
40
41
44
45
48
51
52
.
.
.
.
.
.
.
.
.
strategie
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
. . . . .
3
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
4
INDICE
3.4.2 Un calcolo dei sequenti focalizzato per MALL . . . . . 54
3.4.3 Da MALL alle L- nets . . . . . . . . . . . . . . . . . . 56
3.5 Discussione . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
4 Strutture di eventi tipate
4.1 Strategie come strutture ad eventi senza confusione
4.2 Sistema di etichette . . . . . . . . . . . . . . . . . .
4.2.1 Soggetti e nomi . . . . . . . . . . . . . . . .
4.2.2 Interfacce . . . . . . . . . . . . . . . . . . .
4.3 Strutture di eventi tipate . . . . . . . . . . . . . . .
4.3.1 Proprietà dell’etichettaggio . . . . . . . . . .
4.4 Composizione globale . . . . . . . . . . . . . . . . .
4.4.1 Deﬁnizione . . . . . . . . . . . . . . . . . . .
4.4.2 Proprietà della composizione . . . . . . . . .
4.5 Composizione senza conﬂitti . . . . . . . . . . . . .
4.5.1 Deﬁnizione . . . . . . . . . . . . . . . . . . .
4.5.2 Lavorare con le slice . . . . . . . . . . . . .
4.6 Discussione . . . . . . . . . . . . . . . . . . . . . .
5 Risultati di equivalenza
5.1 Composizione con hiding . .
5.2 Composizione di strutture di
5.3 Risultato di isomorﬁsmo . .
5.4 Risultato di equivalenza . .
5.5 Discussione . . . . . . . . .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
59
60
62
63
63
64
66
69
69
71
72
72
75
77
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
79
80
82
84
88
91
6 CCS polarizzato
6.1 Deﬁnizioni, regole di transizione etichettata . . . . . . . .
6.1.1 Bisimulazione . . . . . . . . . . . . . . . . . . . . .
6.2 Typing system . . . . . . . . . . . . . . . . . . . . . . . . .
6.3 Risultati di type safety . . . . . . . . . . . . . . . . . . . .
6.4 La codiﬁca in strutture di eventi tipate di CCS polarizzato
6.4.1 Deﬁnizione del modello . . . . . . . . . . . . . . . .
6.4.2 Teorema di validità . . . . . . . . . . . . . . . . . .
6.4.3 Corrispondenza fra le semantiche . . . . . . . . . .
6.5 Conclusioni . . . . . . . . . . . . . . . . . . . . . . . . . .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
93
94
95
96
98
99
100
101
102
104
. . . . . . . .
eventi tipate
. . . . . . . .
. . . . . . . .
. . . . . . . .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
A A Graph Abstract Machine Describing Event Structure Composition
111
A.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . 112
A.2 Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114
INDICE
A.2.1 A sketch of strategies composition . . . . . . . . . . .
A.2.2 Event structures . . . . . . . . . . . . . . . . . . . .
A.2.3 Confusion free event structures . . . . . . . . . . . .
A.3 Typed event structures . . . . . . . . . . . . . . . . . . . . .
A.3.1 Names and actions. . . . . . . . . . . . . . . . . . .
A.3.2 Interfaces. . . . . . . . . . . . . . . . . . . . . . . .
A.3.3 Typed event structures. . . . . . . . . . . . . . . . .
A.3.4 Properties of the labelling . . . . . . . . . . . . . . .
A.4 Composition . . . . . . . . . . . . . . . . . . . . . . . . . . .
A.4.1 Compatible interfaces . . . . . . . . . . . . . . . . . .
A.4.2 Conﬂict free composition . . . . . . . . . . . . . . . .
A.4.3 Local rewriting rules . . . . . . . . . . . . . . . . . .
A.4.4 Reducing composition to conﬂict free composition . .
A.4.5 Global composition . . . . . . . . . . . . . . . . . . .
A.5 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . .
A.5.1 Relating with standard event structure composition .
A.5.2 Linear strategies with parallel composition are a subclass of typed event structures . . . . . . . . . . . . .
A.5.3 More comments and future work . . . . . . . . . . .
5
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
114
116
117
118
119
119
120
120
122
122
123
124
124
125
129
129
. 130
. 130
6
INDICE
Capitolo 1
Introduzione
Teoria della concorrenza, semantica dei giochi e teoria della dimostrazione
sono tre importanti aree dell’informatica teorica e della logica. Esse hanno motivazioni diverse, e ciascuna ha strumenti, risultati, ed un linguaggio
proprio, ma esse hanno anche molti punti in comune.
In particolare, un approccio comune consiste nello studio di un determinato fenomemo o oggetto, visto non come una singola entità, ma come parte di
un universo in cui diﬀerenti istanze di questo oggetto interagiscono: si pensi
ad esempio ai processi che eseguono in parallelo in teoria della concorrenza e
dunque al fenomeno del parallelismo. Si parla dunque, per ogni singola area,
di interazione fra gli oggetti.
Una convinzione presente in diversi ambienti di ricerca è che ci possano
essere connessioni profonde tra teoria della concorrenza da una parte, e semantica dei giochi/ teoria della dimostrazione dall’altra. La ricerca di tali
connessioni alimenta in eﬀetti una crescente attività.
Parallelamente, e più speciﬁcatamente, nell’ambito della semantica dei
giochi, un consistente numero di progetti mira a generalizzare in senso concorrente le strutture esistenti, per catturare non-determinismo e calcolo parallelo
[AM99, Mel04, HS02, MW05, SPP05, FM05, CF05, Lai05, GM04].
Questo lavoro si colloca nella linea di entrambe tali direzioni. In particolare, il nostro studio si è concentrato sull’analisi di una struttura comune, che
appare sia nei modelli causali della concorrenza, che in semantica dei giochi.
Infatti, le due aree usano entrambe strutture di ordini parziali: da una parte
abbiamo le strutture di eventi, dall’altra le strategie linari.
Questo capitolo si strutturerà come segue: anzitututto verrà data una
breve introduzione sulla teoria della conocorrenza, semantica dei giochi e
teoria della dimostrazione, speciﬁcando per ciascun ambito quale è l’oggetto di studi e che cosa si intende per interazione. Poi si entrerà nei dettagli
di ciascuna area allo scopo di precisare quali strutture sono prese in con7
8
Introduzione
siderazione e in particolare ci si concentrerà su teoria della concorrenza e
semantica dei giochi analizzando rispettivamente le strutture di eventi e le
strategie lineari. Inﬁne si entrerà nei dettagli del lavoro svolto, precisandone
lo scopo iniziale e i risultati ottenuti.
1.1
1.1.1
Gli ambiti studiati
Teoria della concorrenza
In teoria della concorrenza, l’oggetto di studio è il processo (intuitivamente
un processo è un insieme di azioni svolte in un certo ordine), visto non come
singola entità, ma come parte di un sistema attraverso il quale può interagire
con altri processi. Utilizzando le parole di Edsger Dijkstra (1930 - 2002)
Concurrency occurs when two or more execution ﬂows are able to run
simultaneouslyγ (La concorrenza accade quando due o più ﬂussi di
esecuzione sono in grado di eseguere simmultaneamente)
L’interazione è l’essenza stessa della teoria: si intende studiare tutte le
problematiche che occorrono quando due o più processi eseguono in parallelo
e comunicano tra loro.
1.1.2
Semantica dei giochi
In semantica dei giochi, l’oggetto di studio è il programma (processo di
calcolo o funzione calcolabile). In questo contesto la computazione è modellata come una partita, un gioco tra due entità che sono l’opponente, che
rappresenta l’ambiente e il proponente (detto anche player) che rappresenta il programma. L’oggetto principale, usato per modellare un programma,
è la strategia, che di fatto rappresenta un insieme di possibili partite fra
opponente e proponente. Il concetto di interazione qui è dato dalla composizione di strategie, che corrisponde alla composizione di due programmi o
alla composizione di funzioni (se si pensa in termini di funzioni calcolabili).
La semantica dei giochi è divenuta recentemente un ambito di ricerca
ﬁorente a causa della sua versatilità: infatti il modello a giochi, pur essendo
suﬃcentemente astratto, descrive molto bene il comportamento operazionale
dei programmi e questa sua peculiarità ha reso possibile la costruzione di
numerosi modelli fully abstract per parecchi linguaggi di programmazione,
tra i quali il più famoso è certamente quello per PCF [HO00, AJM00, Cur06].
Strutture con ordine parziale
1.1.3
Teoria della dimostrazione
La teoria della dimostrazione è una branca della logica matematica che rappresenta prove sotto forma di oggetti matematici formali, come ad esempio
liste oppure alberi, i quali sono costruiti seguendo delle regole ben precise.
Utilizzando le parole di Gehart Gentzen (1909 - 1945)
Ich wollte zunächst einmal einen Formaulismus aufstellen, der dem
wirklichen Schliessen möglichst nahe kommt. So ergab sich ein ‘Kalkül des
natürlichen Schliessens’γ1 (Io volevo anzitutto costruire un formalismo che
sia il più possibile vicino al ragionamento vero. Questo ha portato al
calcolo della deduzione naturale)
L’interazione fra prove qui assume un’aspetto fondamentale: intuitivamente se si hanno le prove, descritte utilizzando un certo sistema, di A ⇒ B
e di B ⇒ C allora esiste una prova di A ⇒ C e tale prova è ottenuta, nel
caso del calcolo dei sequenti, utilizzando una procedura detta eliminazione
del taglio.2
1.2
Strutture con ordine parziale
Ciascun ambito ha un oggetto di studio, descritto utilizzando determinate
costruzioni matematiche: in particolare, in tutte e tre gli ambiti è possibile
descrivere gli oggetti di studio mediante ordini parziali. Più precisamente,
in teoria della concorrenza, vi è un’importatante sottoclasse dei modelli utilizzati, detta classe dei modelli causali, in cui strutture dotate di ordini
parziali sono utilizzate per modellare processi (si pensi ad esempio alle reti
di Petri o alle strutture di eventi). In semantica dei giochi, un’importante
sottoclasse delle strategie, detta classe delle strategie lineari [Gir01], è utilizzata come modello per la logica lineare ed esse sono descritte mediante
ordini parziali. Inﬁne, in teoria della dimostrazione, vi sono le reti di prova che sono rappresentazioni a grafo delle prove in calcolo dei sequenti della
logica lineare [Gir87]. Tutte queste strutture possono essere dunque descritte
utilizzando degli ordini parziali oppure utilizzando strutture ben note in teoria dei graﬁ, ovvero dei graﬁ diretti acliclici (d.a.g.) con nodi etichettati (dove
1
39
Gentzen - Untersuchungen über das logische Schliessen - Mathematische Zeitschrift
2
Il teorema di eliminazione del taglio è un risultato molto importante all’interno di un
qualunque sistema formale. Una sua importante conseguenza è la consistenza del sistema
stesso.
9
10
Introduzione
le etichette sono azioni in teoria della concorrenza, mosse in semantica dei
giochi, regole in teoria della dimostrazione).
In particolare, in questo elaborato, ci si concentrerà sulla corrispondenza
fra teoria della concorrenza e semantica dei giochi, e più precisamente sulla
corrispondenza fra strutture di eventi (che sono un modello causale) e
strategie lineari.
1.2.1
Strutture di eventi
Le strutture di eventi sono modelli per la concorrenza causali (detti anche modelli veramente concorrenti), i.e. modelli dove la causalità, concorrenza e conﬂitti sono direttamente rappresentati, in opposizione ai modelli ad interleaving, che descrivono un sistema mediante tutte le possibili
sequenzializzazioni delle azioni concorrenti.
Una struttura di eventi modella la computazione parallela per mezzo di
• eventi che sono occorrenze di azioni
• un ordine parziale che esprime la dipendenza causale
Il non determinismo è modellato per mezzo di
• una relazione di conﬂitto che esprime come l’occorrenza di certi eventi
escluda l’occorrenza di altri
Due eventi sono concorrenti se non sono nè causalmente correlati, nè in
conﬂitto. Eventi in conﬂitto vivono in diﬀerenti evoluzioni del sistema.
In particolare, in questo elaborato, si parlerà di strutture ad eventi
senza confusione, che sono una sotto-classe delle strutture ad eventi, nella
quale il non-determinismo ‘si comporta bene’, ovvero la scelta non determinista è ben ‘localizzata’ in un ben preciso punto della struttura. Questa
sotto-classe è inoltre utilizzata in [VY06] per costruire un modello a strutture
di eventi di π-calcolo.
1.2.2
Strategie lineari:
Le strategie lineari sono delle strategie introdotte come modello per la logica
lineare. Esse sono state introdotte da Girard in [Gir01] ed estese sotto forma
di d.a.g. etichettati, dunque ordini parziali in [FM05]. L’uso di ordini parziali
per descrivere strategie è utilizzato non per descrivere l’ordine con cui le
mosse veranno eseguite, bensı̀ quello di esprimere vincoli di causalità.
Scopi, contributi e risultati
1.3
Scopi, contributi e risultati
Il problema dal quale questo lavoro è partito è il seguente: confrontare le
strutture di eventi senza confusione in teoria della concorrenza e le strategie
lineari in semantica dei giochi allo scopo di poter mappare l’ultima struttura
nella prima. Una volta descritte le strategie lineari come strutture di eventi
senza confusione, ci interessava studiare la nozione di composizione, e in
particolare determinare se ci fosse equivalenza tra
• la composizione di strategie propria alla semantica dei giochi
• la composizione delle stesse strategie interpretate come strutture di
eventi, utilizzando la composizione di struture di eventi data in [VaraccaYoshida].
Tale corrispondenza fra strategie lineari e strutture ad eventi senza confusione è stata eﬀettivamente stabilita.
Tale primo risultato è stato inoltre esteso, arrivando ad ottenere una
deﬁnizione di una struttura generale equipaggiata con una nozione di interazione che è tale per cui:
• se portata nell’ambito semantica dei giochi, di incarnare una strategia lineare e l’operazione di interazione deﬁnita sarà equivalente alla
composizione di strategie lineare
• se portata nell’ambito teoria della concorrenza, di incarnare una struttura di eventi senza confusione e l’operazione di interazione deﬁnita
sarà equivalente alla deﬁnizione di composizione di strutture ad eventi
data in [Varacca-Yoshida].
Tale risultato rappresenta il principale contributo della tesi.
La nozione di interazione, che nella tesi è denominata composizione
globale, è una generalizzazione della procedura di composizione di strategie
lineari data in [Fag02] e denominata macchina LAM.
In questo lavoro sono inoltre stati ottenuti i seguenti risultati speciﬁci
• deﬁnizione di un typing system per le strutture ad eventi senza confusione che garantisce la preservazione dell’assenza di confusione per
composizione.
• applicazione della tecnica ‘working by slice’ propria della semantica dei
giochi e usata per la normalizzazione delle L-nets, alle strutture ad eventi senza confusione, allo scopo di ridurre la procedura di composizione
globale al caso senza conﬂitto.
11
12
Introduzione
• riformulazione della deﬁnizione di composizione di strutture di eventi senza conﬂitto mediante regole di riscrittura di grafo. In particolare questo permette di mostrare la conﬂuenza e l’associatività della
composizione.
• analisi di un frammento di CCS, del quale si è fornito un modello a
strutture ad eventi tipate, del quale si sono mostrate validità e dei
risultati di corrispondenza con la semantica operazionale, fra i quali
spicca la full abstraction
Inoltre, la deﬁnizione di composizione elaborata in questa tesi apporta un
contributo nuovo anche in semantica dei giochi, in quanto la composizione
globale qui introdotta realizza in particolare la composizione globale di strategie lineari, per le quali la composizione era stata deﬁnita in [FM05] e [CF]
solo in termini di slices3 .
1.4
Struttura della tesi
Questa tesi si struttura in 6 capitoli. I capitoli 2 e 3 sono capitoli di introduzione all’argomento. Il contributo di questa tesi è riportato nei capitoli 4,
5, 6.
Il presente elaborato si strutturerà come segue. Nel capitolo 2 si introdurranno in modo generale le due classi principali dei modelli per la concorrenza, che sono i modelli ad interleaving e i modelli causali, per
poi passare ad introdurre le strutture ad eventi, le relative proprietà e la
nozione di composizione. Nel capitolo 3 si introdurrà la semantica dei giochi
stile Hyland-Ong, parlando anzitutto della parte di quest’ultima utilizzata
per costruire modelli per linguaggi di programmazione. Poi si introdurrà la
semantica dei giochi stile Girard (strategie lineari), che è la semantica dei
giochi HO utilizzata per costruire modelli per la logica lineare. Ci si concentrerà principalmente su quest’ultima, introducendo una struttura detta
L-net, introdotta da Claudia Faggian e Francois Maurel in [FM05]. Questa
sarà la struttura di riferimento nel capitolo 4 nel quale si mostrerà appunto
la corrispondenza fra L-net e strutture ad eventi, in particolare mostrando
che una L-net è una particolare struttura ad eventi senza confusione. Si procederà dunque a studiare le strutture ad eventi senza confusione costruendo
un sistema di tipi e dando una deﬁnizione di composizione, che è la generalizzazione di una deﬁnizione di composizione di strategie in semantica dei
3
Come conseguenza, ci aspettiamo di avere un’analoga procedura di composizione
‘globale’ per le reti di prova additive che sono attualmente sviluppate a partire dagli
L-nets
Struttura della tesi
giochi. Nel capitolo 5 si mostrerà che questa deﬁnizione di composizione
è eﬀettivamente equivalente alla composizione di strutture ad eventi data in
[VY06]. Inﬁne nel capitolo 6 si mostrerà la versatilità della struttura studiata nel capitolo 4, deﬁniendo un modello fully abstract di un frammento
di CCS, detto CCS polarizzato, in questa struttura.
Questa tesi è stata realizzata all’interno di una attività di stage svolta
presso l’Università di Parigi 7 nel laboratorio P.P.S. (Preuves Programmes
et Systèmes).
La parte inizile di questa tesi è stata presentata a GT-VC (Graph Transformation for Veriﬁcation and Concurrency) che è un workshop satellite
della conferenza internazionale CONCUR’06 sulla teoria della concorrenza,
svoltasi a Bonn (Germania) dal 27 al 30 agosto. Il relativo articolo appare
nei Proceedings del workshop ed è riportato in appendice alla tesi.
13
14
Introduzione
Capitolo 2
Modelli per la concorrenza
Lo studio dei fenomeni e delle problematiche legate alla concorrenza sono
di fatto un’attività basilare che interessa diﬀerenti ambiti nella realtà e in
molti livelli, dal microchip ﬁno ai sistemi multiprocessore. Il multitasking,
ovvero la capacità di eseguire più di un compito parallelamente, da parte dei
moderni sistemi reattivi è divenuto caratteristica essenziale.
Tuttavia un concetto che a prima vista può apparire semplice come eseguire due o più azioni (o insiemi di azioni) in modo contemporaneo, può essere
fonte di problemi, spesso di diﬃcile soluzione: problemi come il deadlock, il
livelock, la starvation, l’inconsistenza dovuta all’accesso a risorse condivise,
la mutua esclusione sono molto studiati soprattutto dai progettisti di sistemi
concorrenti in quanto di diﬃcile individuazione. Quindi, dire che un sistema
concorrente è corretto (ovvero libero dai problemi sopra citati) è diﬃcile da
mostrare.
Ecco dunque che si rende necessario studiare il problema ad un livello più
alto creando un modello astratto del sistema che si vuole costruire, sul quale
verranno dimostrate le proprietà di correttezza desiderate, e (se il modello è
abbastanza accurato) tali proprietà si riﬂettono sul sistema concreto.
In letteratura sono stati utilizzati vari formalismi per modellare sistemi
reattivi concorrenti, come riportato in [WN95]. Lo scopo di questo capitolo è
dare un’introduzione generale, per poi concentrarsi in uno speciﬁco modello
molto utilizzato per studiare processi concorrenti non deterministici, ovvero
le strutture di eventi [NPW81, Win87, Win82].
2.1
Modelli ad interleaving vs modelli causali
I modelli per la concorrenza possono essere classiﬁcati in base a vari criteri.
Una possibile classiﬁcazione prevede la distinzione fra modelli ad interleaving
15
16
Modelli per la concorrenza
e modelli causali.
Nei modelli ad interleaving, la concorrenza è modellata attraverso la scelta
non deterministica tra tutte le possibili sequenzializzazioni delle azioni concorrenti compiute dal sistema, mentre nei modelli causali viene deﬁnita una
relazione di concorrenza e di mutua esclusione (conﬂitto) fra le azioni che
compongono i vari task.
Esempio: Siano P1 e P2 due processi che devono eseguire in parallelo (indicato come P1 P2 ) e che compongono un sistema concorrente reattivo1 . Il
processo P1 svolge prima l’azione a1 e poi l’azione a2 , mentre il processo P2
svolge l’azione b. Vediamo ora come P1 P2 possa essere modellato in ciascuna
delle due istanze di modello
modelli ad interleaving: in questa tipologia di modello, P1 P2 viene modellato esprimendo tutte le possibili schedulazioni delle azioni compiute
dai due processi in parallelo. Ciò può essere espresso dando tutte le
possibili tracce del sistema, che nel nostro caso sono
{a1 a2 b, a1 ba2 , ba1 a2 }
oppure mediante un automa
a2 b
a2
b
a1
b
a1 .a2 b
b
b
a1 .a2
a1
0
a2
a2
modelli causali: in questa tipologia di modello, P1 P2 viene modellato
esplicitando le relazioni di ordine e di conﬂitto che vi sono fra le azioni,
per poter identiﬁcare quali azioni possono essere svolte in concorrenza.
Nel nostro caso, abbiamo un insieme di azioni A = {a1 , a2 , b} su cui è
deﬁnita una relazione <= {(a1 , a2 )} e da questo possiamo inferire che,
l’azione b può essere svolta contemporaneamente (in concorrenza) con
le azioni a1 ed a2
1
Un sistema concorrente è diﬃcile da caratterizzare: nel seguito utilizzeremo una
sintassi CCS-like per descrivere un sistema concorrente con i relativi task.
Strutture di eventi
17
a2
a1
b
I modelli ad interleaving sono ideali per evidenziare aspetti osservazionali
del sistema: ad esempio sono utili per focalizzare l’attenzione su tutte le possibili interazioni del sistema con l’ambiente esterno. In particolare, l’utilizzo
di modelli ad interleaving è utile per delineare equivalenze osservazionali di
due o più sistemi, modellate tramite relazioni di bisimulazione: nella realtà,
due sistemi sono equivalenti osservazionalmente se essi si comportano allo
stesso modo a partire da una stessa condizione2 : nel modello signiﬁca che
due oggetti sono bisimili se anch’essi, nel modello si evolvono allo stesso modo
a partire da una data condizione3 .
Vi sono tuttavia interessanti proprietà di un sistema concorrente, come
ad esempio l’assenza di conﬂitto fra azioni, l’indipendenza delle scelte da
eventuali politiche di scheduling e la sequenzialità che non sono percepite
come proprietà osservazionali e che, utilizzando un modello ad interleaving,
sono diﬃcili da esprimere. Queste sono proprietà legate alla causalità delle
azioni, che è una caratteristica catturata dai modelli causali, utilizzando i
quali è possibile esprimere queste proprietà in modo semplice. Al contrario
per i modelli ad interleaving, tali proprietà sono di diﬃcile espressione, in
quanto la causalità delle azioni non è una proprietà osservabile.
Quindi i modelli ad interleaving sono pensati per caratterizzare un sistema
dal punto di vista osservazionale, mentre i modelli causali vengono utilizzati
per esprimere proprietà legate alla causalità delle azioni.
2.2
Strutture di eventi
Nell’ambito dei modelli causali, le strutture di eventi sono state oggetto di
numerosi studi, in quanto esse costituivano un framework generale, in cui
2
In un contesto macchina a stati, si intende dallo stesso stato oppure espresso in modo
più concreto, dallo stesso contenuto di dati in memoria, i quali sono situati in una stessa
posizione.
3
più precisamente, se un oggetto è in grado di eﬀettuare una determinata azione e ad
arrivare ad un determinato stato (che nella realtà rappresenta una data conﬁgurazione del
sistema), allora anche l’altro oggetto è in grado di fare altrettanto e di giungere ad uno
stato che sia comparabile con lo stato a cui è arrivato l’oggetto precedente
18
Modelli per la concorrenza
altre strutture potevano trovare espressione [WN95]. Esse furono introdotte
da Nielsen, Plotkin e Winskel [NPW81, Win80] come un modello per sistemi
concorrenti non deterministici e sono apparse in forme diﬀerenti. Quella
che verrà utilizzata nel seguito sarà la nozione di struttura di eventi prima
[Win87].
2.2.1
Deﬁnizioni
Come aﬀermato precedentemente, le strutture di eventi sono utilizzate per
modellare sistemi concorrenti non deterministici. Informalmente, una struttura di eventi modella la computazione parallela attraverso
• eventi che sono occorrenze di azioni
• un ordinamento parziale che esprime la dipendenza causale delle azioni
mentre il non determinismo è espresso attraverso
• una relazione di conﬂitto che esprime come l’occorrenza di determinate
azioni escluda l’occorenza di altre.
Quindi due eventi sono detti concorrenti se non sono nè legati causalmente
e nemmeno in conﬂitto, e due eventi sono in conﬂitto se vivono in diﬀerenti
evoluzioni del sistema.
Deﬁnitione 2.2.1 (Struttura di eventi). Una struttura di eventi è una
tripla E = E, ≤, dove
• E è un insieme ﬁnito o numerabile di eventi
• E, ≤ è un ordine parziale, detto ordine causale
• per ogni e ∈ E, l’insieme [e) = {e |e ≤ e}, detto insieme abilitante
di e, è ﬁnito
• è una relazione non riﬂessiva e simmetrica, detta relazione di
conﬂitto, soddisfacente la proprietà di ereditarietà
∀e1 , e2 , e3 ∈ E.e1 ≤ e2 ∧ e1 e3 ⇒ e2 e3
(2.1)
Con un abuso di notazione, nel seguito, data una strutura ad eventi E si
scriverà che e ∈ E per indicare che e appartiene all’insieme degli eventi di E.
Inoltre dato e ∈ E si denoterà
• parents(e) l’insieme degli eventi massimali secondo ≤ di [e).
Strutture di eventi
19
• e
= [e) ∪ {e}
In base all’ereditarietà è possibile distinguere i conﬂitti tra eventi tra
conﬂitti ereditati e non: quindi dati e1 , e2 , e3 ∈ E diciamo che e2 e3 è
un conﬂitto ereditato da e1 e3 se e1 < e2 . Se e1 e3 non è ereditato da
nessun altro conﬂitto allora esso si dice immediato e si indica con e1 µ e3 .
La chiusura riﬂessiva dei conﬂitti (risp. dei conﬂitti immediati) si indica
con (risp. µ ). Si noti inoltre che il conﬂitto e l’ordinamento causale sono
mutualmente esclusivi. Due eventi si dicono concorrenti se non sono nè in
conﬂitto, nè legati causalmente.
E’ importante notare che gli eventi qui sono intesi come occorrenze di
azioni. Si prenda ad esempio la seguente situazione.
Esempio 1: si intende modellare con una strutura di eventi la seguente
semplice situazione: si supponga che un processo consumatore richieda due
volte l’accesso ad una risorsa R: la prima volta la trova libera e vi accede
e poi ne esce e poi la accede di nuovo. Dunque le azioni che compie sono
ask(R) e exit(R) e poi nuovamente ask(R). La corrispondente struttura di
eventi è dunque:
ask(R)
e3
exit(R)
e2
ask(R)
e1
Si noti che gli eventi e1 ed e3 sono occorrenze della stessa azione ask(R).
Esempio 2: un esempio più strutturato un sistema concorrente può
eseguire in modo mutualmente esclusivo le azioni a e b e può eseguire l’azione
c solo dopo l’esecuzione di una delle due azioni precedenti. Vogliamo costruire la corrispondente struttura di eventi E. Ovviamente avremo due eventi
ea , eb ∈ E corrispondenti alle azioni a e b con ea eb , le quali occorrono
una sola volta. L’azione c invece occorre due volte: o dopo a o dopo b e
quindi avremo due eventi ec1 , ec2 ∈ E con ea ≤ ec1 ed eb ≤ ec2 : si noti che
20
Modelli per la concorrenza
per ereditarietà abbiamo ec1 ec2 . Nel seguito vi è una rappresentazione
graﬁca della struttura di eventi costruita: i conﬂitti immediati sono indicati
con linee ondulate.
e c1
e c2
c
c
a
b
ea
eb
Il precedente esempio induce ad introdurre una nozione di struttura di
eventi, a cui ad ogni evento è associata l’azione (etichetta) corrispondente:
abbiamo dunque la seguente
Deﬁnitione 2.2.2 (Struttura di eventi etichettata). Una struttura di
eventi etichettata è una quadrupla E = E, ≤, , λ dove:
• E, ≤, è una struttura di eventi.
• λ : E → L è una funzione di etichettaggio, in cui L è un insieme di
etichette (azioni).
Nel seguito, ove non speciﬁcato diversamente, quando si parlerà di struttura di eventi si intenderà una struttura di eventi etichettata, ovvero una
struttura di eventi con una funzione di etichettatura.
Esempio: Prendendo come riferimento il precedente esempio, possiamo
costruire la relativa event structure etichettata Elab con λ : E → L dove
L = {a, b, c}, con l’etichettatura λ(ea ) = a, λ(eb ) = b, λ(ec1 ) = c, λ(ec2 ) = c.
Il precedente esempio e la naturale interpretazione aiutano a formulare
una nozione di stato (traccia) della computazione di una struttura di eventi
E. Una nozione ragionevole può essere data dall’insieme di azioni che sono
occorse nella computazione (gli eventi) e in particolare per insiemi sı̀ fatti ci
si aspetta che
• se un evento appartiene a questo insieme, allora tutti gli eventi dai
quali esso dipende causalmente devono appartenere a questo insieme
• non ci sono due eventi in conﬂitto fra loro che appartengono a questo
insieme
Strutture di eventi
21
Da qui quindi abbiamo la seguente:
Deﬁnitione 2.2.3 (conﬁgurazione). Sia E una struttura di eventi e sia
C ⊆ E un insieme di eventi. C è una conﬁgurazione se valgono le seguenti
proprietà
assenza di conﬂitto
∀e, e ∈ C.e e
chiusura verso il basso
∀e, e ∈ E . (e ≤ e ∧ e ∈ C) ⇒ e ∈ C
Data una struttura di eventi E, si denota con L(E) l’insieme delle conﬁgurazioni di E. Si noti che dato e ∈ E, [e), e
sono conﬁgurazioni.
Un evento e si dice abilitato da una conﬁgurazione C se x ∪ {e} è una
conﬁgurazione. Due conﬁgurazioni C1 , C2 si dicono compatibili se C = C1 ∪C2
è una conﬁgurazione.
Lemma 2.2.1 (compatibilità). Sia E una struttura di eventi e siano e1 , e2
due eventi distinti. e1 e2 se e solo se e1 e e2 non sono compatibili.
Dimostrazione. Si supponga e1 e2 : allora e1 e e2 non possono essere
compatibili. Dall’altro lato, si prendano e1 ed e2 tali che e1 e e2 non sono
compatibili. Allora esistono d1 ∈ e1 , d2 ∈ e2 tali che d1 d2 . Allora per
ereditarietà e1 e2
La relazione di transizione da una conﬁgurazione all’altra, data come
sistema di transizione etichettato è pertanto deﬁnita come segue:
Deﬁnitione 2.2.4 (Labelled Transition System). Sia E una struttura
di eventi, siano C, C ∈ L(E) due conﬁgurazioni e sia a ∈ L un’etichetta. Si
scrive
C → C ⇐⇒ ∃e ∈ E . λ(e) = a ∧ e ∈ C ∧ C = C ∪ {e}
a
Esempio: prendendo come riferimento il precedente esempio, il sistema di
transizione etichettata indotto dalla struttura di eventi E è il seguente:
22
Modelli per la concorrenza
{eb , ec2 }
{ea , ec1 }
c
c
{eb }
{ea }
a
b
∅
2.2.2
Strutture di eventi senza conﬂitto e senza confusione
Una sottoclasse importante delle strutture di eventi è la seguente:
Deﬁnitione 2.2.5 (Struttura di eventi senza conﬂitto). Una struttura
di eventi E si dice senza conﬂitto se non contiene due eventi distinti che sono
tra loro in conﬂitto
Ovvimaente una struttura di eventi senza conﬂitto E ha la relazione vuota ed è semplicemente un ordine parziale. Inoltre la proprietà di assenza
di conﬂitti è la versione secondo i modelli causali della conﬂuenza: è infatti semplice dimostrare che data E senza conﬂitti, il sistema di transizione
etichettato dedotto da E è conﬂuente.
L’introduzione del conﬂitto serve, come detto sopra, per modellare il non
determinismo. Per poter meglio studiare la natura del non determinismo, si
intende studiare nel seguito una forma di non determinismo che si ‘comporta
bene’, ovvero che garantisca delle proprietà di indipendenza dallo scheduling
delle azioni (la scelta del sistema in un certo stato è invariante rispetto alla
politica di schedulazione delle azioni non legate causalmente eﬀettuata dal
sistema). Per studiare questa proprietà è stata introdotta un’importante
sottoclasse delle strutture di eventi con conﬂitto, che è la seguente
Deﬁnitione 2.2.6 (Struttura di eventi senza confusione). Sia E una
struttura di eventi. Essa è senza confusione se valgono le seguenti
transitività per ogni e, e , e ∈ E distinti, e µ e e e µ e implica e µ
e
cellularità per ogni e, e ∈ E, e µ e implica [e) = [e )
Si osservi che, in base a quanto detto sopra, l’assenza di confusione comporta una forma di non determinismo controllata e localizzata in una determinata conﬁgurazione del sistema. Tale localizzazione è detta cella ed è
Strutture di eventi
23
deﬁnita come un insieme di eventi che sono tra loro in conﬂitto e che hanno
lo stesso insieme abilitante: più formalmente
Deﬁnitione 2.2.7 (cella). Una cella c è un insieme massimale di eventi
tale che per ogni e, e ∈ c vale e µ e e [e) = [e )
Lemma 2.2.2. Sia E una struttura ad eventi senza confusione. Allora la
relazione µ è una relazione di equivalenza e le classi di equivalenza sono le
celle della strutura di eventi
Dimostrazione. µ è per deﬁnizione riﬂessiva, simmetrica e transitiva, pertanto è un’equivalenza. Sia dunque Ce = {e |e µ e}. Per cellularità tutti
gli e ∈ Ce hanno lo stesso insieme abilitante. Inoltre Ce è massimale per
costruzione.
Le strutture ad eventi senza confusione, dunque, modellano una forma
di non determinismo controllata, molto utile per caratterizzare quei sistemi
in cui le scelte non deterministiche non dipendono dalla schedulazione di
componenti indipendenti da tali scelte: per illustrare meglio questo concetto,
si consideri il seguente esempio:
Esempio: di seguito diamo una rappresentazione graﬁca di due strutture
di eventi, una con e una senza confusione
(1.) Senza confusione
t3
t4
(2.) Confusione
t5
t3
t4
t2
t2
t1
t1
t5
Si supponga che esse modellano ciascuna un sistema concorrente non
deterministico in cui vengono eseguiti un insieme di task T = {t1 , t2 , t3 , t4 , t5 }
e ciascuna struttura di eventi deﬁnisce un ordine causale e una relazione di
conﬂitto fra questi task. Si supponga che il sistema debba schedulare tali
task. Nel caso senza confusione (1.), lo scheduler deve partire con t1 . Poi la
situazione è la seguente:
• dopo t1 , lo scheduler può scegliere o t5 o uno fra t2 , t3 , t4
24
Modelli per la concorrenza
• se lo scheduler sceglie t1 e uno fra t2 , t3 , t4 , esso può ancora scegliere t5
• se lo scheduler sceglie t1 e t5 , allora esso può ancora scegliere uno tra
t2 , t3 , t4
Il caso (2.) invece descrive una situazione che è confusa: cambiando
lo scheduling dei task, alcune scelte che erano disponibili, potrebbero non
esserlo più.
Se si osserva la ﬁgura, si vede che sia t1 che t4 non hanno task propedeutici
e quindi possono essere schedulati per primi. Dopo t1 è possibile scegliere
uno tra t2 , t3 , t4 oppure t5 . Ma se si sceglie t4 e poi t1 , la scelta tra t2 , t3 non
risulta essere più disponibile.
2.2.3
Operazioni con le event structure
Di seguito si deﬁniscono alcune operazioni sulle strutture di eventi etichettate:
preﬁssamento: Sia E = E, ≤, , λ una struttura di eventi e sia a un’etichetta. Si deﬁnisce a.E = E , ≤ , , λ come segue:
• E = E ∪ {e} con e ∈ E
• ∀d, d ∈ E . d ≤ d ⇒ d ≤ d . Inoltre ∀d ∈ E . e ≤ d
• =
• λ (d) =
a
se d = e
λ(d) altrimenti
a.E
E
a
e
somma preﬁssata: Siano ai .Ei = Ei ∪ {ei }, ≤i , i, λi con i ∈ I una
famiglia di strutture di eventi preﬁssate (dove ei è l’evento aggiunto
a causa dell’operazione di preﬁssamento e ai = aj , ei = ej , Ei ∩ Ej = ∅
con i = j). Si deﬁnisce i∈I ai .Ei = E, ≤, , λ dove
Strutture di eventi
• E=
25
i∈I (Ei
∪ {ei }).
• ∀i ∈ I . ∀d1 , d2 ∈ ai .Ei . d1 ≤i d2 ⇐⇒ d1 ≤ d2
• ∀d1 , d2 ∈ E.d1 d2 se e solo se valgono le seguenti
– d1 , d2 ∈ ai .Ei con d1 i d2
– ei ∈ d1 e ej ∈ d2 con i = j
• λ(d) = λi (d) se d ∈ ai .Ei
n
j=1
E1
aj .Ej
Ei
a1
En
ai
...
...
an
unione: Siano Ei = Ei , ≤i , i, λi con i ∈ I una famiglia
di strutture di
eventi tali che Ei ∩ Ej = ∅ se i = j. Si deﬁnisce i∈I Ei = E, ≤, , λ
dove:
• E = i∈I Ei
• ∀i ∈ I . ∀d1 , d2 ∈ Ei . d1 ≤i d2 ⇐⇒ d1 ≤ d2
• ∀i ∈ I . ∀d1 , d2 ∈ Ei . d1 i d2 ⇐⇒ d1 d2
• λ(d) = λi (d) se d ∈ Ei
restrizione: Sia E = E, ≤, , λ una struttura di eventi e sia X un insieme
di etichette. Ponendo up(EX ) = {e ∈ E|e ≥ d con d ∈ EX } dove
EX = {e ∈ E|λ(e) ∈ X}, si deﬁnisce E \ X = E , ≤ , , λ dove:
• E = E \ up(EX )
• ∀d1 , d2 ∈ E . d1 ≤ d2 ⇐⇒ d1 ≤ d2
• ∀d1 , d2 ∈ E . d1 d2 ⇐⇒ d1 d2
• λ (d) = λ(d)
E \ {a, b}
i
g
h
c
d
f
e
a
b
26
Modelli per la concorrenza
rietichettatura: Sia E = E, ≤, , λ una struttura di eventi e sia f : L →
L. Si deﬁnisce E[f ] = E, ≤, , f ◦ λ
E’ facile vedere che tutte le suddette operazioni preservano la classe delle
strutture di eventi senza confusione. Inoltre, con l’ovvia eccezione della
somma preﬁssata, esse preservano la classe delle strutture di eventi senza
conﬂitto.
2.2.4
Composizione parallela di strutture di eventi
Fare interagire tra loro due o più sistemi concorrenti comporta determinate
problematiche: occorre infatti considerare il fatto che le azioni compiute
possano essere in qualche modo dipendenti tra loro (ad esempio il risultato parziale di una azione di un sistema deve essere utilizzato in input da
una procedura dell’altro sistema). In un certo senso, dunque occorre modellare queste interdipendenze e capire come esse possano inﬂuire nel sistema
globale; in particolare occorre capire se e come determinate proprietà di correttezza4 , eﬀettuando l’interazione di più sistemi, che singolarmente le rispettano, vengano preservate. Questo è un problema interessante, in quanto le
interdipendenze che si instaurano fra le azioni dei sistemi coinvolti potrebbero causare l’insorgere di problemi che minano la correttezza del sistema
complessivo.
In particolare, ciò che si intende deﬁnire in questa sezione, è la composizione parallela di due strutture di eventi (che modellano sistemi), e discutere
se tale operazione preserva le classi delle strutture di eventi senza conﬂitto e
senza confusione.
Azioni polarizzate
Nelle sezioni precedenti un’azione è stata modellata come un’etichetta, anche
se non è stata data alcuna deﬁnizione formale. A questo scopo, dunque si
cercherà dunque di caratterizzare meglio un’azione, fornendo all’etichetta che
la rappresenta le informazioni aggiuntive per capire come essa si relaziona con
l’ambiente in cui opera. Si consideri per iniziare il seguente esempio:
Esempio: Si intende qui modellare una semplice macchina distributrice di
caﬀè M: essa è in grado di eseguire due azioni, nell’ordine:
• inizialmente richiede l’inserimento di una moneta (evento e1 )
4
esse possono essere assenza di deadlock, livelock, confusione, inconsistenza dovuta ad
accesso contemporaneo a risorse condivise e tutti i problemi già citati
Strutture di eventi
27
• poi produce un bicchiere pieno di caﬀè (evento e2 )
Essa interagisce con un processo cliente C che, nell’ordine
• inizialmente inserisce una moneta nella macchina (evento e3 )
• poi prende il bicchiere di caﬀè prodotto dalla macchina (evento e4 )
Gli eventi e1 ed e3 corrispondono ad azioni che operano sul medesimo soggetto
(l’uso della moneta), ma la natura di questo utilizzo è duale nei due processi
(C la rende, la dà in output mentre M la richiede, la vuole in input). Lo
stesso anche per gli eventi e2 ed e4 , per i quali la risorsa dell’azione a cui essi
corrispondono è il caﬀè. Si descrive ora il comporamento dei due processi in
analisi: per farlo si utilizzerà una sintassi che ricorda quella di CCS:
M = moneta.caf f è
C = moneta.caf f è
A questo punto, si intende far interagire i due processi M e C, costruendo
il processo MC. Si noti che i due processi componenti del processo MC
eseguono azioni duali: si consideri ad esempio l’azione moneta compiuta
da M e l’azione moneta compiuta da C. Queste due azioni sono in grado
di interagire nel processo composto e di produrre un azione non osservabile, privata in quanto frutto dell’interazione delle due entità M e C, avente
sempre come soggetto la moneta. Ciò è detto sincronizzazione. Quindi,
sempre ispirandosi a CCS, il processo MC può essere cosı̀ descritto:
MC = τmoneta .τcaf f è
L’esempio precedente mette in evidenza il fatto che ci sono due aspetti
fondamentali, quando si sta trattando di azioni:
aspetto 1: come un’azione singolarmente si relaziona con il mondo esterno
(ovvero su quale soggetto e come essa opera)
aspetto 2: come due o più azioni possano interagire tra loro tramite la
sincronizzazione.
Questi due aspetti verranno nel seguito discussi separatamente, anche se
essi sono comunque legati tra loro.
28
Modelli per la concorrenza
Analisi di un’azione: Si intende qui dare una deﬁnizione formale di azione.
Partendo dalle intuizioni date dal precendente esempio, un’azione dovrebbe
avere un soggetto ovvero un ambito, un’entità su cui essa agisce e una
polarità ovvero il modo con cui l’azione agisce sul soggetto.
Anzitutto si ha un insieme universo di soggetti di un’azione, denotato
con S. Per quanto concerne invece le polarità, si hanno in tutto tre possibili
modi con cui un’azione si relaziona con il suo soggetto, che sono un input
(denotato con −), un output (denotato con +) e un modo non osservabile
(denotato con ±). L’insieme di tutte le possibili polarità è denotato con Π
ed è il seguente:
Π = {+, −, ±}
Un’azione è dunque cosı̀ deﬁnita:
Deﬁnitione 2.2.8 (azione). Si deﬁnisce azione una coppia α = a, dove
• a ∈ S è il soggetto dell’azione
• ∈ Π è la polarità dell’azione
Nel seguito, al posto della notazione pesante a, , si utilizzerà la notazione a per denotare un’azione. Data un’azione a , si deﬁnisce subj(a ) = a
e π(a ) = .
All’occorrenza, un’azione può implicare un passaggio o un utilizzo di valori: un valore può essere o un tipo di base ovvero un naturale o un booleano
(denotiamo l’insieme dei tipi di base con B), oppure una risorsa ovvero un
soggetto. L’insieme universo di tutti i valori è denotato con V ed è
V=SB
Tenendo conto di ciò, si ha la seguente deﬁnizione di azione con passaggio di
valori, denominata azione estesa:
Deﬁnitione 2.2.9 (azione estesa). Un’azione estesa è una tripla αv =
a, , v dove
• a, è un’azione
• v ∈ V è un valore
Nel seguito, al posto della notazione pesante a, , v, si utilizzerà la notazione a v per denotare un’azione estesa. Data un’azione estesa a v, si
deﬁniscno subj e π nel modo analogo al caso dell’azione semplice. Inoltre si
deﬁnsce val(a v) = v.
Strutture di eventi
Sincronizzazione: Una sincronizzazione è determinata da una interazione
di due azioni di polarità opposta e genera una azione neutra. Essa modella l’interdipendenza di due azioni eseguite dai due sistemi che si vuole far
interagire. Intuitivamente, due azioni polarizzate si possono sincronizzare
se esse operano su uno stesso soggetto, hanno polarità opposta e il risultato della sincronizzazione è un’azione apolare che opera sullo stesso soggetto
delle suddette due azioni.
La provenienza delle azioni che si sincronizzano è anch’essa importante:
esse infatti possono provenire dai due sistemi in parallelo che si stanno
analizzando, ma possono anche provenire dall’ambiente esterno5 .
Tenendo conto di ciò, l’insieme universo delle azioni, denotato con U(A),
è cosı̀ deﬁnito:
U(A) = {a |a ∈ S, ∈ Π} ∪ {}
Le strutture di eventi che si considereranno nel seguito saranno etichettate
in sottoinsiemi di U(A). La costante è un’azione speciale e modella la ‘non
azione’ ovvero serve per modellare il fatto che il processo con cui sto eseguendo in parallelo non risponde ad una determinata azione, non si sincronizza:
ciò singiﬁca che lo fa l’ambiente esterno, dunque è come dire che è l’azione
dell’ambiente esterno. Si noti che nessun evento verrà mai etichettato con .
Per modellare la sincronizzazione, viene deﬁnito un operatore binario
parziale commutativo e associativo su U(A), denotato con •6 e cosı̀ deﬁnito:
• ∀α ∈ U(A) . α • = • α = α
• ∀a ∈ S . a+ • a− = a− • a+ = a±
• indeﬁnito per tutte le altre coppie
Si ha una deﬁnizione analoga anche nel caso delle azioni estese.
Si noti che + e − sono polarità opposte.
Composizione
In questa sezione si intende fornire la deﬁnizione formale di composizione
di strutture di eventi. Un approccio usuale, usato in [VY06] da cui è stata tratta la deﬁnizione seguente, è di deﬁnire la composizione utilizzando
un’operazione di prodotto categoriale, seguita da una restrizione e da un
rietichettaggio.
5
Occorre considerare il fatto che i due sistemi concorrenti non operano in un ambiente
isolato, ma assieme a loro operano in parallelo altri sistemi che potrebbero interagire con
uno o entrambi i sistemi in oggetto
6
in letteratura, la coppia U(A), • è conosciuta come algebra di sincronizzazione
29
30
Modelli per la concorrenza
Il prodotto categoriale corrisponde intuitivamente ad una giustapposizione
delle due strutture di eventi in questione, dalla quale vengono esclusi tutti
gli eventi che non possono interagire tra loro. Il rietichettaggio si occupa di
applicare la sincronizzazione fra le azioni. Ovviamente si devono modellare
anche le azioni dell’ambiente esterno e come esse possano interagire con le
azioni dei due sistemi concorrenti che hanno come modello le strutture di
eventi da mettere in parallelo.
Prodotto categoriale: Siano E1 = E1 , ≤1 , 1 , λ1 ed E2 = E2 , ≤2 , 2
, λ2 due strutture di eventi etichettate in sottoinsiemi di U(A) che non
contengono .
Si aggiunga a ciascun Ei un evento ﬁttizio ei con λ(ei ) = che rappresenta l’occorrenza di un’azione eﬀettuata dall’ambiente esterno (si denota
con Ei l’insieme degli eventi della struttura di eventi Ei con aggiunto l’evento
ﬁttizio ei ).
ottenuto come soluzione iniziale dell’equazione
Si consideri l’insieme E
X = Pf in (X) × E1 × E2 . I suoi elementi hanno la forma (x, e1 , e2 ) con x
Questo permette di deﬁnire induttivamente una nozione di
ﬁnito, x ⊆ E.
7
altezza di un elemento di E.
h(∅, e1 , e2 ) = 0
h(x, e1 , e2 ) = max{h(e)|e ∈ x} + 1
e λ : E → U(A) × U(A) come
Si deﬁnisce E1 × E2 = E, ≤, , λ, con E ⊆ E
segue, per induzione sull’altezza di e ∈ E:
caso base: si ha che (∅, e1 , e2 ) ∈ E se
1. e1 ∈ E1 , e2 ∈ E2 e e1 minimale in E1 e e2 minimale in E2 o
2. e1 ∈ E1 , e2 = e2 e e1 minimale in E1 o
3. e1 = e1 , e2 ∈ E2 e e2 minimale in E2
Gli elementi di altezza 0 non sono confrontabili.
Inﬁne, per il conﬂitto, si ha (∅, e1 , e2 ) (∅, d1, d2 ) se e1 1 d1 o e2 2 d2
passo induttivo: si assuma che tutti gli elementi in E di altezza ≤ n siano
stati deﬁniti e su di essi siano deﬁniti ordine e conﬂitto. Sia (x, e1 , e2 )
un elemento di altezza n+1. Sia y l’insieme degli elementi massimali in
x. Siano y1 = {d1 ∈ E1 |(z, d1 , d2 ) ∈ y} e y2 = {d2 ∈ E2 |(z, d1 , d2 ) ∈ y}
7
Gran parte delle prove che coinvolgeranno il prodotto categoriale di strutture di eventi
saranno per induzione sull’altezza degli elementi
Strutture di eventi
31
le proiezioni di y sulle due componenti. Abbiamo che(x, e1 , e2 ) ∈ E se
x è chiuso verso il basso e senza conﬂitti e inoltre:
1. Si supponga e1 ∈ E1 , e2 = e2 .
parents(e1 )
Allora deve valere che y1 =
2. Si supponga e2 ∈ E2 , e1 = e1 .
parents(e2 )
Allora deve valere che y2 =
3. Si supponga e1 ∈ E1 , e2 ∈ E2 . Allora
• se (z, d1 , d2 ) ∈ y allora d1 ∈ parents(e1 ) o d2 ∈ parents(e2 )
• per ogni d1 ∈ parents(e1 ), esiste un (z, d1 , d2 ) ∈ x
• per ogni d2 ∈ parents(e2 ), esiste un (z, d1 , d2 ) ∈ x
4. Sia x1 = {d1 ∈ E1 |(z, d1 , d2 ) ∈ x} e x2 = {d2 ∈ E2 |(z, d1 , d2 ) ∈ x}.
Allora per nessun d1 ∈ x1 , d1 1 e1 e per nessun d2 ∈ x2 , d2 2 e2 .
L’ordine parziale è esteso con e ≤ (x, e1 , e2 ) se e ∈ x o e = (x, e1 , e2 ).
Si noti che se e < e allora h(e) < h(e ).
Inﬁne, per i conﬂitti si prenda e = (x, e1 , e2 ) e d = (z, d1 , d2) dove o
h(e) = n + 1, o h(d) = n + 1 o entrambi. Allora si ha e d se vale
una delle seguenti:
• e1 1 d1 o e2 2 d2 con e = d
• esiste un e = (x , e1 , e2 ) ∈ x tale che e1 1 d1 o e2 2 d2 e e = d
• esiste un d = (z , d1 , d2) ∈ z tale che d1 1 e1 o d2 2 e2 e e = d
• esiste un e ∈ x , d ∈ z tali che e d
Per quanto concerne l’etichettatura, si ha λ(x, e1 , e2 ) = (λ1 (e1 ), λ2 (e2 )).
Si può dimostrare che questa costruzione è eﬀettivamente un prodotto della categoria delle strutture di eventi. Il punto di vista categoriale è comunque
al di là dello scopo del presente elaborato.
Sul prodotto categoriale di strutture di eventi si ha un lemma abbastanza
importante che è il seguente:
Lemma 2.2.3 (stabilità). Se (x, e1 , e2 ), (x , e1 , e2 ) ∈ E e x = x allora
esiste d ∈ x, d ∈ x tali che d d
La dimostrazione è data in [VY06]
32
Modelli per la concorrenza
Composizione: La composizione parallela di strutture di eventi è deﬁnita
come segue, a partire dal prodotto categoriale:
Deﬁnitione 2.2.10 (composizione). Siano E1 , E2 due strutture di eventi.
Si deﬁnisce
E1 |E2 = ((E1 × E2 ) \ X)[f ]
dove
• X = {(α1 , α2 ) ∈ U(A)2 |α1 • α2 è indeﬁnito}
• f : U(A)2 → U(A) con f (α1 , α2 ) = α1 • α2
Esempio:
b−
b−
d1
a−
a+
e1
E1
b−
d
a−
e2
E2
d
a±
e
e
a+
e
E3
Si consideri la ﬁgura sovrastante: siano E1 , E2 due strutture di eventi
con E1 = {e1 , d1 } ed E2 = {e2 }. I conﬂitti e l’ordine come da ﬁgura, e
λ(e1 ) = a− , λ(d1 ) = b− , λ(e2 ) = a+ . La struttura di eventi E3 = E1 |E2 è cosı̀
deﬁnita:
• E3 = {e := (∅, e1 , ), e := (∅, , e2), e := (∅, e4 , e5 ), d := ({e}, d4 , ), d :=
({e }, d4 , )}
• l’ordine è deﬁnito con e ≤ d, e ≤ d
• i conﬂitti sono e e , e e e tutti quelli ereditati da loro.
L’esempio precedente rende noti alcuni aspetti importanti della composizione parallela. Anzitutto essa modella fedelmente tutte le possibili
evoluzioni dei due sistemi concorrenti le cui strutture di eventi qui sopra
costituiscono il modello: infatti le azioni che coinvolgono il soggetto a eﬀettuate dai due sistemi si possono sincronizzare tra loro, ma è anche possibile
che esse si sincronizzino con azioni dell’ambiente esterno, in quanto a è un
soggetto pubblico. Se si vuole escludere la sincronizzazione sul soggetto da
Discussione
33
parte di azioni dell’ambiente esterno occorre nasconderlo: in questo caso la
composizione diventerebbe:
b−
b−
d
d1
a−
a+
e1
E1
a±
e
e2
E2
E3
Abbiamo dunque
Deﬁnitione 2.2.11 (composizione con occultamento). Sia S ⊆ S. Si
deﬁnisce
(νS)(E1 |E2 ) = (E1 |E2 ) \ LS
con LS = {s |s ∈ S, ∈ {+, −}}.
Un’altro aspetto importante è che la composizione parallela non preserva
la classe delle strutture di eventi senza conﬂitto e senza confusione. L’esempio
ne è un caso importante.
2.3
Discussione
In questo capitolo, dunque, si è data una panoramica delle principali classi di
modelli per la concorrenza utilizzati, concentrandosi in particolare sui modelli
causali e sulle strutture di eventi. Le strutture ad eventi sono una struttura
molto generale e utilizzata per modellare CCS [Win82] e recentemente anche
π-calcolo [VY06, RBM06].
In particolare in questa sezione, ci si è concentrati sulle strutture ad
eventi senza confusione, come riferimento per lo studio del fenomeno del nondeterminismo: le strutture ad eventi senza confusione infatti modellano una
forma di non determinismo che si comporta bene, in quanto ben localizzato
nella struttura.
Si sono studiate inﬁne le dinamiche che avvengono durante la composizione di strutture di eventi, per capire quali proprietà inerenti al nondeterminismo (assenza di confusione) preservasse la composizione: si è concluso che la composizione non preserva la classe delle strutture ad eventi senza conﬂitto e senza confusione, come ha testimoniato l’esempio fatto nella
sezione precedente.
34
Modelli per la concorrenza
Le strutture ad eventi sono uno strumento molto versatile per studiare la
concorrenza e il non determinismo: a conferma di ciò nel prossimo capitolo
si vedrà un formalismo matematico utilizzato per interpretare programmi, in
cui si utilizzano strutture e aspetti similari di quelli qui visti per le strutture
ad eventi.
Le strutture ad eventi non sono solo utilizzate per per lo studio del non
determinismo in concorrenza, ma anche come framework astratto in teoria
dei domini e in numerosi altri campi. Per il lettore interessato il riferimento
principale è [Win87].
Capitolo 3
Semantica dei giochi
Nello studio dei linguaggi di programmazione, lo scopo della semantica è
quello di dare signiﬁcato ai costrutti sintattici del linguaggio in questione.
In particolare vi sono due aspetti importanti che, a questo scopo, vengono
studiati
aspetto operazionale: Si analizza un programma dal punto di vista delle
operazioni che esso esegue su una macchina. Esse vengono usualmente
descritte mediante regole di riduzione.
aspetto denotazionale: Il signiﬁcato di un costrutto è speciﬁcato da oggetti matematici più o meno complessi, ad esempio funzioni di una certa
tipologia o costruzioni particolari (poset, graﬁ, ...). Ciò è fatto per poter studiare i programmi da un livello di astrazione più alto e in modo
indipendente dai linguaggi con cui essi sono stati scritti.
Questi due aspetti danno vita a due stili di semantiche dette appunto semantica operazionale e semantica denotazionale.
Nozione di equivalenza e relazione fra le due semantiche Data una
semantica denotazionale di un programma, un problema importante è valutarne il suo livello di corrispondenza con la semantica operazionale, in
particolare in tema di equivalenza: in semantica operazionale l’equivalenza
di due programmi è deﬁnita in termini delle computazioni che essi fanno
(informalmente due programmi sono operazionalmente equivalenti se quando essi eseguono ‘immersi in un uguale contesto’, si comportano allo stesso
modo) mentre in semantica denotazionale due programmi sono equivalenti se
vengono ‘interpretati’ nello stesso oggetto. Un problema importante e usualmente diﬃcile da risolvere è quello di dire se, data una semantica operazionale
35
36
Semantica dei giochi
e denotazionale di un linguaggio di programmazione, le nozioni di equivalenza operazionale e denotazionale siano equivalenti. Questa proprietà della
semantica denotazionale data è detta full abstraction.
Semantica dei giochi La semantica dei giochi, introdotta da P. Lorenzen con l’appellativo dialogische Logik [Lor60, Lor61] negli anni ’50, è stata
riscoperta recentemente appunto per risolvere questo problema, in particolare per lo studio del linguaggio funzionale PCF, per il quale è stato dato un
modello a giochi fully abstract [Cur06].
In semantica dei giochi la computazione è modellata come un dialogo,
una partita fra due diﬀerenti giocatori che sono
l’opponente , (spesso indicato con O), rappresenta l’ambiente in cui il
programma viene eseguito.
il proponente , o player (spesso indicato con P), rappresenta il programma.
A questo punto, il programma è modellato come un insieme di partite fra
questi due soggetti detto strategia. Questo approccio porta con sè un’importante vantaggio: infatti pur essendo una rappresentazione ad alto livello
di un programma, esso tiene conto, attraverso il concetto di partita, di interazione, di contenuti operazionali che ne riguardano la dinamica, soprattutto
ﬂussi di calcolo e aspetti algoritmici.
La semantica dei giochi è stata applicata anche allo scopo di costrure
modelli per la logica: in questo contesto la partita avviene fra proponente di
una formula (il quale ne sostiene la verità) e un falsiﬁcatore (il quale cerca
appunto di falsiﬁcarla). In particolare essa è stata utilizzata per costruire
modelli per la logica lineare [Gir87] e ad essa è molto legata la ludica [Gir01].
Il presente capitolo intende introdurre la semantica dei giochi, dapprima
descrivendone le applicazioni alla semantica dei linguaggi di programmazione
e poi parlando delle sue applicazioni alla logica lineare e in particolare descrivendo le strategie lineari.
3.1
Introduzione informale alle strategie
Contrariamente ai modelli classici basati sulla teoria dei domini, i modelli a
giochi di programmi non sono modelli di funzioni, ma sono modelli di tracce:
l’intrerpretazione di un programma è dunque l’insieme di tracce di esecuzione
possibili di quel programma in tutti i possibili ambienti.
Una traccia, o partita, non è altro che una sequenza di mosse (una
stringa), in cui ciascuna mossa può essere giocata o dall’opponent (O) o dal
Introduzione informale alle strategie
37
player (P), la sequenza di mosse è alternante (se una mossa è giocata da un
determinato giocatore, la mossa successiva è giocata dall’altro giocatore), la
mossa iniziale è giocata dall’opponent e la sequenza di mosse è di lunghezza
pari. Inoltre tale sequenza di mosse è corredata da puntatori, dove una mossa
ha un puntatore alla mossa precedente che la rende possibile (la relazione di
giustiﬁcazione è data dall’arena, che l’interpretazione di un tipo).
Esempio 1: (tipo bool) Un programma di tipo bool corrisponde o al valore
V (vero) o al valore F (falso)
Vero
Falso
bool
bool
O
q
O
q
P
T
P
F
In questi due esempi, alla domanda dell’opponent di fornire un valore
booleano, il player risponde con il corrispondente valore, a seconda dei casi.
Esempio 2: (tipo bool → bool) Un programma di tipo bool → bool,
richiede un valore booleano in input, esegue il calcolo e fornisce in output il valore booleano calcolato. Nel seguito sono riportate le due tracce
di esecuzione che assieme modellano la funzione booleana NOT
NOT
bool1
O
bool1
bool2
q1
O
bool2
q1
P
q2
P
q2
O
T2
O
F2
P
F1
P
T1
In queste due tracce, si vede che alla domanda dell’opponent di fornire un
valore booleano, che corrisponde al risultato del calcolo (mossa q1 ), il player
38
Semantica dei giochi
risponde domandando il valore in input (mossa q2 ). Se l’opponent risponde
F2 allora il player dà come risultato T1 ; dualmente se l’opponent risponde
T2 allora il player dà come risultato F1 .
Anche la seguente è una traccia di un programma di tipo bool → bool
bool1
O
q1
P
T1
bool2
Essa corrisponde alla funzione costante (quella che ignora il proporio
input e risponde sempre T1 ).
Come si è visto nei due esempi, un programma è modellato da un opportuno insieme di tracce, il quale è detto strategia. Esso è l’oggetto
fondamentale in semantica dei giochi. Nella letteratura solitamente si usa
rappresentare una strategia sotto forma di albero.
Esempio 3: la strategia NOT La strategia NOT, di cui si sono viste
le tracce nell’esempio precedente, è rappresentata sotto forma di albero nel
modo seguente (le mosse circondate da un cerchio sono le mosse Player,
mentre quelle non cerchiate sono le mosse Opponent)
F1
T1
T2
F2
q2
q1
La nozione centrale in semantica dei giochi che coinvolge le strategie
è la nozione di interazione, espressa nell’operazione di composizione di
strategie. Vediamone un esempio:
Modello HO
39
Esempio 4: composizione di strategie Si consideri la strategia che
modella la funzione booleana NOT (bool → bool) e la strategia false (bool).
F1
T1
T2
F2
τ
q2
F2
T1
q2
q1
τ
q1
NOT
FALSE
NOT;
FALSE
Come si vede dalla ﬁgura la strategia composta ha tipo bool e corrisponde
alla strategia true (come ci si aspetterebbe). Si noti il percorso seguito
per costruirla (marcato con delle frecce a linea continua) e in particolare
il fenomeno della sincronizzazione (marcato con dei rettangoli che racchiudono le mosse che si sincronizzano), che avviene fra due mosse delle due
strategie, che sono la stessa ma che vengono giocate da giocatori diversi.
3.2
Modello HO
In questa sezione si formalizzano i concetti espressi nella sezione precedente.
Essa è scritta per completezza.
3.2.1
Arene
Un’arena è una foresta ﬁnita dove i nodi sono chiamati mosse. La polarità
di una mossa è la parità della lunghezza del cammino dalla radice a quella
mossa. Le radici sono di polarità O o −, i loro ﬁgli di polarità P o + e cosı̀
via alternando ﬁno alle foglie. Le radici n degli alberi sono chiamate mosse
iniziali dell’arena e sono denotate con n. Se una mossa m è ﬁglia di una
mossa n, si dice che n giustiﬁca m e si denota con n m.
40
Semantica dei giochi
Costruzione
Le arene sono costruite induttivamente nel modo seguente:
Arena vuota: La foresta vuota è un’arena denotata con .
Arena singoletto: La foresta avente un solo albero con un solo nodo è
denotata con ⊥.
Arena prodotto: Date due arene A e B, l’arena A × B è l’unione digiunta
delle due arene A e B.
Arena freccia: Date due arene A e B, l’arena A → B è ottenuta aggiungendo come ﬁgli di ciascuna radice di B le radici di A
Si osservi che cosı̀ facendo, le polarità delle mosse di B rimarranno
inalterate, mentre le polarità delle mosse di A risulteranno invertite.
Esempio: arene Nel seguito sono raﬃgurate due arene A e B e l’arena
A→B
A
3.2.2
B
A→B
Partite
Deﬁnitione 3.2.1 (sequenza giustiﬁcata). Una sequenza giustiﬁcata sull’arena A è una coppia (s, f ), dove s = n1 n2 . . . nk è una sequenza di mosse
dell’arena A, f : {1, . . . , k} → 0, . . . , k − 1 tale che
1. f (i) < i
2. se f (i) = 0 allora ni è una mossa iniziale dell’arena A
3. se f (i) = j allora nj ni
Si noti che la mossa iniziale di una sequenza puntata è una mossa O.
Modello HO
41
Deﬁnitione 3.2.2 (partita). Una partita sull’arena A è una sequenza puntata sull’arena A in cui la polarità delle mosse è alternata.
L’inisieme delle partite sull’arena A è denotato con PA . Si noti inoltre
che data una partita (s, f ), se i è pari (risp. dispari) allora f (i) è dispari
(risp. pari).
Esempio: partite Sull’arena bool → bool, se s = q1 q2 V2 q2 F2 F1 q1 V1 q1 q2 F2
e
f :1
2
3
4
5
6
7
8
9
10
11
→
→
→
→
→
→
→
→
→
→
→
0
1
2
1
4
1
0
7
0
7
4
Allora (s, f ) è una partita rappresentata da
q1
q2
V2
q2
F2
F1
q1
V1
q2
Sulle sequenze puntate è deﬁnita l’operazione di proiezione. Essa è cosı̀
deﬁnita:
Deﬁnitione 3.2.3 (proiezione). Sia (s, f ) una sequenza puntata sull’arena
A → B (o A × B). Si deﬁnisce s A la sottosequenza puntata ottenuta da s
togliendo tutte le mosse che non appartengono ad A.
3.2.3
Strategie
In questa sottosezione si darà la deﬁnizione formale di strategia. Come già
anticipato, essa consiste di un insieme di partite soddisfacenti determinate
proprietà. Anzitutto esse devono terminare con una mossa P , dunque devono
F2
42
Semantica dei giochi
essere di lunghezza pari. Inoltre, poichè il player rappresenta il programma,
esso, rispondendo ad una determinata mossa dell’opponent che rappresenta
l’ambiente, deve giocare una ben precisa mossa. In altre parole una strategia
descrive il comportamento deterministico del player parametrizzato su
tutte le mosse sconosciute dell’opponent. Formalizzando questo concetto si
ha dunque la seguente
Deﬁnitione 3.2.4 (strategia). Una strategia σ sull’arena A è un’insieme
di partite sull’arena A chiuso per preﬁsso pari, soddisfacente la seguente
proprietà
determinismo se sm, sn ∈ σ allora m = n ed esse puntano alla medesima
mossa
Composizione di strategie
Siano σ : A → B e τ : B → C due strategie. Come dall’esempio riportato nella sottosezione precedente, la strategia che risulta dalla composizione
delle due strategie è il risultato dell’interazione fra le due strategie dove la
sincronizzazione avviene sulle mosse di B. Essa risulta essere il risultato di
due operazioni eseguite in cascata che sono l’interazione e l’hiding (si noti che
vi sono medesime operazioni anche per deﬁnire la composizione di strutture
di eventi). Vediamole in dettaglio: si deﬁnisce
I(A, B, C) = {(s, f )|s A→B ∈ PA→B , s B→C ∈ PB→C , s A→C alternante}
L’operazione di interazione di due strategie σ : A → B e τ : B → C è cosı̀
deﬁnita
στ = {u ∈ I(A, B, C)|u A→B ∈ σ, u B→C ∈ τ }
mentre la composizione è
σ; τ = {u A→C |u ∈ στ }
la quale è ottenuta dall’interazione nascondendo le mosse private in B.
Per quanto concerne la composizione delle strategie, abbiamo le seguenti
Proposizione 3.2.1 (buona deﬁnizione). Siano σ : A → B e τ : B → C
due strategie. Allora σ; τ : A → C è una strategia
Proposizione 3.2.2 (associatività). Siano σ : A → B , τ : B → C ,
ν : C → D tre strategie. Allora
σ; (τ ; ν) = (σ; τ ); ν
Le dimostrazioni di questi asserti sono date in [Lau04, Har05].
Modello HO
43
Strategia identità
Sia A un’arena. Si deﬁnisce idA strategia sull’arena A → A nel modo seguente
idA = {s ∈ PA1 →A2 |∀t preﬁsso di s.t A1 = t A2 }
Rispetto a idA si hanno le seguenti
Proposizione 3.2.3 (buona deﬁnizione). idA : A → A è una strategia
Proposizione 3.2.4 (neutralità). Sia σ : A → B una strategia. Allora
idA ; σ = σ; idB = σ
Le dimostrazioni di questi asserti sono date in [Lau04, Har05].
Innocenza
In questa sottosezione si introdurrà una sottoclasse delle strategie, detta
classe delle strategie innocenti. Intutitivamente una strategia innocente è una
strategia che non dipende dai calcoli intermedi dell’Opponente: nelle partite
di una strategia innocente, le mosse dell’Opponente dipendono solamente
dalle mosse del Proponente giocate immediatamente prima. Si deﬁnisce
pertanto:
Deﬁnitione 3.2.5 (view). Sia s una sequenza puntata sull’arena A. La
view di s, denotata con s è una sottosequenza puntata deﬁnita come segue:
• = • snP = snP
• snO = nO se n è iniziale
• smtno = smn = smn se m giustiﬁca n in smtn
Una strategia si dice innocente se essa contiene solo view: in una view
ogni mossa dell’Opponente deve puntare alla mossa (del proponente) immediatamente precedente. In particolare, una mossa mimimale nell’arena (che
è giocata dall’Opponente) deve essere la prima mossa in una view.
44
Semantica dei giochi
Esempio: la traccia seguente non è innocente in quanto usa più della sua
view per determinare la risposta
(bool
bool)
O
P
bool
q
q
O
q
P
V
O
q
P
F
La classe delle strategie innocenti è inoltre chiusa per composizione [Lau04].
Le strategie innocenti sono molto importanti e sono usate come modello
per molti linguaggi funzionali, in particolare PCF [Cur06].
3.3
Strategie lineari
In questa sezione si introdurranno le strategie lineari ovvero la semantica dei
giochi utilizzata come modello per la logica lineare
Le strategie lineari sono strategie HO (innocenti) senza ripetizioni di
mosse durante l’esecuzione, ma la struttura additiva rende possibile la presenza di copie di mosse (anche se in ‘tracce’ diﬀerenti del sistema). Esse sono
strategie della ludica ([Gir01]), che è un setting astratto per la teoria della
dimostrazione. In ludica giocano un ruolo fondamentale i puntatori (indirizzi, che possono essere visti come nomi) e l’interazione. Essi sono in grado
di catturare la nozione di concorrenza in logica, allo scopo di aprire un ponte
con la teoria della concorrenza.
A questo scopo verrà introdotta una struttura generale, estensione delle
strategie lineari, detta L-net ([FM05]). Essa si presenta come una struttura
versatile, che se portata nel contesto semantica dei giochi, corisponde ad una
strategia, mentre se portata nel contesto ludica, corrisponde ad un disegno.
Come si vedrà nel seguito, le L-net sono rappresentate sotto forma di
d.a.g., quindi sono ordini parziali deﬁniti sulle mosse (azioni).
Strategie lineari
3.3.1
45
L-nets
Azioni (mosse)
Un puntatore (indirizzo) è una sequenza di indici (numeri naturali). Un’azione
(o mossa) è una coppia k = (ξ, I) data da un puntatore ξ e da un insieme
ﬁnito di indici I. Si dice che k usa il puntatore ξ, e che un’azione (ξ, I) genera
i puntatori ξi con i ∈ I. Questa nozione di generazione induce una relazione
d’ordine sulle azioni: in particolare date due azioni k1 = (ξ, I) e k2 = (σ, J)
si deﬁnisce k1 ≤ k2 se ξ è un preﬁsso di σ. Si scriverà k1 k2 se il puntatore
di k2 è stato generato dal puntatore di k1
Un’azione polarizzata è un’azione assieme ad una polarità, positiva (k + )
o negativa (k − ).
Interfacce
Un’interfaccia è una coppia di insiemi ﬁniti disgiunti Ξ, Λ di puntatori,
scritti come un sequente Ξ Λ. Λ è l’insieme dei puntatori positivi (che
daranno vita ad azioni positive), e Ξ l’insieme dei nomi negativi. Si impone
che Ξ sia vuoto oppure un singoletto.
Data un’interfaccia Ξ Λ e un’azione k = (σ, I), essa si dice iniziale se σ
appartiene all’interfaccia. Se σ ∈ Ξ, l’azione è negativa, altrimenti, se σ ∈ Λ,
l’azione è positiva. Siano k1 k2 due azioni: allora k2 ha polarità opposta
rispetto a k1 . Un’azione k è generata dall’interfaccia Ξ Λ se è iniziale
oppure se esiste k ≤ k generata dall’interfaccia.
L-nets
Si ricorda che un d.a.g. G è un grafo orientato senza cicli (orientati). Si
considererà ogni grafo diretto aciclico G senza considerare gli archi transitivi.
Infatti, si è interessati solo alle proprietà degli archi non transitivi. Per questa
ragione, nelle ﬁgure che verranno disegnate si disegnerà soltanto lo scheletro
del grafo.
Dati due nodi c e d si scriverà c ← b se c’è un arco non transitivo da b a
+
c. Si utilizzerà la notazione ← per la chiusura transitiva di ←.
Un nodo n si dice minimale (risp. massimale) se non esiste nessun
nodo a tale che a ← n (risp. n ← a).
+
Dato un nodo n, si denota n
= {n |n ← n} la chiusura verso il basso
di n.
Dato un d.a.g. G, si deﬁnisce in modo diretto un ordine stretto sui nodi
ponendo a <1 b se a ← b. L’ordine parziale ≤ invece si ottiene dalla chiusura
riﬂessiva e transitiva di <1 .
46
Semantica dei giochi
Nel seguito si parlerà di d.a.g. con nodi etichettati con azioni. Quindi, come per gli eventi nelle strutture di eventi, qui i nodi rappresentano
occorrenze di azioni. Si ha dunque la seguente
Deﬁnitione 3.3.1 (L-net). Sia Ξ Λ un’interfaccia. Una L-net D sull’interfaccia Ξ Λ è data da:
Un insieme X di nodi che sono etichettati con azioni polarizzate generate da Ξ Λ. Nel seguito, quando si parlerà di nodo, si farà riferimento
all’azione con la quale quel nodo è etichettato.
Una struttura su X di grafo bipartito diretto aciclico (se k ← k , le
corrispondenti azioni hanno polarità opposta) che soddisfa le condizioni 1-6
sottostanti
1. Lin. Dato un nodo k, tutti gli indirizzi usati in k
sono distinti
2. Giustiﬁcazione. Ogni nodo k è o iniziale o esiste un nodo predecessore
c (il giustiﬁcatore) tale che c k.
3. Innocenza. Se k è negativo e c è suo predecessore immediato allora
ck
4. Positività. Se a è massimale, allora a è positivo.
Si deﬁniscono fratelli due nodi x1 , x2 che hanno lo stesso genitore e usano
lo stesso puntatore, i.e. x1 = (σ, I1 ) e x2 = (σ, I2 ). Si deﬁnisce coppia
additiva una coppia di nodi fratelli negativi. Per innocenza, il genitore di
due nodi fratelli negativi è lo stesso.
5. Coppia additiva. Due nodi fratelli negativi sono distinti (nell’esempio
sopra si ha I1 = I2 )
6. Duplicazione additiva. Dati due nodi fratelli positivi k1 , k2 , esiste una
+
+
coppia additiva w1 , w2 tale che w1 ← k1 e w2 ← k2 .
Regole e conclusioni
Una regola è un insieme massimale di nodi fratelli negativi. Una regola è
unaria se è un singoletto. Quando non è unaria, essa è detta regola additiva.
Una regola i cui nodi sono minimali è detta conclusione.
L-nets come insieme di view
Cosı̀ come per le strategie innocenti (e per i disegni in ludica [Gir01]), una
L-net può essere presentata come un insieme di view. In questo contesto,
una view è un ordine parziale con elemento massimo.
Strategie lineari
47
Deﬁnitione 3.3.2 (view/chronicle). Sia Ξ Λ un’interfaccia e sia C =
C, ≤ un ordine parziale dove C è un’insieme di azioni generate dall’interfaccia Ξ Λ. C è una view se soddisfa:
top element: C ha un elemento massimo
alternanza: deﬁnendo <1 la relazione di predecessore immediato fra elementi di C rispetto a ≤ (a <1 b se a è un massimale dell’insieme
{b |b ≤ b e b = b}), se a <1 b allora essi hanno polarità opposte.
giustiﬁcazione
innocenza
Con un abuso di notazione, data una view C = C, ≤, si scriverà c ∈ C
inteso come c ∈ C. Una view si dice positiva o negativa in base alla polarità
del suo elemento massimo. Si deﬁnisce inoltre sulle view un ordine parziale
come segue: date due view C1 e C2 si deﬁnisce C1 C2 e si dice che C1 è la
restrizione di C2 , se esiste a ∈ C2 tale che C1 = {x ∈ C2 |x ≤ a}.
Deﬁnitione 3.3.3 (strategia). Una strategia σ è un insieme di view soddisfacente le seguenti
chiusura per restrizione: se C2 ∈ σ e C1 C2 allora C1 ∈ σ.
positività: se C è una view massimale rispetto a allora C è positiva.
coppia additiva: deﬁnendo la nozione di view sorelle allo stesso modo dei
nodi fratelli nelle L-nets, ogni view sorella negativa è distinta.
duplicazione additiva: date due view sorelle positive C1 e C2 , esiste una
coppia additiva D1 e D2 tale che D1 C1 e D2 C2
Le deﬁnizioni 3.3.1 e 3.3.3 sono equivalenti. Infatti data una L-net D, si
può costruire il relativo insieme di view
V iew(D) = {n
: n è un nodo di D}
ed è un lavoro di routine dire che V iew(D) è una strategia.
Data invece una strategia σ, è possibile costruire il grafo Graph(σ) dove i
nodi sono le view e vengono etichettati con l’elemento massimo della relativa
+
view e dati due nodi n1 e n2 si ha n1 ← n2 se e solo se n1 n2 . Anche
in questo caso è evidente che Graph(σ) è una L-net (per i dettagli si veda
[FM05]).
48
Semantica dei giochi
Inﬁne deﬁniamo l’operazione di sovrapposizione di L-nets: date due
L-nets D1 e D2 la loro sovrapposizione D1 ∪ D2 è l’unione insiemistica dei
loro insiemi di view.
D1 ∪ D2 = Graph(V iews(D1 ) ∪ V iews(D2 ))
3.3.2
Composizione
In questa sezione si discuterà della normalizzazione di L-net, ovvero la composizione di strategie. Essa è deﬁnita utilizzando una tecnica detta working
by slices, molto comune in ludica, usata soprattutto per la normalizzazione
delle strategie additive [Gir01].
Deﬁnitione 3.3.4 (slice). Una slice S su una L-net D è un sotto-grafo
chiuso verso il basso di D in cui tutte le regole negative sono singoletti ovvero
non ci sono coppie additive
Si noti che, per la condizione duplicazione additiva, tutti gli indirizzi usati
in una slice sono distinti: quindi tutte le azioni sono distinte, pertanto in una
slice vi è una corrispondenza uno-a-uno fra nodi ed azioni, pertanto una slice
può essere identiﬁcata come un ordine parziale sulle sue azioni ; questo è
fondamentale per la deﬁnizione della composizione.
NOTA: una L-net in cui tutte le regole negative sono singoletti è detta
puramente moltiplicativa (ed è una slice).
La tecnica ‘working by slices’
La tecnica ‘working by slice’ è la tecnica che verrà utilizzata per deﬁnire la
composizione di L-net.
La principale diﬃcoltà nel comporre due L-net sta nella gestione degli
additivi e in particolare nel fenomeno della duplicazione additiva (ci sono
due nodi etichettati con la stessa azione).
Nelle L-net puramente moltiplicative, cosı̀ come nelle slice, non è presente
questo fenomeno, pertanto è semplice dare una deﬁnizione di composizione:
ciò che fa la tecnica ‘working by slice’ è di ridurre la composizione delle L-net
generali (additive) alla composizione di L-net puramente moltiplicative e lo
fa nel modo seguente:
1. decomporre le due L-net da comporre in tutte le sue slices
2. per ogni coppia di slices, eﬀettuarne la composizione
3. sovrappore tutti i risultati della fase precedente allo scopo di ottenere
la L-net composta
Strategie lineari
Nel seguito i dettagli.
L-net compatibili: Si possono comporre due L-nets D1 e D2 che hanno
interfacce compatibili, ovvero quando un nome positivo ξ nell’interfaccia di
D1 coincide con il nome negativo nell’interfaccia di D2 , come ad esempio in
Ξ Λ, ξ e ξ ∆. Il nome condiviso σ è detto taglio.
Una rete di tagli è un insieme ﬁnito R = {D1 , . . . , Dn } di L-nets tale
che
1. ogni indirizzo occorre al massimo in due interfacce, una volta come
nome positivo e una volta come nome negativo;
2. il grafo i cui vertici sono le interfacce e i cui archi sono i tagli è connesso
e aciclico
Si deﬁnisce interno un indirizzo che è un sotto-indirizzo di un taglio, visibile
altrimenti. La deﬁnizione si estende alle azioni. L’interfaccia di una rete di
taglio è l’interfaccia indotta dagli indirizzi visibili dell’interfaccia (Ξ Λ, ∆
con riferimento all’esempio sopra). Una rete di taglio la cui interfaccia è il
sequente vuoto (non ci sono azioni visibili) è detta rete di taglio chiusa.
Due interfacce complementari che messe assieme producono un’interfaccia
vuota sono dette opposte ( ξ e ξ sono interfacce opposte).
Una slice di una rete di taglio R è una rete di taglio S ⊆ R tale che
S è una rete di taglio di slices. Data una rete di taglio R = {D1 , . . . , Dn } si
dice slice di R l’insieme {S1 , . . . , Sn } dove Si è una slice di Di .
Si denota con [[R]] la forma normale di R. Si avrà
[[S]]
[[R]] =
S slice di R
Normalizzazione di slices: in questo paragrafo si farà estensivo uso del
fatto che una slice è un ordine parziale sulle azioni. La normalizzazione segue il paradigma standard dell’interazione più occultamento dell’informazione interna.
La deﬁnizione data nel seguito sarà operazionale: dunque verrà deﬁnita
una macchina astratta, che è un’adattamento della macchina LAM [Fag02].
L’interazione tra le L-nets, formante una rete di taglio, è descritta mediante
un multi-gettone che lavora sulla rete di taglio. Questo gettone si muove
verso l’alto visitando le azioni visibili, mentre sulle azioni interne si muove
dall’azione positiva k + verso l’azione negativa corrispondente k − . L’ordine
con cui i nodi sono raggiunti durante l’interazione stabilisce un nuovo ordine
parziale, che al termine sarà quello della forma normale.
49
50
Semantica dei giochi
La procedura è molto simile alla procedura di composizione delle strutture di eventi o delle reti di Petri. Si deﬁniscono parents(k) = {k |k ← k}
i nodi che precedono immediatamente k (le precondizioni di k). Il concetto chiave è che è possibile raggiungere un’azione k solo dopo che sono state
raggiunte tutte le azioni in parents(k): un’azione è abilitata (acceduta) dall’abilitazione di tutte le azioni in parents(k). A causa della struttura di una
L-net, muovere da un’azione positiva a una negativa è ‘asincrono’, mentre
raggiungere un’azione positiva k ha bisogno di una sincronizzazione tra tutti
i nodi negativi in parents(k).
Sia R una rete di taglio di slice. R è l’ordine parziale associato al grafo
(V, E) sulle azioni (non polarizzate) di R ottenuto come segue
• Se k è un’azione visibile di R (positiva o negativa) e parents(k) ⊆ V
allora k ∈ V e k ← k ∈ E per ogni k ∈ parents(k). Si osservi che se
k è iniziale allora k ∈ V .
• Se k + è un’azione interna di R, parents(k) ⊆ V e k − ∈ R, allora k ∈ V
e k ← k per ogni k ∈ parents(k + )
Il grafo (V, E) è un d.a.g. Se R è chiusa, si chiama R una partita. Se
R = {S, I} chiamiamo R = [S I].
La forma normale [R] di R è ottenuta nascondendo
• le azioni interne (corrispondenti a comunicazioni interne)
• le azioni negative che sono massimali (corrispondenti a eventuale spazzatura derivante da comunicazioni fallite)
Proposizione 3.3.1. [R] è una L-net
Dimostrazione. Diretto per induzione sui passi di costruzione eﬀettuati dall’algoritmo
In particolare vale la seguente
Proposizione 3.3.2 (assiciatività). Siano A, B, C slices. Allora
[[A, B], C] = [A, B, C] = [A, [B, C]]
La dimostrazione è data in [FM05].
Da MALL alle L-nets
51
Normalizzazione di L-nets Si è ora in grado di deﬁnire la normalizzazione di L-nets:
Deﬁnitione 3.3.5 (Normalizzazione). Sia R una rete di taglio. Si deﬁnisce
[[R]] come segue
[S]
[[R]] =
S slice di R
˙
Poiche [S] = [[S]], da ora in poi si utilizzerà la notazione [[]].
Per la normalizzazione si hanno gli usuali risultati di buona deﬁnizione e
di associatività, per i quali si fa riferimento a [FM05].
Esempio : nella ﬁgura sottostante si dà un esempio di normalizzazione
di L-net. Si consideri la L-net in alto a sinistra: le azioni (ξ0, I) e (ξ0, J)
formano una coppia additiva. Si pensi ad esse come una componente di una
regola & (vedi sezione successiva) e ad α come una formula dell’environment
che viene duplicata nelle premesse. Si separano le azioni in due slice e si
normalizzano separatamente. Inﬁne si sovrappongono le slice.
α0
α0
ξ0, I ξ0, J
D:
α0
α
α
ξ, {0}
ξ, {0}
τ2
τ1
ξ, {0}
....
τ
MLL normalization
[ S1 ]
ξ0, I
S2
τ2
τ1
α0
α
α
τ
slicing
S1
α0
ξ0, I
τ2
τ1
[ S2 ]
τ
τ2
τ1
ξ0, J
ξ, {0}
τ
superposing
[ S1 ]
3.4
[ S2 ] :
ξ0, I
ξ0, J
ξ, {0}
τ2
τ1
τ
Da M ALL alle L-nets
In questa sezione si considereranno le strategie lineari viste come modello per
la logica lineare. Si introdurrà anzitutto la logica lineare, suddivisa in fram-
52
Semantica dei giochi
mento moltiplicativo, additivo ed esponenziale spiegando le regole di calcolo
dei sequenti standard. Ci si concentrerà poi su MALL, ovvero sul frammento moltiplicativo additivo, introducendo un calcolo, detto calcolo focalizzato,
adatto per costruire un modello a giochi. Inﬁne si darà un’intuizione su ciò
che è il modello a strategie lineari di prove in MALL focalizzato.
3.4.1
Logica lineare
La logica lineare è stata introdotta da Girard in [Gir87]. Essa diﬀerisce
dall’approccio classico soprattutto per il fatto che le ipotesi sono interpretate
come risorse e come tali devono essere utilizzate esattamente una volta nella
prova. Quest’approccio è particolarmente adatto per modellare realtà del
tipo
‘Ho 1 euro, con 1 euro compero i biscotti’
BASE DI CONOSCENZA (K.B.): euro, euro ⇒ biscotti
Un agente logico (basato dunque sui principi della logica proposizionale
[RN05]), eﬀettuando una ask sulla base di conoscenza, sarebbe in grado di
inferire euro∧biscotti, il che non risulta rispondere ai criteri di ragionevolezza
che inferirebbero soltanto biscotti, poichè euro è stato consumato.
Di seguito diamo le regole di calcolo dei sequenti classiche
A, A⊥
Ax
1
1
Γ
⊥
Γ, ⊥
, Γ
Γ, A, B
Γ1 , A Γ2 , B
⊗
Γ1 , Γ2 , A ⊗ B
Γ, A B
Γ, A
Γ, A Γ, B
Γ, B
⊕1
⊕
&
Γ, A & B
Γ, A ⊕ B
Γ, A ⊕ B 2
Γ, A A⊥ , ∆
cut
Γ, ∆
La logica linerare si suddivide in
frammento moltiplicativo: con i connettivi ⊗ e
e le costanti 1 e ⊥
Da MALL alle L-nets
53
congiunzione moltiplicativa (⊗): detta anche tensore
Γ1 , A Γ2 , B
⊗
Γ1 , Γ2 , A ⊗ B
Derivare A ⊗ B signiﬁca dire che si hanno a disposizione simmultaneamente sia la risorsa A che la risorsa B. Per esempio, se si
scrive euro ⊗ euro si intende modellare il fatto che si hanno due
euro. La costante 1 è l’elemento neutro
1
1
A⊗1≡ 1⊗A≡A
e dunque rappresenta l’assenza di una risorsa.
disgiunzione moltiplicativa ( ): detta anche par
Γ, A, B
Γ, A B
Derivare A B signiﬁca dire che si vuole richiedere di consumare
la risorsa A, o la risorsa B o entrambe. Per esempio, se si scrive
biscotti latte si intende dire che si vorrebbe dei biscotti, oppure
del latte oppure entrambi. La costante ⊥ è l’elemento neutro
Γ
⊥
Γ, ⊥
A
⊥≡⊥
A≡A
e dunque rappresenta l’assenza di richiesta.
frammento additivo: con i connettivi & e ⊕ e le costanti e 0.
congiunzione additiva (&):
Γ, A Γ, B
&
Γ, A & B
Il connettivo & esprime una scelta fra più alternative di cui si ha
il controllo: si supponga ad esempio di avere 50 euro e dopo averli
54
Semantica dei giochi
dati ad un cassiere esso ci dica che è possibile scegliere se comperare l’abito rosso o l’abito blu. Quindi abitor & abitob signiﬁca che
sono a disposizione sia l’abito rosso che l’abito blu e che spetta a
noi sceglierne uno dei due. L’elemento neutro è , Γ
&A≡A&≡A
il quale rappresenta l’assenza di alternativa.
disgiunzione additiva (⊕):
Γ, B
Γ, A
⊕
⊕
Γ, A ⊕ B 1 Γ, A ⊕ B 2
Il connettivo ⊕ esprime una scelta fra alternative di cui non si
ha il controllo: riprendendo l’esempio del caso precedente, dal
punto di vista del cassiere vi è una situazione in cui egli verrà
⊥
privato dell’abito blu (abito⊥
b ) o dell’abito rosso (abitor ), ma siamo
noi ad avere la scelta, non lui (dal suo punto di vista dunque
⊥
abito⊥
r ⊕ abitob ). L’elemento neutro è 0
A⊕0≡0⊕A≡A
e rappresenta qualcosa che non deve accadere, ad esempio la distruzione della Terra o l’assimilazione della razza umana da parte
dei Borg [Fra96].
Esiste anche il frammento esponenziale con i connettivi ! e ?, che qui non
sono trattati.
3.4.2
Un calcolo dei sequenti focalizzato per MALL
Focalizzazione
Il calcolo dei sequenti moltiplicativo additivo (MALL) soddisfa una proprietà
chiamata focalizzazione, scoperta da Andreoli [And92]. Una dimostrazione
π di un sequente Γ può essere trasformata in una dimostrazione π f oc dello stesso sequente, ottenuta da π mediante permutazione di regole, soddisfancente una proprietà detta appunto focalizzazione. Essa si basa sulla
distinzione dei connettivi della logica lineare in due famiglie, che sono le
seguenti:
Da MALL alle L-nets
55
• connettivi positivi: ⊗, ⊕, 1, 0
• connettivi negativi: &, , ⊥, Una prova soddisfa la proprietà della focalizzazione se segue le seguenti
discipline:
• una volta che la prova inizia a decomporre una formula applicando una
regola di un certo connettivo, essa continua a farlo ﬁnchè non incontra
un connettivo di polarità opposta oppure un atomo
• se c’è una formula negativa (ovvero il connettivo più esterno è negativo)
nel sequente allora la prova inizia a decomporre da quella.
Una conseguenza della focalizzazione è che data una prova focalizzata, è
possibile vedere un gruppo di connettivi con la stessa polarità come un singolo
connettivo e una cascata di applicazioni di regole riguardanti connettivi con
la stessa polarità, come una singola applicazione. In questo modo, la divisione
di connettivi in positivi e negativi corrisponde perfettamente all’alternanza
Opponent/Player nella Semantica dei Giochi.
Il calcolo
In questa sottosezione deﬁniremo il calcolo utilizzato: esso è tratto da [Fag].
La sintassi delle formule è dunque cosı̀ deﬁnita:
P ::= 0|1| ⊕I∈I (⊗i∈I (Ni ))
N ::= |⊥| &I∈I ( i∈I (Pi ))
Dove Pi e Ni sono rispettivamente formule positive e negative.
Per quanto concerne le regole, si hanno le seguenti:
Assiomi:
A, A⊥
e le regole per le costanti.
regole di inferenza:
∆j , Nj ∀j ∈ J con J ∈ I
(P, N J )
⊕I∈I(⊗i∈I (NiI )), . . . , ∆j , . . . , ∆k , . . .
Dove P = ⊕I∈I(⊗i∈I (Ni )).
P1J , . . . , PnJJ , ∆ ∀J ∈ I con J = {1, . . . , nJ }
&I∈I(
Dove N = &I∈I(
I
i∈I (Pi )), ∆
i∈I (Pi )).
{(N, P J )|J ∈ I}
56
Semantica dei giochi
taglio:
Γ, A A⊥ , ∆
(cut)
Γ, ∆
condizione di polarità: ogni sequente ha al massimo una formula negativa.
Le coppie utilizzate nelle etichette delle regole sono chiamate azioni. Si noti
che presa un’azione, essa ci dà una visione locale esaustiva dicendoci la formula sulla quale in quel momento la prova sta lavorando e le sottoformule su
cui lavorerà nel passo immediatamente successivo. Si noti che all’applicazione
di una regola positiva corrisponde una sola azione, mentre all’applicazione
di una regola negativa corrispono un cluster di azioni operanti sulla stessa
formula (si noti l’analogia con le coppie additive).
3.4.3
Da MALL alle L- nets
Volendo ridurre al minimo l’informazione, si può pensare di non voler lavorare direttamente con le formule, ma ad esempio di immagazzinarle in
una struttura dati indicizzata, alle quali è possibile accedere mediante dei
puntatori.
Si consideri il sequente seguente:
a⊥ ⊗ b⊥ , c
d
Di seguito, si ha la prova in calcolo dei sequenti focalizzato,
a0 , c ⊥ b0 , d ⊥
a
b
a⊥ , c
b⊥ , d ⊥
a ⊗ b⊥
a⊥ ⊗ b⊥ , c, d
c d
a⊥ ⊗ b⊥ , c d
Nel seguito si dà una versione ad albero della prova con indicazione, per ogni
nodo, delle sottoformule, cerchiando le formule positive (ovvero quelle che
hanno un connettivo positivo come connettivo più esterno)
Da MALL alle L-nets
57
c {c0 ⊥ }
d
{d0 ⊥ }
a⊥ {a0 }
b⊥ {b0 }
a⊥ ⊗ b⊥ {a⊥ , b⊥ }
c
{c, d}
d
d, a⊥ ⊗ b⊥
c
A questo punto, si ‘immagazzinano’ le formule in una struttura dati
indicizzata, in questo modo, per poterle associare a dei puntatori
Addresses
c
c
a⊥
d
σ1
d
σ2
σ
b⊥
ξ2
ξ1
a ⊥ ⊗ b⊥
ξ
E ora si considera l’albero e si sostituiscono le formule e le sottoformule
coi relativi puntatori.
σ1
σ2
ξ1
ξ2
ξ
σ
Ora si memorizza in ogni nodo, oltre al puntatore alla formula, anche
l’informazione necessaria a ricavare i puntatori alle sottoformule. Si noti che
per ricavare i puntatori alle sottoformule a partire da un puntatore σ a una
data formula basta solamente concatenare a σ l’indice della sottoformula.
Dunque, per ogni nodo basta memorizzare il puntatore alla formula e l’insieme di indici che genereranno i puntatori alle sottoformule (quindi la coppia
(σ, I), la quale genera i puntatori σi con i ∈ I).
58
Semantica dei giochi
σ1 {0}
σ2 {0}
ξ1 {0}
ξ2 {0}
ξ
{1, 2}
σ {1, 2}
σξ
In ogni caso, una L-net modella un oggetto in teoria della dimostrazione
più astratto della prova in calcolo dei sequenti focalizzato. Questo oggetto è
detto rete di prova. In una rete di prova l’ordine con cui le regole del calcolo
sono applicate è ridotto al minimo. Le reti di prova sono state introdotte
da Girard in [Gir87], ed esse sono adatte a catturare l’idea di concorrenza
all’interno della teoria della dimostrazione.
3.5
Discussione
In questo capitolo, dunque, sono stati introdotti i principali aspetti della
semantica dei giochi. Si è parlato anzitutto di semantica dei giochi HO,
ovvero quella usata per costruire modelli per i linguaggi di programmazione:
si è introdotto il concetto di strategia, la quale è descritta tramite l’insieme di
tutte le tracce possibili della computazione. Poi si è parlato di semantica dei
giochi utilizzata per costruire modelli per la logica lineare, e in particolare si
è parlato di strategie lineari, le quali sono descritte mediante ordini parziali.
Di ambedue le tipologie di strategie, si è discusso anche della composizione
La distinzione strategie a traccia/strategie lineari ricorda molto la distinzione modelli ad interleaving/modelli causali in teoria della concorrenza.
Cosı̀ come vi sono somiglianze nella nozione di interazione: il fenomeno
della sincronizzazione è presente in entrambi gli ambiti (sincronizzazione
fra mosse = sincronizzazione fra azioni). Inoltre il fatto che, in entrambi
gli ambiti la composizione parallela sia un risultato di due sotto-operazioni
(giustapposizione più occultamento) è un’aspetto comune molto importante.
Nei prossimi capitoli si intenderà approfondire maggiormente questo legame,
prendendo in esame le strutture di eventi, in teoria della concorrenza e le Lnets in semantica dei giochi e si vedrà che esse sono strutture molto simili
tra loro. In particolare, si metterà in evidenza la stretta corrispondenza fra
nozione la di conﬂitto e la coppia additiva.
Capitolo 4
Strutture di eventi tipate
Nei primi due capitoli si è data una panoramica di due diﬀerenti aree dell’informatica teorica, che sono la teoria della concorrenza e la semantica dei
giochi. In particolare la discussione si è soﬀermata su due strutture particolari utilizzate, che sono le strutture ad eventi e le L-nets: pur essendo
utilizzate in contesti completamente diﬀerenti, esse sono accomunate dal fatto che possono essere descritte mediante ordini parziali: infatti, cosı̀ come
riportato nella deﬁnizione 2.2.2 una struttura ad eventi etichettata non è altro che un insieme di eventi con un’etichetta su cui è deﬁnita una relazione
d’ordine parziale, mentre una L-net (vedi deﬁnizione 3.3.1) non è altro che
un d.a.g. con nodi etichettati, ovvero un’ordine parziale.
Dunque una costruzione comune (un ordine parziale) è utilizzata per descrivere due diﬀerenti strutture situate in due diﬀerenti aree (struture di
eventi in teoria della conocrrenza e L-nets in semantica dei giochi).
Pertanto, lo scopo di questo capitolo è studiare questa similitudine allo
scopo di approfondire il legame fra strutture di eventi e L-nets per poter
poi costruire una struttura versatile, che se portata nei due ambiti di studio
(teoria della concorrenza e semantica dei giochi), essa possa essere identiﬁcata con le strutture già note. Questa struttura versatile è qui denominata
struttura ad eventi tipata: essa è
• una struttura ad eventi senza confusione
• una generalizzazione delle strategie lineari
In particolare si stabilirà, tramite la nozione di struttura ad eventi tipata,
un legame di stretta similitudine fra le L-nets e le strutture ad eventi senza
confusione, mostrando che le L-nets sono una sotto-classe di queste ultime.
Di conseguenza, il presente capitolo si articolerà come segue: anzitutto si
analizzerà la similitudine fra L-net e strutture di eventi mostrandone il legame
59
60
Strutture di eventi tipate
con le strutture ad eventi senza confusione. Poi, sfruttando tecniche presenti
nelle strategie lineari, si costruirà un typing system per le strutture ad eventi
per garantirne l’assenza di confusione e se ne analizzeranno le proprietà.
Dopo di che, si deﬁnirà una nozione globale di composizione di strutture ad
eventi tipate, per la quale si mostrerà la buona deﬁnizione, ovvero l’assenza
di confusione (la tipatura) è preservata per composizione. Inﬁne si darà una
deﬁnizione equivalente di composizione di strutture ad eventi tipate basata
sulla tecnica ‘working by slice’, largamente utilizzata in semantica dei giochi.
4.1
Strategie come strutture ad eventi senza
confusione
Come si è visto nel capitolo 3, una L-net è una struttura versatile, in grado
di descrivere un disegno se portata nell’ambito ludico e in grado di descrivere
una strategia lineare se portata nell’ambito semantica dei giochi.
Nel capitolo 2, invece sono state introdotte le strutture di eventi (etichettate), descrivendole come strutture generali in grado di modellare sistemi
concorrenti non deterministici. Si è inoltre parlato di una forma di non determinismo localizzata modellata da una particolare sotto-classe di strutture
ad eventi detta classe delle strutture ad eventi senza confusione.1
Come già detto queste due strutture possono essere descritte mediante
ordini parziali (la corrispondenza tra d.a.g. e ordini parziali è ben nota in
letteratura): in questa sezione si intende analizzare meglio questa similarità
allo scopo di stabilire se il legame va ben oltre questo fatto.
Sia dunque D una L-net di interfaccia Ξ Λ. Si costruisca la struttura
ED = ED, ≤D, D, λD cosı̀ deﬁnita:
• ED è dato dall’insieme di nodi X di D
+
• siano n, m ∈ ED: si pone n ≤ m se n ← m.
• si etichetta ciascun nodo con la corrispondente azione k = (ξ, I)
• siano n, m ∈ ED distinti: si pone n m se vale una delle seguenti
1. se n ed m sono una coppia additiva
2. se esistono n ≤ n, m ≤ m tali che m ed n sono coppie additive.
1
Si invita il lettore a rivedere le deﬁnizioni di L-net, strutture di eventi e strutture ad
eventi senza confusione
Strategie come strutture ad eventi senza confusione
La struttura cosı̀ costruita è una struttura ad eventi senza confusione:
infatti per costruzione m µ n se e solo se m ed n sono coppie additive:
inoltre sono mosse negative e per la costrizione di innocenza i genitori sono
gli stessi, per cui anche gli antenati lo sono. Inoltre la relazione di coppia
additiva è ovviamente transitiva, per cui anche la seconda condizione che
caratterizza le strutture ad eventi senza confusione è soddisfatta.
Remark 4.1.1. Si osservi inoltre che il ‘luogo‘ in cui è localizzata la scelta
in una struttura di eventi senza confusione (la cella) ha chiaramente la regola
additiva nelle L-net come sua controparte: infatti se si pensa al signiﬁcato del
connettivo & in logica lineare, il quale esprime la scelta, la cosa non dovrebbe
sorprendere.
Quindi una L-net è una particolare struttura di eventi senza confusione:
tra le innumerevoli proprietà che essa gode, colpisce particolarmente il fatto
che per esse la composizione è ben deﬁnita, cosa che non è aﬀatto vera per
le strutture ad eventi senza confusione.
Esempio: Si considerino le seguenti strutture di eventi senza confusione,
per le quali si stabilisce che il nome privato sia b
E2
E1
a
b
b
c
La loro composizione risulta essere
E1 E2
a
τb
c
che chiaramente non è senza confusione
Il problema di questo controesempio stà nel fatto che le azioni di una cella
non sono uniformi dal punto di vista della visibilità (nell’esempio a è privato
mentre b è pubblico). Una delle peculiarità chiave delle L-nets è che i nodi
di una regola additiva (cella) sono occorrenza di uno stesso nome, dal quale
però può generare successori diversi a seconda del nodo. Dunque l’aspetto
chiave sta nell’identiﬁcare una cella (ovvero un insieme di eventi tra loro in
61
62
Strutture di eventi tipate
conﬂitto immediato e con gli stessi predecessori) con uno stesso nome (per
cui se quel nome venisse dichiarato privato, tutti gli eventi di quella cella
diventerebbero automaticamente privati).
Esempio: Rivisitiamo l’esempio precedente applicando questa intuizione:
si hanno dunque le due strutture di eventi da comporre in cui gli eventi
appartenenti alla stessa cella sono etichettati con lo stesso nome b e dunque
entrambi privati. Quindi la struttura composta è
E1 E2
τb
c
Dunque l’idea è di utilizzare un modo di etichettare le strutture di eventi
senza confusione in cui gli eventi che appartengano ad una stessa cella siano
etichettati con uno stesso nome. Infatti nelle sezioni successive si introdurrà
un sistema di tipi che etichetterà gli eventi in questo modo e si mostrerà
come, cosı̀ facendo, tutte le proprietà delle L-nets che sono importanti per
la buona deﬁnizione della composizione (Lin. e duplicazione additiva), in
questo contesto siano invece derivabili dal sistema di tipi.
4.2
Sistema di etichette
In questa sezione si introdurrà una nozione di struttura di eventi etichettata
con particolari proprietà, le quali garantiscono che la composizione di due
strutture di eventi senza confusione sia senza confusione.
L’etichettaggio utilizzato può essere visto come una variante minimalista
del sistema di tipi in [VY06] senza l’utilizzo di tipi lineari e morﬁsmi; questo
perchè si è interessati nella preservazione dell’assenza di confusione durante
la composizione.
Richiamiamo alcuni concetti e notazione visti in precedenza: nella sezione
2.2.4 è stato descritto il concetto di etichetta. Come già visto, data un’etichetta a , essa rappresenta un’azione2 che ha come soggetto subj(a ) = a e viene
eseguita secondo la modalità dettattata da ∈ {+, −, ±}. Nel seguito verrà
utilizzato il termine azione non polarizzata come sinonimo di soggetto.
L’insieme universo dei soggetti era denotato con S, l’insieme delle polarità
con Π e l’insieme universo delle azioni era denotato con U(A) = {s |s ∈ S, ∈
2
Nel seguito si tratterà il caso di azioni senza passaggio di valori
Sistema di etichette
63
Π} ∪ {} e le strutture di eventi erano etichettate in sottoinsiemi di U(A),
che non contengono .
Nel seguito si intenderà dare maggiore struttura alle etichette, in modo
da costruire insiemi di etichette che godono di determinate proprietà e che
verranno utilizzati per etichettare strutture di eventi. In particolare, per
garantire l’assenza di confusione occorre un etichettaggio che sia in grado
di identiﬁcare le celle della struttura di eventi (in pratica una cella della
struttura di eventi verrà etichettata con un nome).
4.2.1
Soggetti e nomi
Sia N un insieme di nomi avente come elementi α, β, . . . e sia I ⊆ N un
insieme di indici. L’insieme universo di soggetti S è caratterizzato come
segue
S=
Ni = {(α, i)|α ∈ N, i ∈ I}
i∈I
Su S si deﬁnisce una relazione binaria #. Intuitivamente due soggetti s1 , s2
sono in relazione # se hanno lo stesso nome: più formalmente
(α, i)#(β, j) se α = β
Dato a = (α, i) ∈ S si dice che α è il nome di a e si denota name(a) = α.
E’ facile vedere che # è una equivalenza. E’ inoltre ovvio che dato α ∈ N
esso identiﬁca in modo univoco la classe di equivalenza Cα = {(α, i)|i ∈ I}.3
4.2.2
Interfacce
Le strutture di eventi saranno tipate con interfacce: le interfacce forniscono
un insieme di nomi sui quali le strutture di eventi comunicano e la loro
rispettiva polarità. Si ha dunque la seguente
Deﬁnitione 4.2.1 (Interfaccia). Un’interfaccia è una coppia A = A, πA dove
• A ⊆ N è un insieme di nomi
• πA : A → Π è una funzione che fornisce la polarità di un nome
3
Un’appproccio leggermente diﬀerente e comunque equivalente può essere dato dicendo
che su S è deﬁnita un’opportuna relazione di equivalenza # e che i nomi sono le classi
di equivalenza indotte da # (dato un s ∈ S la classe di equivalenza indotta da s è [s] =
{s ∈ S|s#s }). Tenendo conto di ciò, la funzione name, che restituisce il nome dell’azione
diventerebbe la proiezione del soggetto nella sua classe di equivalenza (dunque name(s) =
[s])
64
Strutture di eventi tipate
L’interfaccia vuota è denotata con I = ∅, ∅. Nel seguito, data un’interfaccia A, identiﬁcheremo il suo insieme di nomi con A, ovvero con la
corrispondente lettera in forma maiuscola e la sua funzione di polarità con
πA .
Data un’interfaccia A, l’insieme di soggetti generato da essa è dato da
Subj(A) = {(α, i)|α ∈ A, i ∈ I}, mentre l’insieme di azioni da essa generata
è dato da Acts(A) = {(α, i) |α ∈ A, i ∈ I, = πA (a)}. Si noti due aspetti
importanti rigurado al suddetto insieme di azioni:
• ogni azione che coinvolge un soggetto appare con una singola polarità,
o positiva, o negativa, o neutra.
• le azioni che coinvolgono insiemi di soggetti che sono tra loro in relazione di mutua esclusione (ovvero hanno lo stesso nome) appaiono
con una stessa polarità, o positiva, o negativa, o neutra.
Operazioni con le interfacce
Si deﬁniscono di seguito le seguenti operazioni sulle interfacce:
unione: Siano A, B due interfacce tali per cui A ∩ B = ∅. Si deﬁnisce
A ∪ B = A ∪ B, π dove
πA (s) se s ∈ A
π(s) =
πB (s) altrimenti
In particolare se A = {a} è un singoletto con πA (a) = , si deﬁnisce
a ∪ B = A ∪ B.
dualizzazione: Sia A un’interfaccia tale che per ogni a ∈ A, πA (a) = ±. Si
deﬁnisce A⊥ = A, π dove π(s) = −πA (s)
neutralizzazione: Sia A un’interfaccia. Si deﬁnisce A± = A, π dove
π(s) = ± per ogni s.
4.3
Strutture di eventi tipate
Una struttura di eventi di interfaccia A è una struttura di eventi etichettata
con azioni generate da A. Più formalmente essa è una tripla E, A, λ dove:
• E = E, ≤, è una struttura di eventi
• A = A, πA è un’interfaccia
Strutture di eventi tipate
65
• λ : E → Acts(A) è la funzione di etichettatura
Sia e ∈ E: se λ(e) = (α, i) allora
• si dice che e usa il nome α e si scrive name(e) = α
• si dice che e ha come soggetto (α, i) e si scrive subj(e) = (α, i)
• si dice che e ha polarità e si scrive π(e) = Una struttura di eventi di interfaccia A viene tipata se
• tutti gli eventi nella stessa cella usano lo stesso nome (e hanno la stessa
polarità)
• due eventi che usano lo stesso nome (e hanno la stessa polarità) sono
in conﬂitto
• gli eventi in conﬂitto immediato hanno gli stessi predecessori.
Più formalmente
Deﬁnitione 4.3.1 (struttura di eventi tipata). Una struttura di eventi
E di interfaccia A ha tipo A, e si scrive E : A se soddisfa le seguenti, per
ogni e1 , e2 ∈ E distinti:
1. se e1 µ e2 e subj(e1 ) = (α, i) allora subj(e2 ) = (α, j) con j = i
2. se subj(e1 )#subj(e2 ) allora e1 e2
3. se e1 µ e2 allora parents(e1 ) = parents(e2 )
La condizione di assenza di confusione è già garantita dalle tre proprietà
suddette: abbiamo infatti la seguente:
Proposizione 4.3.1 (assenza di confusione). Sia E : A una struttura di
eventi tipata. Allora E è senza confusione.
Dimostrazione. La condizione di cellularità è diretta conseguenza della proprietà 3. Per quanto riguarda la condizione di transitività, siano e1 , e2 , e3
distinti tali che e1 µ e2 e e2 µ e3 : questo implica subj(e1 )#subj(e2 ) e
subj(e2 )#subj(e3 ) per la proprietà 1 e per transitività di # si ha subj(e1 )#subj(e3 )
e questo signiﬁca per la proprietà 2 che e1 e3 . Se e1 µ e3 si conclude.
Altrimenti, facciamo vedere che non è mai il caso che il conﬂitto e1 e3 sia
ereditato. Se fosse ereditato allora esisterebbero e1 ‘ ≤ e1 , e3 ‘ ≤ e3 tali che
e1 ‘ µ e3 ‘. Senza perdita di generalità si assume e1 ‘ = e1 . Per la proprietà
3 applicata al conﬂitto e1 µ e2 si ha e1 ‘ ≤ e2 e sempre per la proprietà 3
applicata al conﬂitto e2 µ e3 abbiamo e1 ‘ ≤ e3 : contraddizione.
66
Strutture di eventi tipate
Inoltre la polarizzazione è rispettata. Si ha infatti la seguente
Proposizione 4.3.2. Sia E : A una struttura di eventi tipata e siano e1 , e2 ∈
E due eventi distinti tali che e1 µ e2 oppure name(e1 ) = name(e2 ). Allora
π(e1 ) = π(e2 )
Dimostrazione. Se name(e1 ) = name(e2 ), π(e1 ) = π(e2 ) è immediato per
costruzione.
Se e1 µ e2 , per la proprietà 1 si ha name(e1 ) = name(e2 ) e si conclude.
4.3.1
Proprietà dell’etichettaggio
L’etichettaggio di una struttura di eventi tipata garantisce due importanti
proprietà che sono
• l’identiﬁcazione di un evento tramite un insieme di etichette
• la relazione di conﬂitto calcolabile osservando l’etichettaggio
La notazione utilizzata sarà la seguente: data una struttura di eventi E e
un S ⊆ E, si indicherà con
• λ(S) = {λ(s)|s ∈ S}
• subj(S) = {subj(s)|s ∈ S}
Alcuni lemmi utili, che verranno utilizzati nel seguito, sono i seguenti:
Lemma 4.3.1 (iniettività sulle conﬁgurazioni). Sia E : A una struttura
di eventi tipata e sia X ⊂ E una conﬁgurazione. Siano x1 , x2 ∈ X: se
subj(x1 ) = subj(x2 ) allora x1 = x2 .
Dimostrazione. Siano x1 , x2 ∈ X tali che subj(x1 ) = subj(x2 ). Se x1 = x2
allora si è ﬁnito. Se x1 = x2 , poiche subj(x1 )#subj(x2 ), per la proprietà 2,
si ha x1 x2 ma questo non può essere poiché X è una conﬁgurazione.
Si noti qui l’analogia con la nozione di slice in L-net: i nodi che appartengono ad una slice sono etichettati in modo distinto.
Lemma 4.3.2 (stabilità 2). Sia E : A una struttura di eventi tipata. Siano
e1 e2 ∈ E tali che subj(e1 ) = subj(e2 ). Allora esistono e1 ∈ e1 , e2 ∈ e2 tali che e1 µ e2 e subj(e1 ) = subj(e2 ).
Dimostrazione. Poiche e1 e2 , devono esistere e1 ∈ e1 , e2 ∈ e2 tali che
e1 µ e2 . Inoltre per la proprieta 1 si ha subj(e1 )#subj(e2 ) con subj(e1 ) =
subj(e2 ) come si voleva.
Strutture di eventi tipate
Si noti il lemma di stabilità: riformulandolo utilizzando una terminologia
appartenete al dominio L-nets, esso stabilisce che se esistono due nodi distinti
n1 , n2 etichettati con la stessa azione, allora esiste una coppia additiva k1 , k2
+
+
tale che k1 ← n1 e k2 ← n2 , ovvero la condizione duplicazione additiva.
Insiemi di etichette identiﬁcano eventi
Ogni evento e ∈ E è univocamente identiﬁcato dall’insieme di etichette λ e
,
come si evince dalla seguente proposizione:
Proposizione 4.3.3. Sia E : A una struttura di eventi tipata e siano e1 , e2 ∈
E due eventi distinti. Allora subj(e1 ) = subj(e2 ).
Dimostrazione. Siano e1 , e2 ∈ E due eventi distinti. Se e1 e2 allora per il
lemma di compatibilità, e1 ∪ e2 è una conﬁgurazione e si conclude per il
lemma di iniettività sulle conﬁgurazioni. Se e1 e2 , il caso meno semplice è
quando subj(e1 ) = subj(e2 ): in questo caso, per il lemma di stabilità 2 si ha
che esistono e1 ≤ e1 , e2 ≤ e2 tali che subj(e1 ) = subj(e2 ) e e1 µ e2 . Inoltre
subj(e1 ) ∈ subj(e2 ): infatti per 1 si ha subj(e1 )#subj(e2 ) e ciò signiﬁca
(se subj(e1 ) ∈ subj(e2 )) che esiste d ∈ e2 tale che subj(d) = subj(e1 ) ma
in tal caso per la proprietà 2 tale d sarebbe in conﬂitto con e2 ∈ e2 , ma
e2 è una conﬁgurazione e ciò non può valere.
Nel dominio L-net, questa proprietà è presente ed è conseguenza della condizione Lin.. E’ interessante notare che quest’ultima condizione è presente
nelle strutture di eventi tipate: infatti si ha la seguente
Proposizione 4.3.4 (Lin). Sia E : A e sia e ∈ E. Allora i nomi in e
sono utilizzati esattamente una volta.
Dimostrazione. Dal capitolo 2, si sa che e
è una conﬁgurazione. Quindi
si procede per assurdo, per cui esistono e1 , e2 ∈ e
tali che name(e1 ) =
name(e2 ). Ma per la proprietà 2 si ha e1 e2 contro il fatto che e
è una
conﬁgurazione. Contraddizione.
E’ dunque possibile dare una dimostrazione alternativa della proposizione
4.3.3, che deriva direttamente da quella data per le L-nets.
Dimostrazione della proposizione 4.3.3 Si supponga che non sia il caso,
ovvero esistono e1 , e2 tali che subj(e1 ) = subj(e2 ). Allora in particolare
subj(e1 ) = subj(e2 ) e per il lemma di stabilità esistono e1 ≤ e1 , e2 ≤ e2
tali che e1 µ e2 . Allora per l’assunzione di partenza, esiste d1 ∈ e1 con
subj(d1 ) = subj(e2 ), ma ciò viola la proprietà Lin. Contraddizione. 2
67
68
Strutture di eventi tipate
Conﬂitti
La relazione di conﬂitto in strutture di eventi tipate può essere inferita
dall’etichettaggio: si ha infatti la seguente
Proposizione 4.3.5. Sia E : A una struttura di eventi tipata e siano e1 , e2 ∈
E. Allora vale la seguente
e1 e2 ⇐⇒ ∃e1 ≤ e1 , e2 ≤ e2 : name(e1 ) = name(e2 )
(4.1)
Dimostrazione. Si supponga e1 e2 : allora esistono e1 ≤ e1 , e2 ≤ e2 tali
che e1 µ e2 e per la proprietà 1 si ha name(e1 ) = name(e2 ) come si voleva.
Dall’altro lato, siano e1 , e2 tali per cui esistono e1 ≤ e1 , e2 ≤ e2 tali che
name(e1 ) = name(e2 ): allora e1 e2 per la proprietà 2 e per ereditarietà si
conclude e1 e2 come si voleva.
Come conseguenza della proposizione precedente, nelle strutture di eventi
tipate il conﬂitto è deducibile dall’etichettaggio e dunque, da questo momento
in avanti sarà possibile trattare il conﬂitto implicitamente. Quindi
Remark 4.3.1. Data una struttura di eventi tipata E : A e dati e1 , e2 ∈ E
distinti, si può dedurre e1 e2 se e solo se esistono e1 ∈ e1 , e2 ∈ e2 tali
che name(e1 ) = name(e2 )
Inoltre si ha un’altro risultato
Proposizione 4.3.6. Sia E una struttura di eventi etichettata in A tale per
cui valgono la proprietà 3 e 4.1. Allora E : A.
Dimostrazione. Occorre far vedere che valgono 2 e 1.
Per quanto concerne 1, siano e1 µ e2 . Quindi e1 e2 e per 4.1 esistono
e1 ≤ e1 , e2 ≤ e2 tali che name(e1 ) = name(e2 ). Se e1 = e1 ed e2 = e2 allora
si è ﬁnito. Si supponga dunque almeno uno dei due diversi: senza perdita di
generalità e1 = e1 : questo signiﬁca per 4.1 e1 e2 e dunque e1 e2 sarebbe
ereditato, contro l’ipotesi che il conﬂitto fosse immediato.
Per quanto concerne 2, siano e1 , e2 distinti tali che name(e1 ) = name(e2 ).
Ma allora per 4.1 e1 e2 come si voleva
In conclusione si ha il seguente:
Corollario 4.3.1. Sia E una struttura di eventi etichettata in A tale per cui
vale la proprietà 3. E : A se e solo se vale 4.1
Composizione globale
4.4
Composizione globale
In questa sezione verrà deﬁnita la composizione tra due strutture di eventi
tipate. La deﬁnizione è data ‘operazionalmente’ ed è basata sulla deﬁnizione
di composizione di strategie in semantica dei giochi e in particolare sulla
macchina LAM introdotta in [Fag02] e deﬁnita nel capitolo 3.
Tale deﬁnizione può essere vista come una generalizzazione della macchina
suddetta: infatti essa si basa sul fatto che uno o più eventi vengono ‘raggiunti’
(il che signiﬁca che possono essere aggiunti alla struttura che si sta costruendo
e che alla ﬁne del processo diverrà la struttura ad eventi composta) solo
quando i suoi predecessori lo sono (ovvero sono presenti nella struttura che
si sta costruendo) e la costruzione della struttura continua ﬁnchè tutti gli
eventi non saranno ‘raggiunti’ (come si vedrà nel seguito, non è stato usato
il verbo ‘visitare’ in quanto un evento potrebbe essere visitato più di una
volta). Si illustrerà in modo migliore questo concetto nelle successive sezioni.
4.4.1
Deﬁnizione
In questa sezione si deﬁnirà la composizione tra due strutture di eventi tipate.
Siano E1 : A ∪ B ed E2 : B⊥ ∪ C due strutture ad eventi tipate: si deﬁnisce
la struttura ad eventi E1 E2 etichettata in A∪B± ∪C ricorsivamente a partire
dalla struttura vuota come segue:
1. Sia e ∈ Ei tale che name(e) ∈ A (risp. C). Si assuma S ⊆ E
soddisfacente le seguenti
condizione sui genitori subj(S) = subj([e))
condizione sul conﬂitto S è senza conﬂitti4
In questo caso si ha
evento ed etichetta: v ∈ E nouvo evento con λ(v) = λ(e)
ordine: per tutti i vi ∈ S
si pone vi ≤ v
2. Siano e1 ∈ E1 , e2 ∈ E2 tali che subj(e1 ) = subj(e2 ) = b e name(b) ∈ B.
Si assuma S = S1 ∪ S2 con S1 ⊆ E1 e S2 ⊆ E2 (...) soddisfacente le
seguenti
condizione sui genitori subj(S1 ) = subj([e1 )), subj(S2 ) = subj([e2 ))
4
In base alla proprietà 4.1 questo signiﬁca che per ogni s1 , s2 distinti non deve valere
che esistono s1 ∈ s1 , s2 ∈ s2 tali che subj(s1 )#subj(s2 )
69
70
Strutture di eventi tipate
condizione sul conﬂitto S è senza conﬂitti5
In questo caso si ha
evento ed etichetta: v ∈ E nuovo evento con λ(v) = b±
ordine: per tutti i vi ∈ S
si pone vi ≤ v
Come detto in sezioni precedenti, si noti che la relazione di conﬂitto nella
struttura composta è trattata implicitamente in quanto automaticamente
dedotta dall’etichettaggio. Inoltre la struttura è costruita in modo che gli
eventi siano univocamente identifati dalla loro storia etichettatata, come nella
proposizione 4.3.3.
La macchina genera E = E1 E2 passo per passo; ogni volta si aggiunge ad
E un evento v che si riferisce ad (viene da) un evento (o una coppia di eventi
in grado di sincronizzarsi) x in E1 E2 . Si aggiunge v ad E solo se
• l’insieme abilitante di x ha già un’immagine in E
• questa immagine è senza conﬂitto
Per capire la condizione di conﬂitto, si ricordi che eventi in conﬂitto sono
eventi mutualmente esclusivi. Se si ha bisogno che un insieme di precondizioni
accadono assieme, devono stare in una struttura di eventi senza conﬂitti S ⊆
E. Come si vedrà successivamente sarà possibile analizzare e anche calcolare
la composizione di strutture di eventi tipate attraverso la composizione di
strutture di eventi senza conﬂitti (si osservi che se si eﬀettua la composizione
di strutture di eventi senza conﬂitti, la condizione di conﬂitto è vacuamente
soddisfatta).
Esempio di composizione
Si consideri le seguenti strutture di eventi:
• E1 = {e1 , e2 , e3 , e4 } con e1 < e3 , e2 < e4 e e1 µ e2
• E2 = {e5 , e6 } con e5 < e6
e interfacce A = {a+ }, B = {b+ }, C = {c+ }.
Si abbrevierà (a, i) con ai e similmente per b e c.
Si consideri
+
+
• E1 : A ∪ B con λ(e1 ) = a+
1 , λ(e2 ) = a2 , λ(e3 ) = λ(e4 ) = b1 .
5
vedi nota 4
Composizione globale
71
+
• E2 : B⊥ ∪ C con λ(e5 ) = b−
1 , λ(e6 ) = c1
Qui si ha una rappresentazione graﬁca delle due strutture di eventi:
e3
b1
e1
a1
e4
b1
a2
E1
e2
e6
c1
e5
b1
E2
E qui il calcolo della struttura composta passo-passo
E 1 E 2
∅
e1 ∈ E 1
name(λ(e1 )) ∈ A
S =∅
v1
a1
v3
4.4.2
v6
c1
v3
τb
v4
τb
v1
a1
a2
v2
a1
v2
a2
name(λ(v1 ) = name(λ(v2 ))
e3 ∈ E 1 e5 ∈ E 2
λ(e3 ) = λ(e5 ) = b1
S1 = {v1 } S2 = ∅
v5
c1
v3
τb
a1
v1
e6 ∈ E 1
name(λ(e6 )) ∈ C
S = {v3 , v1 }
v3
τb
v4
τb
a2
v2
v4
τb
τb
a1
v1
c1
e6 ∈ E 1
name(λ(e6 )) ∈ C
S = {v2 , v4 }
e2 ∈ E 1
name(λ(e2 )) ∈ A
S =∅
v1
v5
a2
e4 ∈ E 1 e5 ∈ E 2
λ(e4 ) = λ(e5 ) = b1
S1 = {v2 } S2 = ∅
v2
a1
v1
a2
v2
Proprietà della composizione
La composizione di due strutture di eventi tipate è ben deﬁnita, come testimonia il seguente:
Teorema 4.4.1. Siano E1 : A ∪ B ed E2 : B⊥ ∪ C. Allora E1 E2 : A ∪ B± ∪ C.
Dimostrazione. Si osservi che basta dimostrare la proprietà 3, in quanto da
questa e dalla proprietà 4.1 si conclude utilizzando il corollario 4.3.1.
Siano u µ v e siano Su , Sv i due sottoinsiemi ottenuti per aggiungere i
due eventi a E1 E2 . Si noti che [v) = [v) se e solo se Su = Sv . Per costruzione
72
Strutture di eventi tipate
si ha name(u) = name(v) pubblico (name(u) ∈ A o name(u) ∈ C) o privato
(name(u) ∈ B).
caso pubblico: Senza perdita di generalità assumiamo name(u) ∈ A (l’altro caso è duale). Ciò signiﬁca che esistono e, d ∈ E1 tali che subj(Su ) =
subj([e)) e subj(Sv ) = subj([e)). Si ha che e µ d: questo vale (per
la proprietà 2) e questo conﬂitto non può essere ereditato perchè altrimenti anche u v lo sarebbe. Poichè E1 è senza confusione, si ha
subj(Su ) = subj(Sv ) e come conseguenza immediata della proposizione
4.3.3 si ha Su = Sv come si voleva.
caso privato: In questo caso esistono eu , ev ∈ E1 e du , dv ∈ E2 tali che
esistono Seu , Sdu , Sev , Sdv tali che
• Su = Seu ∪ Sdu , Sv = Sev ∪ Sdv
• subj(Seu ) = subj([eu )) , subj(Sdu ) = subj([du )) ,
subj(Sev ) = subj([ev )) , subj(Sdv ) = subj([dv )).
Per considerazione analoghe al caso precedente si ha eu µ ev e du µ
dv e per l’assenza di confusione si ha subj(Seu ) = subj(Sev ) e subj(Sdu ) =
subj(Sdv ) e come conseguenza della proposizione 4.3.3 si conclude Seu =
Sev e Sdu = Sdv che implica Su = Sv come si voleva.
4.5
Composizione senza conﬂitti
In questa sezione si analizzerà la deﬁnizione di composizione nel caso in cui
le strutture di eventi da comporre siano senza conﬂitto. In particolare, si
riformulerà la deﬁnizione di composizione di strutture di eventi, per deﬁnire
la quale verranno date regole di riscrittura di grafo.
Il caso senza conﬂitto è molto importante perchè, utilizzando una tecnica
detta ‘working by slice’ (vedi capitolo 3) è possibile ridurre la composizione
globale di strutture di eventi con conﬂitto alla composizione senza conﬂitto.
4.5.1
Deﬁnizione
Deﬁniamo anzitutto la composizione di strutture di eventi tipate senza conﬂitto. Questo caso è molto semplice e chiaro in quanto le strutture prese in
considerazione sono semplici ordini parziali, tuttavia per le ragioni sovraesposte, merita di essere analizzato a fondo. Un concetto chiave molto importante è il seguente:
Composizione senza conﬂitti
73
Se E : A senza conﬂitto allora tutti gli eventi usano nomi distinti6
In tutta questa sezione si assumerà E1 : A ∪ B ed E2 : B⊥ ∪ C senza
conﬂitti e la loro composizione E1 E2 : A ∪ B± ∪ C anch’essa senza conﬂitti
(si mostra in modo diretto per costruzione).
Istanziando la deﬁnizione di composizione globale al caso senza conﬂitti
si ottiene la macchina LAM deﬁnita nel capitolo 3. Essa può essere descritta
per mezzo di un gettone che visita la struttura ad eventi E1 E2 . Quando un’azione privata è raggiunta, per continuare occorre sincronizzarsi con
l’azione di polarità opposta. Si osservi, che per costruzione vi può essere una
sola di azione sı̀ fatta.
Remark 4.5.1. Si osservi che in E1 E2 ogni evento è etichettato con una
diﬀerente azione polarizzata, quindi è possibile identiﬁcare univocamente un
evento con l’azione polarizzata con cui è etichettato.
La procedura è descritta come segue:
1. Se a ∈ A o a ∈ C e i suoi predecessori sono stati abilitati, allora a è
abilitato. Si illustra ciò nella ﬁgura qui in basso in cui nodi quadrettati
denotano azioni abilitate.
→
a
a
2. se a ∈ B, a+ e a− sono entrambe presenti e i loro genitori abilitati,
allora a è abilitato e il grafo è trasformato come segue
a
a
→
τa
end. I nodi che non sono abilitati si cancellano (garbage collection).
Il procedimento descritto sopra genera una nuova struttura di eventi senza conﬂitti (E, ≤) dove E è un insieme di eventi etichettato con etichette
generate dall’interfaccia A ∪ B⊥ ∪ C e con azioni che sono state abilitate.
6
Si osservi che questo fatto è una conseguenza del lemma di iniettività delle
conﬁgurazioni
74
Strutture di eventi tipate
Regole di riscrittura locali
La procedura descritta nella sezione precedente può essere riscritta mediante
regole di riscrittura di grafo locali, come illustrato nel seguito
Private a:
1. There are a, a, parallel
→
a
a
τa
2. Otherwise:
→
a
Proposizione 4.5.1 (Church-Rosser). Sia G = (V, E) un grafo generato
da un passo intermedio della procedura sopra illustrata. Si supponga G → G1
e G → G2 . Allora esiste G3 tale che G1 → G3 e G2 → G3 .
Dimostrazione. Si procede per casi: quello più problematico è il seguente
a e b privati
G
a
b
a
regola 1 su a
regola 2 su b
G2
τa
G1
regola 2 su b
b
Ma in questo caso basta prendere G3 = G1 e chiaramente G2 → G1
applicando la regola (2.)
Composizione senza conﬂitti
Si osservi che a questo punto l’associatività discende come corollario:
infatti date E1 : A ∪ B, E2 : B⊥ ∪ C1 ∪ C2 , E3 : C⊥
2 ∪ D , si ha
(E1 E2)E3 = E1 E2E3
Infatti al primo membro si fa anzittto E1 E2 e poi si eseguono le regole
di riscrittura di grafo e poi si fa (E1 E2 ) E3 e si eseguono le regole di
riscrittura di grafo. Ma ciò posso simularlo anche in E1 E2 E3 : difatti a
partire da E1 E2 E3 eseguo le regole di riscrittura di grafo nel medesimo
ordine che ho seguito per calcolare E1 E2 e poi faccio lo stesso per termiare
il calcolo: la conﬂuenza garantisce l’unicità di E1 E2 E3 qualunque ordine io
prenda. Analogamente dimostro
E1 (E2E3 ) = E1 E2E3
Quindi ho
Corollario 4.5.1 (associatività). Se E1 : A ∪ B, E2 : B⊥ ∪ C1 ∪ C2 , E3 :
C⊥
2 ∪ D, sono tre strutture ad eventi senza conﬂitti allora
(E1 E2 )E3 = E1 E2 E3 = E1 (E2 E3 )
4.5.2
Lavorare con le slice
Cosı̀ come per la composizione delle L-nets, è possibile applicare la tecnica
‘working by slice’ per deﬁnire la composizione di strutture di eventi e far
vedere che tale deﬁnizione è equivalente a quella globale data sopra. Lo
scopo principale di tale operazione è quello di provare l’associatività della
composizione, che è facile da mostrare slice per slice (corollario 4.5.1). In
questa sezione non verranno dati i dettagli per applicare questa tecnica, che
sono descritti nel capitolo 3, ma ne verrà descritta la procedura generale allo
scopo di convincere il lettore della validità della tecnica.
Una struttura di eventi senza confusione E può essere vista come una
sovrapposizione di strutture di eventi senza conﬂitto, ovvero una sovrapposizione di slice. Una slice S di E è un sottoinsieme chiuso verso il basso di
E, con l’ordine indotto da E. La tecnica di riduzione consta di tre passi:
• scomporre E = Ei nelle sue slice (Ei sono le strutture ad eventi da
comporre)
• comporre a due a due le slices ottenute
• sovrapporre le slice composte cosı̀ ottenute
75
76
Strutture di eventi tipate
La proposizione 4.3.3 gioca un ruolo chiave, soprattutto per quanto concerne
la sovrapposizione, in quanto permette di utilizzare le stesse tecniche usate
in [Gir01, FM05].
L’equivalenza della deﬁnizione di composizione cosı̀ ottenuta con la composizione globale sta nel fatto che la composizione globale è di fatto una
‘composizione per slice intelligente’: essa infatti è in grado di unire il passo
2 con il passo 3 eﬀettuando la composizione classica LAM assieme con la
duplicazione additiva, cosa che nella composizione per slice viene fatto solo
nel passo 3.
Si consideri ad esempio le due strutture di eventi raﬃgurate nella ﬁgura
sottostante: vi sono due struture di eventi E1 ed E2 costruite in questo modo
• E1 è composta da tre sottostrutture senza conﬂitto S1 , S2 eS3 e si ha che
S1 è collegata a S2 e S3 da due nodi in conﬂitto.
• E2 è composta da un un’unica sottostruttura senza conﬂitto S4
E1
E2
S2
S3
S4
S1
E ora si confrontano le due procedure di composizione (per slice e globale)
in questa ﬁgura, in cui si ha V1 , V2 , V3 , V4 sottostrutture senza conﬂitto della
struttura composta. Inoltre si assume che i due nodi in conﬂitto immediato
contengano azioni pubbliche.
Discussione
77
Composizione per slice
E1
E2
S2
Composizione globale
S3
S4
S1
passi macchiina astratta
slicing
S3
S2
V1
S4
S4
S1
S1
V1
V2
composizione
slice per slice
V1
V3
V2
V1
V2
V1
V1
unione
ultimo passo
V2
V3
V1
E1 E2
4.6
Discussione
In questo capitolo, dunque, si sono descritte le strutture ad eventi senza
confusione come strutture generali e versatili, di cui le L-net ne sono un caso
particolare. E’ stato deﬁnito un typing system per le strutture ad eventi senza
confusione e si sono descritte le loro principali proprietà. Inoltre si è deﬁnita
78
Strutture di eventi tipate
una nozione di composizione che è una generalizzazione della deﬁnizione di
composizione di L-net.
Quindi di fatto in questo capitolo si sono fornite alle strutture di eventi
senza confusione tecnologie provenienti dalla semantica dei giochi, in particolare per quel che riguarda la composizione. La composizione di strutture
ad eventi senza confusione qui deﬁnita, se portata nel contesto semantica dei
giochi, è la composizione di L-net.
Rimane da controllare che la composizione cosı̀ deﬁnita sia eﬀettivamente
la composizione di strutture ad eventi senza confusione deﬁnita nel capitolo
2. Questo risultato, che è molto importante in quanto completa l’opera di
ediﬁcazione del ponte fra semantica dei giochi e teoria della concorrenza, è
dato nel capitolo successivo.
Capitolo 5
Risultati di equivalenza
In questa sezione si intende dimostrare l’equivalenza della composizione di
strtture di eventi tipate illustrata nel capitolo 4 con la composizione di strutture di strutture di eventi vista nel capitolo 2, in particolare la composizione
con occultamento, dove i soggetti che sono dichiarati nascosti sono quelli
generati dai nomi comuni dichiarati nelle interfacce.
L’equivalenza è stabilita mostrando l’isomorﬁsmo fra le due strutture,
ovvero mostrando che esiste una funzione biettiva che preserva e riﬂette
ordine e conﬂitti: più formalmente, si ha il seguente risultato.
Teorema 5.0.1. Siano E1 : A∪B , E2 : B⊥ ∪C due strutture di eventi tipate.
Allora
E1 E2 ! (ν Subj(B))E1 |E2
La dimostrazione dell’asserto è data nel seguito ed è molto articolata,
data la natura diﬀerente delle due deﬁnizioni in gioco. Essa è strutturata nel
modo seguente:
• verrà rianalizzata la deﬁnizione di composizione con hiding di strutture
di eventi senza confusione, riformulandola in un modo ‘più costruttutivo’
• verrà data una deﬁnizione di composizone di strutture di eventi tipate
che è uno step intermedio fra le due deﬁnizioni in gioco.
• verrà dimostrato l’isomorﬁsmo della deﬁnizione intermedia con la composizione con hiding di strutture di eventi.
• verrà dimostrata l’uguaglianza della deﬁnizione intermedia con la composizone di struture di eventi tipate.
79
80
Risultati di equivalenza
5.1
Composizione con hiding
Siano E1 : A ∪ B, E2 : B⊥ ∪ C due strutture di eventi tipate. Allo scopo
di costruire (ν Subj(B))E1|E2 , occorre costruire il prodotto categoriale e poi
eﬀettuare delle restrizioni in base alle sincronizzazioni e alla speciﬁca delle
azioni nascoste. Questa visione però è abbastanza limitante nel caso in cui
occorra studiare nel dettaglio la struttura di eventi composta. Anzitutto
occorre capire esattamente quali eventi del prodotto categoriale restano nella
struttura composta.
A questo scopo, date due strutture ad eventi tipate E1 : A ∪ B ed E2 :
B⊥ ∪ C , si deﬁnisce la struttura ad eventi Comp(E1 , E2 ) ⊆ E1 × E2 , dove per
ogni e ∈ Comp(E1 , E2 )
• se e ≡ (x, e1 , ) allora name(e1 ) ∈ A.
• se e ≡ (x, , e2 ) allora name(e2 ) ∈ C.
• se e ≡ (x, e1 , e2 ) allora subj(e1 ) = subj(e2 ) con name(e1 ) ∈ B.
Si ha la seguente:
Proposizione 5.1.1. Siano E1 : A ∪B ed E2 : B⊥ ∪C due strutture ad eventi
tipate. Allora (ν Subj(B))E1 |E2 = Comp(E1 , E2)
Dimostrazione. Per dimostrare l’asserto basta far vedere che l’insieme degli
eventi delle due strutture sono uguali, in quanto entrambi sono sottostrutture
del prodotto categoriale.
Siano dunque EComp(E1 ,E2 ) ed E(ν Subj(B))E1 |E2 gli insiemi di eventi delle
rispettive strutture di eventi. Si dimostra la doppia inclusione:
EComp(E1 ,E2 ) ⊆ E(ν Subj(B))E1 |E2 : Sia (x, e1 , e2 ) ∈ EComp(E1 ,E2 ) : esso appartiene
a E(ν Subj(B))E1 |E2 in quanto per costruzione, la coppia (e1 , e2 ) è in grado
di sincronizzarsi (anche nel caso e1 , e2 = si ha name(x, e1 , e2 ) ∈ B ma
la polarità dell’azione associata è per costruzione ±). Inoltre sempre
per costruzione non vi è nessun (x, e1 , ) o (x, , e2 ) con name(ei ) ∈ B
e dunque anche nessun evento al di sopra di un evento sı̀ fatto, e quindi
si conclude.
E(ν Subj(B))E1 |E2 ⊆ EComp(E1 ,E2 ) : Sia e ∈ E(ν Subj(B))E1 |E2 : si hanno tre casi
• e ≡ (x, e1 , ): in questo caso si ha subj(x, e1 , ) ∈ Subj(B) per
costruzione e poiche e1 appare nella prima componente deve essere
subj(x, e1 , ) ∈ Subj(A), il che implica name(e1 ) ∈ A come si
voleva.
Composizione con hiding
• e ≡ (x, , e2 ): duale al caso precendente.
• e ≡ (x, e1 , e2 ): in questo caso si ha subj(x, e1 , e2 ) ∈ Subj(B)
con polarità dell’azione neutra (±). Ciò puo accadere solo se
subj(e1 ) = subj(e2 ) e π(e1 ) = −π(e2 ) che è ciò che si voleva
E’ utile tuttavia avere una deﬁnizione più strutturata di Comp(E1 , E2 ),
la quale è derivata direttamente dalla procedura di costruzione del prodotto categoriale, allo scopo di sfruttare la nozione di induzione sull’altezza
dell’elemento.
Date E1 = E1 , ≤1 , 1, λ1 : A ∪ B ed E2 = E2 , ≤2 , 2 , λ2 : B⊥ ∪ C,
ottenuto come soluzione iniziale dell’equazione X =
si consideri l’insieme E
Pf in (X) × E1 × E2 . I suoi elementi hanno la forma (x, e1 , e2 ) con x ﬁnito,
nel modo
Si deﬁnisce Comp(E1 , E2 ) = E, ≤, , λ con E ⊆ E
x ⊆ E.
seguente per induzione sull’altezza di e ∈ E:
caso base:
1. (∅, e1 , ∗) ∈ E se name(e1 ) ∈ A e minimale in E1
2. (∅, ∗, e2) ∈ E se name(e2 ) ∈ C è minimale in E2
3. (∅, e1 , e2 ) ∈ E se e1 , e2 sono minimali, con name(e1 ) = name(e2 ) ∈
B e tali che subj(e1 ) = subj(e2 )
Gli elementi di altezza 0 non sono confrontabili.
Inﬁne, per il conﬂitto, si ha (∅, e1 , e2 ) (∅, d1 , d2 ) se e1 1 d1 o e2 2 d2
passo induttivo: Assumendo che tutti gli elementi di altezza ≤ n siano
stati deﬁniti, sia (x, e1 , e1 ) di altezza n+1. Sia y l’insieme degli elementi
massimali di x e siano y1 = {d1 ∈ E1 |(x, d1 , d2 ) ∈ y} e y2 = {d2 ∈
E2 |(x, d1, d2 ) ∈ y}. Si ha che (x, e1 , e2 ) ∈ E se x è chiuso verso il basso
e (privo di conﬂitti) e
1. si supponga e1 ∈ E1 e e2 ≡ ∗: allora name(e1 ) ∈ A e y1 =
parents(e1 )
2. si supponga e2 ∈ E2 e e1 ≡ ∗: allora name(e2 ) ∈ C e y2 =
parents(e2 )
3. si supponga e1 ∈ E1 e e2 ∈ E2 : allora:
(a)
(b)
(c)
(d)
name(e1 ) = name(e2 ) ∈ B e tali per cui subj(e1 ) = subj(e2 )
se (z, d1 , d2 ) ∈ y allora d1 ∈ parents(e1 ) o d2 ∈ parents(e2 )
per ogni d1 ∈ parents(e1 ), esiste (z, d1 , d2 ) ∈ x
per ogni d2 ∈ parents(e2 ), esiste (z, d1 , d2 ) ∈ x
81
82
Risultati di equivalenza
4. Siano x1 = {d1 ∈ E1 |(z, d1 , d2 ) ∈ x} e x2 = {d2 ∈ E2 |(z, d1 , d2 ) ∈
x}. Allora per nessun d1 ∈ x1 e d2 ∈ x2 ho che d1 e1 o d2 e2
L’ordine parziale è esteso con e ≤ (x, e1 , e2 ) se e ∈ x o e = (x, e1 , e2 ).
Si noti che se e < e allora h(e) < h(e ).
Inﬁne, per i conﬂitti si prenda e = (x, e1 , e2 ) e d = (z, d1 , d2 ) dove o
h(e) = n + 1, o h(d) = n + 1 o entrambi. Allora si ha e d se vale
una delle seguenti:
• e1 1 d1 o e2 2 d2 con e = d
• esiste un e = (x , e1 , e2 ) ∈ x tale che e1 1 d1 o e2 2 d2 e e = d
• esiste un d = (z , d1, d2 ) ∈ z tale che d1 1 e1 o d2 2 e2 e e = d
• esiste un e ∈ x , d ∈ z tali che e d
Tenendo conto del fatto che, per la proposizione 4.3.1, E1 ed E2 sono
strutture di eventi senza confusione, la condizione 4 è ridondante: infatti
non è mai il caso che esista d1 ∈ x1 tale che d1 e1 e lo stesso per x2 ;
si supponga infatti che sia il caso, ovvero che esista d1 ∈ x1 tale d1 e1 :
allora, a causa della chiusura verso il basso di x e per il fatto che µ è
cellulare, non si può avere d1 µ e1 , quindi il conﬂitto non è immediato
ma è ereditato da un altro conﬂitto. Quindi esistono d1 ∈ d1 , e1 ∈ e1 tali che
e1 µ d1 . Senza perdita di generalità si assume e1 = e1 . Dunque
e1 ∈ h1 ∈parents(e1 ) h1 ⊆ x1 ; si noti anche che d1 ⊆ x1 . Questo signiﬁca
che ci sono due elementi in x1 che sono in conﬂitto, ma questo contraddice il
fatto che x1 sia senza conﬂitto.
5.2
Composizione di strutture di eventi tipate
In questa sezione si fornirà una deﬁnizione di composizione che costituisce
un passo intermedio fra le due deﬁnizioni sulle quali si vuole dimostrare
l’equivalenza. Tale composizione, date due strutture di eventi tipate, fornisce
una coppia dove la prima componente è la struttura di eventi composta,
mentre la seconda componente è una funzione di etichettatura che assegna a
ciascun evento della struttura di eventi composta gli eventi delle strutture di
eventi di partenza dai cui quell’evento ‘proviene’.
Più formalmente, date due strutture di eventi tipate E1 = E1 , ≤1 , 1
, λ1 : A∪B ed E2 = E2 , ≤2 , 2 , λ2 : B⊥ ∪C si deﬁnisce Int(E1 , E2 ) = E, ϕ
dove E = E, ≤, , λ è una struttura di eventi e ϕ : E → (E1 + {e1 }) ×
(E2 + {e2 }) è una funzione di etichettatura.
Si introdurrà qui la notazione nel seguito utilizzata:
Composizione di strutture di eventi tipate
83
• Dato e ∈ E tale che πi (ϕ(e)) = ei 1 , si deﬁnisce e Ei = πi (ϕ(e)).
• Dato S ⊆ E, tale che per ogni s ∈ S, s Ei è deﬁnito, si deﬁnisce
S Ei = {s Ei |s ∈ S}.
La struttura composta è deﬁnita ricorsivamente nel seguente modo:
1. Sia e ∈ Ei tale che name(e) ∈ A (risp C). Si assuma S ⊆ E soddisfacente le seguenti proprietà:
condizione etichettata sui genitori: S Ei = parents(ei )
condizione etichettate sui conﬂitti: S è un insieme senza conﬂitti
In questo caso si ha
evento: v ∈ E nuovo evento con λ(v) = λ(ei ) e ϕ(v) =
(e, e2 ) se i = 1
(e1 , e) se i = 2
ordine: per tutti i vi ∈ S
si pone vi ≤ v
conﬂitti: • per tutti i d ∈ E tali che d Ei ei si pone d v
• per tutti i d1 d2 con d1 ≤ v, si pone v d2
2. Siano e1 ∈ E1 , e2 ∈ E2 tali che name(e1 ), name(e2 ) ∈ B e subj(e1 ) =
subj(e2 ) = b. Sia S = S1 ∪ S2 ⊆ E soddisfacente le seguenti
condizione etichettata sui genitori: S1 E1 = parents(e1 ) e S2 E2 =
parents(e2 ).
condizione etichettata sui conﬂitti: S è un insieme senza conﬂitti.
In questo caso si ha:
evento: v ∈ E nuovo evento con λ(v) = b± e ϕ(v) = (e1 , e2 )
ordine: per ogni vi ∈ S
si pone vi ≤ v
conﬂitti: • per ogni d ∈ E tale che d E1 1 e1 o d E2 2 e2 si pone
vd
• per tutti i d1 d2 con d1 ≤ v, si pone v d2
Un lemma importante sulla composizione cosı̀ deﬁnita è il seguente:
Lemma 5.2.1 (stabilità). Siano u, v ∈ E distinti tali che ϕ(u) = ϕ(v).
Allora esistono u ∈ u
, v ∈ v
tali che u v e ϕ(u ) = ϕ(v )
1
Qui si usa π come funzione di proiezione nelle coppie
84
Risultati di equivalenza
Dimostrazione. Il lemma si dimostra per induzione sulla grandezza congiunta
di u
, v
. Il caso base è vacuamente vero. Siano u = v con ϕ(u) = ϕ(v) =
(e1 , e2 ). Poichè u
e v
sono insiemi chiusi verso il basso, essi coincidono
se e solo se l’insieme degli elementi massimali coincidono (si denota con yu
e yv i rispettivi insiemi di elementi massimanli). Dunque esiste u ∈ yu con
ϕ(u) = (d1 , d2 ) tale che u ∈ yv . Per la condizione sui genitori etichettati e
senza perdita di genralità si può assumere d1 ∈ parents(e1 ). Quindi sempre
per la condizione sui genitori etichettati esiste v ∈ v
con ϕ(v ) = (d1 , d2 ).
Se d2 = d2 allora sono proprio u e v gli eventi cercati e si noti che u v . Altrimenti si applica l’ipotesi induttiva a u ⊂ u
e v ⊂ v
e si
conclude.
Dato S ⊆ E, si deﬁnisce ϕ(S) = {ϕ(s)|s ∈ S}. Un’ulteriore lemma
importante è inoltre il seguente:
Lemma 5.2.2 (iniettività sulle conﬁugurazioni). Sia S ⊆ E un insieme
senza conﬂitto e siano s, s ∈ S tali che ϕ(s) = ϕ(s). Allora s = s
Dimostrazione. Siano s, s ∈ S con ϕ(s) = ϕ(s). Si supponga per assurdo
s = s . Ma allora per la condizione sui conﬂitti si ha s s contro l’ipotesi
che S sia senza conﬂitti.
Dati i due lemmi precedenti, è possibile ricavare un risultato analogo
rispetto a quello esposto nella sezione 4.3.1: si ha dunque il seguente
Corollario 5.2.1. Siano e, e ∈ E distinti. Allora ϕ(e
) = ϕ(e ).
5.3
Risultato di isomorﬁsmo
In questa sezione si mostrerà che la struttura di eventi composta precedente
è isomorfa alla struttura deﬁnita nella prima sezione. Per non appesantire la notazione, nel seguito non si distinguerà più l’ordine,il conﬂitto e
l’etichettatura di diverse strutture di eventi e si utilizzerà sempre la medesima
notazione che è ripsettivamente ≤, e λ.
Proposizione 5.3.1 (isomorﬁsmo). Siano E1 : A ∪ B ed E2 : B⊥ ∪ C due
strutture di eventi tipate. Siano Comp(E1 , E2 ) la struttura ad eventi composta ottenuta dalla deﬁnizione in sezione 5.1. Sia Int(E1 , E2 ) la struttura ad
eventi composta con la funzione di etichettatura ϕ ottenuta dalla deﬁnizione
in sezione 5.2. Allora esiste una funzione biettiva f : Comp(E1 , E2 ) →
Int(E1 , E2 ) soddisfacente le seguenti proprietà:
Risultato di isomorﬁsmo
riﬂessione e preservazione dell’ordine:
∀e, e ∈ Comp(E1 , E2), e ≤ e ⇐⇒ f (e) ≤ f (e )
riﬂessione e preservazione dei conﬂitti:
∀e, e ∈ Comp(E1 , E2), e e ⇐⇒ f (e) f (e )
preservazione dell’etichettaggio:
∀e ∈ Comp(E1 , E2), λ(e) = λ(f (e))
Dimostrazione. Si deﬁnisce f : Comp(E1 , E2 ) → Int(E1 , E2) per induzione
sull’altezza di e ∈ Comp(E1 , E2 )
caso base:
f (∅, e1 , e2 ) = v ∈ Int(E1 , E2 ) : ϕ(v) = (e1 , e2 )
passo induttivo:
f (X, e1 , e2 ) = v ∈ Int(E1 , E2 ) : ϕ(v) = (e1 , e2 ) e
{f (x)|x ∈ X} ∪ {v} = v
Per dimostrare l’isomorﬁsmo, f deve essere ben deﬁnita, iniettiva, suriettiva
e devono valere le tre condizioni suddette.
buona deﬁnizione: Sia e ∈ Comp(E1 , E2 ). Si mostrerà f (e) ∈ Int(E1 , E2 )
per induzione sull’altezza di e.
caso h = 0: Posti e1 ∈ E1 , e2 ∈ E2 , si hanno i seguenti casi
• e ≡ (∅, e1 , e2 ): allora si ha name(e1 ) ∈ A e parents(e1 ) =
∅ e dunque applicando il caso 1 della procedura esiste v ∈
Int(E1 , E2 ) con ϕ(v) = (e1 , e2 ). Tale v è unico per il corollario
5.2.1 e dunque si ha f (∅, e1, e2 ) = v
• e ≡ (∅, e1 , e2 ): simmetrico al precedente.
• e ≡ (∅, e1 , e2 ): allora si ha name(e1 ), name(e2 ) ∈ B, subj(e1 ) =
subj(e2 ) e parents(e1 ) = parents(e2 ) = ∅ e dunque applicando il caso 2 della procedura v ∈ Int(E1 , E2 ) con ϕ(v) =
(e1 , e2 ). Tale v è unico per il corollario 5.2.1 e dunque si ha
f (∅, e1 , e2 ) = v
caso h = n + 1: Posti e1 ∈ E1 , e2 ∈ E2 , si hanno i seguenti casi
85
86
Risultati di equivalenza
• e ≡ (X, e1 , e2 ): allora si ha name(e1 ) ∈ A e, posto Y l’insieme
degli elementi massimali di X e Y1 = {d1 |(z, d1 , d2 ) ∈ Y },
Y1 = parents(e1 )
dove Y1 = {d1 |(z, d1 , d2 ) ∈ Y }
(5.1)
(5.2)
Per ipotesi induttiva si ha f (Y ) ⊆ Int(E1 , E2 ). Inoltre per
5.1 si ha f (Y ) E1 = parents(e1 ). Inoltre è un insieme senza
conﬂitti per costruzione. Dunque applicando il caso 1 della
procedura esiste v ∈ Int(E1 , E2 ) tale che ϕ(v) = (e1 , e2 ). Inoltre per costruzione v
= {f (x)|x ∈ X} ∪ {v} e tale v è
unico per il corollario 5.2.1. Dunque f (X, e1 , e2 ) = v.
• e ≡ (X, e1 , e2 ): simmetrico al caso precendente.
• e ≡ (X, e1 , e2 ): allora si ha name(e1 ), name(e2 ) ∈ B, subj(e1 ) =
subj(e2 ). Inoltre per costruzione esiste S ⊆ X tale che per
ogni (z, d1 , d2 ) ∈ S, d1 ∈ parents(e1 ) o d2 ∈ parents(e2 ).
Si ponga dunque S = {(z, d1 , d2 ) ∈ S|d1 ∈ parents(e1 )} ed
S = {z, d1 , d2 ) ∈ S|d2 ∈ parents(e2 )}. Si noti che
S1 = parents(e1 ) e S2 = parents(e2 )(5.3)
dove S1 = {d1 |(z, d1 , d2 ) ∈ S } e S2 = {d2 |(z, d1 , d2 ) ∈ S }(5.4)
Quindi per ipotesi induttiva f (S ) ∪ f (S ) ⊆ Int(E1 , E2 ). Inoltre per 5.3 vale la condizione etichettata sui genitori (quella sul conﬂitto vale per costruzione) e dunque esiste v ∈
Int(E1 , E2 ) tale che ϕ(v) = (e1 , e2 ). Inoltre per costruzione
v
= {f (x)|x ∈ X} ∪ {v} e tale v è unico per il corollario
5.2.1. Dunque f (X, e1 , e2 ) = v.
iniettività: Vera in quanto due eventi che hanno predecessori uguali sono
uguali per costruzione.
suriettività Sia v ∈ Int(E1 , E2 ). Occorre dimostrare che esiste e ∈ Comp(E1 , E2)
tale che f (e) = v, per induzione sui passi della procedura. Vi sono due
casi:
v generato dal passo 1: In questo caso vi sono due sottocasi, ovvero
ϕ(v) = (e1 , e2 ) con e1 ∈ E1 e name(e1 ) ∈ A oppure ϕ(v) = (e1 , e2 )
con e2 ∈ E2 e name(e2 ) ∈ C. Verrà sviluppato solo il primo caso
in quanto il secondo è simmetrico rispetto al primo. In questo
caso esiste S ⊆ Int(E1 , E2 ) tale che S E1 = parents(e1 ). Poiche
Risultato di isomorﬁsmo
87
tali elementi sono stati generati in un passo precedente è possibile applicare su di essi l’ipotesi induttiva, pertanto per ogni
s ∈ S esiste es ∈ Comp(E1 , E2 ) tale che f (es ) = s. Si denota con Y = {es ∈ Comp(E1 , E2 )|f (es ) = s, s ∈ S} l’insieme di
questi elementi. Si noti che per costruzione Y1 = {d1 |(z, d1 , d2) ∈
Y } = parents(e1 ): quindi da qui è possibile costruire l’evento (Y , e1 , e2 ) ∈ Comp(E1 , E2 ) che è l’evento cercato in quanto
f (Y , e1 , e2 ) = v.
v generato dal passo 2: In questo caso si ha ϕ(v) = (e1 , e2 ) con
e1 ∈ E1 , e2 ∈ E2 , name(e1 ), name(e2 ) ∈ B e subj(e1 ) = subj(e2 ).
In questo caso esistono S1 , S2 ⊆ Comp(E1 , E2 ) tali che Si Ei =
parents(ei ). Poichè tali elementi sono stati generati in un passo
precedente è possibile applicare su di essi l’ipotesi induttiva, pertanto per ogni si ∈ Si esiste un esi tale che f (esi ) = si . Si denota
con Xi = {esi ∈ Comp(E1 , E2 )|f (esi ) = si , si ∈ Si }. Si costruisca
l’insieme X1 ∪ X2 ; si noti che per costruzione valgono:
• se Y è l’insieme degli elementi massimali di X1 ∪ X2 allora
per ogni (z, d1 , d2) ∈ Y , d1 ∈ parents(e1 ) o d2 ∈ parents(e2 )
• per ogni d1 ∈ parents(e1 ) esiste (z, d1 , d2 ) ∈ X1 ∪ X2 • per ogni d2 ∈ parents(e2 ) esiste (z, d1 , d2 ) ∈ X1 ∪ X2 Da qui è possibile costruire l’evento (X1 ∪ X2 , e1 , e2 ) ∈ Comp(E1 , E2 ).
Si noti che f (X1 ∪ X2 , e1 , e2 ) = v come si voleva.
riﬂessione e preservazione dell’ordine: Siano (x, e1 , e2 ) ≤ (z, d1 , d2 ) ∈
Comp(E1 , E2 ). Vi sono due casi:
• (X, e1 , e2 ) = (Z, d1, d2 ): in questo caso si conclude in modo banale.
• (X, e1 , e2 ) ∈ Z. In questo caso si ha f (z, d1 , d2 ) = v tale che
v
= {v} ∪ {f (z)|z ∈ Z} e da qui si conclude.
L’altra direzione vale banalmente per costruzione.
riﬂessione e preservazione del conﬂitto: Siano (x, e1 , e2 ) (z, d1 , d2 ) ∈
Comp(E1 , E2 ). Si hanno i seguenti casi
• e1 d1 o e2 d2 con e = d: in questo caso è immediato che
f (x, e1 , e2 ) f (z, d1 , d2 ).
• esiste un e = (x , e1 , e2 ) ∈ x tale che e1 1 d1 o e2 2 d2 e e = d:
in questo caso f (x , e1 , d1 ) f (z, d1 , d2 ) e poichè (x , e1 , e2 ) ≤
(x, e1 , e2 ) si conclude per ereditarietà dei conﬂitti.
88
Risultati di equivalenza
• esiste un d = (z , d1, d2 ) ∈ z tale che d1 1 e1 o d2 2 e2 e e = d
: analogo al precedente.
• esiste un e ∈ x , d ∈ z tali che e d : analogo al precedente
Nell’altra direzione, siano u = f (x, e1 , e2 ) v = f (z, d1 , d2 ).Si procede
per induzione sui passi dell’algoritmo con i seguenti casi:
• e1 d1 o e2 d2 : immediato
• esiste u v con u ≤ u: per suriettività esiste e ∈ Comp(E1 , E2 )
tali che f (e) = u . Per ipotesi induttiva si ha e (z, d1 , d2 ).
Per riﬂessione dell’ordine si ha e ≤ (x, d1 , d2 ) e si conclude per
ereditarietà.
preservazione dell’etichettaggio Vera per costruzione.
5.4
Risultato di equivalenza
In questa sezione si dimostrerà l’equivalenza della composizione illustrata
nella sezione 4.4 con la composizione di strutture di eventi tipate illustrata
nel capitolo 4. Si intende qui mostrare che le strutture generate dalle due
deﬁnizioni in realtà sono la stessa: per fare ciò si mostrerà che quando viene
aggiunto un evento alla struttura di eventi composta usando una deﬁnizione,
il medesimo evento viene aggiunto utilizzando l’altra deﬁnizione. Si hanno
dunque i seguenti:
Lemma 5.4.1. Sia S ⊆ Int(E1 , E2 ) senza conﬂitti e sia ei ∈ Ei. Se subj(S) =
subj(e1 ) allora esiste t ∈ S tale che t Ei = ei
Dimostrazione. Conseguenza immediata del corollario 5.2.1 e della proposizione 4.3.3.
Proposizione 5.4.1. Siano E1 : A ∪ B ed E2 : B⊥ ∪ C due strutture di eventi
tipate. Sia v ∈ E1 E2 . Allora v ∈ Int(E1 , E2 ).
Dimostrazione. La prova è per induzione sui passi della procedura. Sia v ∈
E1 E2 : esso è stato generato utilizzando il caso
1. in questo caso name(v) ∈ A o name(v) ∈ C: si sviluppa solo il caso
name(v) ∈ A poiché l’altro è duale. In questo caso esiste e1 ∈ E1 tale
che λ(e1 ) = λ(v) ed esiste S ⊆ E1 E2 tale che subj([e1 )) = subj(S).
Per ipotesi induttiva si ha S ⊆ Int(E1 , E2 ). Si mostrerà nel seguito che
Risultato di equivalenza
89
esiste S ⊆ S soddisfacente la condizione sui genitori etichettate e sui
conﬂitti da cui segue v ∈ Int(E1 , E2 ) e si mostrerà che S
= S .
Si noti anzitutto che
[e1 ) =
d
d∈parents(e1 )
che implica
subj([e1 )) =
subj(d
)
d∈parents(e1 )
= subj(S)
Quindi esitono S1 , . . . , Sn ⊆ S (n = |parents(e1 )|) tali che
n
i=1
subj(Si ) =
subj(d
)
d∈parents(e1 )
= subj(S)
di ∈ parents(e1 ) i ∈ {1, . . . , n}
con subj(Si ) = subj(di )
Per il lemma 5.4.1 esiste ui ∈ Si tale che ui E1 = di per ogni i. Quindi si
ha che S = {ui|i ∈ {1, . . . , n}}. S è senza conﬂitti per la proposizione
4.3.5. Inﬁne si noti che per costruzione si ha S
= S .
2. in questo caso name(v) ∈ B: quindi esistono e1 ∈ E1 , e2 ∈ E2 tali
che subj(e1 ) = subj(e2 ) = subj(v) ed esistono S1 , S2 ⊆ E1 E2 tali che
subj([e1 )) = subj(S1 ) e subj([e2 )) = subj(S2 ). Per ipotesi induttiva
S1 , S2 ⊆ Int(E1 , E2) e utilizzando argomenti analoghi al caso precedente
si costruiscono S1 , S2 cercati.
Proposizione 5.4.2. Siano E1 : A ∪ B ed E2 : B⊥ ∪ C due strutture di eventi
tipate. Sia v ∈ Int(E1 , E2 ). Allora v ∈ E1 E2 .
Dimostrazione. La prova è per induzione sulla costruzione di Int(E1 , E2 ). Si
hanno due casi:
1. in questo caso v ∈ Int(E1 , E2) con name(v) ∈ A o name(v) ∈ C. Si
sviluppa solo il caso name(v) ∈ A in quanto l’altro è duale. Quindi
esiste e1 ∈ E1 tale subj(e1 ) = subj(v) ed esiste S ⊆ Int(E1 , E2) tale che
S E1 = parents(e1 ). Per ipotesi induttiva S ⊆ E1 E2 e questo signiﬁca
che per ogni s ∈ S esiste d ∈ parents(e1 ) tale che esiste Vs ⊆ [s) tale
90
Risultati di equivalenza
che subj(Vs ) = subj([d)). Quindi si costruisce S = s∈S Vs ∪ {s} e
per costruzione si ha subj(S ) = subj([e1 )) come si voleva. Inoltre esso
è senza conﬂitti per la proposizione 5.4.3. Inﬁne si noti, sempre per
costruzione che S
= S .
2. in questo caso v ∈ Int(E1 , E2) con name(v) ∈ B. Quindi esistono e1 ∈
E1 , e2 ∈ E2 tali che subj(e1 ) = subj(e2 ) = subj(v) ed esistono S1 , S2 ⊆
Int(E1 , E2 ) tali che S1 E1 = parents(e1 ) ed S2 E2 = parents(e2 ). Per
ipotesi induttiva S1 , S2 ⊆ E1 E2 e si costruiscono S1 , S2 utilizzando
argomenti analoghi al caso precedente.
Le proposizioni precedenti permettono di mostrare che le due strutture di
eventi composte sono uguali rispetto all’insieme degli eventi e all’ordine che
su di essi è deﬁnito: occorre mostrare che anche le due relazioni di conﬂitto
sono equivalenti. Si denotano con Int e la relazioni di conﬂitto deﬁnite
ripsettivamente in Int(E1 , E2) e E1 E2 . Si ha la seguente:
Proposizione 5.4.3. v1 Int v2 ⇐⇒ v1 v2
Dimostrazione. Si dimostra la doppia implicazione:
(⇒): per induzione sulla deﬁnizione di v1 Int v2 .
• v1 Int v2 perchè v1 Ei = e1 v2 Ei = e2 . Poichè Ei è tipata allora
vale uno dei seguenti
– name(e1 ) = name(e2 ) e allora conseguentemente name(v1 ) =
name(v2 ) e si conclude
– esistono e1 ≤ e1 , e2 ≤ e2 tali che name(e1 ) = name(e2 ). Ma allora
per costruzione esistono v1 ≤ v1 , v2 ≤ v2 tali che name(v1 ) =
name(v2 ) e si conclude.
• v1 Int v2 perchè esiste v1 ≤ v1 tale che v1 Int v2 . Per ipotesi
induttiva si ha v1 v2 e si conclude per ereditarietà.
(⇐): Sia v1 v2 : allora si hanno due casi
• name(v1 ) = name(v2 ). Ma allora per costruzione v1 Ei v2 Ei
• esistono v1 ≤ v1 , v2 ≤ v2 tali che name(v1 ) = name(v2 ). Ma allora per
costruzione v1 Ei v2 Ei e si conclude per eriditarietà.
Discussione
5.5
Discussione
Con questo capitolo, si chiude il cerchio attorno alle strutture di eventi
tipate, mostrando che la deﬁnizione di composizione data è equivalente alla
composizione di strutture di eventi deﬁnita nel capitolo 2.
L’intenzione qui è quella di esporre la portata di questo risultato: infatti,
dopo tutte le analisi e le considerazioni fatte nei capitoli 4 e 5, è stata deﬁnita
una struttura generale e versatile, la quale ‘vive’ in due diﬀerenti ambiti:
teoria della concorrenza: dove essa incarna le strutture ad eventi senza
confusione e la composizione data qui è la composizione di strutture ad
eventi senza confusione.
semantica dei giochi: dove essa incarna le L-net e la composizione data
qui è la normalizzazione delle L-net deﬁnita in [FM05].
Dunque è possibile utilizzare questa struttura generale come mezzo di
trasferimento di tecnologie da un ambito ad un ambito all’altro: in particolare
questo trasferimento inizierà già nel prossimo capitolo dove verrà dato un
modello a strutture ad eventi tipate per un frammento di CCS, detto CCS
polarizzato.
91
92
Risultati di equivalenza
Capitolo 6
CCS polarizzato
In questo capitolo si introdurrà una forma di calcolo dei processi che può
essere identiﬁcato in un frammento di CCS di R. Milner. Questo calcolo sarà
utilizzato come linguaggio di riferimento per darne una codiﬁca a strutture
di eventi tipate , il quale verrà impostato al termine di questo capitolo.
Le modiﬁche principali del linguaggio, che nel seguito si chiamerà CCS
polarizzato, rispetto al CCS standard sono le seguenti e sono introdotte
allo scopo di facilitarne uno studio attraverso le strutture ad eventi senza
confusione:
polarizzazione: la scelta non deterministica, resa dall’operatore +, è data
in forma preﬁssa con azioni che sono tutte della medesima polarità.
uso controllato degli operatori di parallelo e restrizione: l’operatore
di parallelo fra processi è utilizzato in modo controllato assieme all’operatore di restrizione in modo da mettere in evidenza i soggetti su cui i
processi in questione si sincronizzeranno.
mancanza dell’operatore di ricorsione.
Questo frammento si ispira a NCCS, introdotto in [VY06], come passo
intermedio per la codiﬁca di un frammento di π-calcolo in strutture di eventi,
il quale riporta fra le sue caratteristiche gli stessi aspetti sopra citati. Inoltre,
un’altra aﬃnità di CCS polarizzato con NCCS è la nozione di equivalenza
strutturale di processi che non prevede nessuna nozione di α-equivalenza.
Questo aspetto è molto importante e verrà chiarito nel seguito.
Tuttavia CCS polarizzato diﬀerisce da NCCS per due aspetti
1. le azioni di NCCS sono costruite in modo da riferirsi ad una precisa
arena e costituire una sequenza giustiﬁcata stile semantica dei giochi,
mentre le azioni di CCS polarizato sono meno strutturate in quanto
esse non si riferiscono a nessuna arena in particolare.
93
94
CCS polarizzato
2. in NCCS è previsto un costrutto per eﬀettuare la replicazione dei
processi, mentre in CCS polarizzato ciò non è realizzato.
Il capitolo si articolrerà come segue: inizialmente verrà deﬁnito il linguaggio con le relative regole di transizione etichettata e la nozione di equivalenza
strutturale. Dopo di che verrà formalizzato il concetto di equivalenza osservazionale deﬁnendo la nozione di bisimulazione. Succssivamente verrà
introdotto un sistema di tipi per CCS polarizzato il quale serve per garantire che la codiﬁca in strutture di eventi tipate sia ben deﬁnito. Inﬁne si
costruirà il modello in strutture di eventi tipate per il quale si dimostrerà la
correttezza.
6.1
Deﬁnizioni, regole di transizione etichettata
In questa sezione verrà introdotto CCS polarizzato. Posto N un insieme di
nomi, I, J insiemi di indici, ∈ Π, la sintassi è la seguente:
α ::=
P ::=
|
|
|
ai con a ∈ N, i ∈ I
α con ∈ {+, −, ±}
j∈J αj .Pj
P1 |P2
(νX)P
0
azioni non polarizzate
azioni polarizzate
somma preﬁssata
operatore di parallelo
restrizione con X ⊆ N
zero
Dato un processo P , si deﬁniscono f n(P ) ⊆ N per induzione sulla
struttura di P :
• f n(0) = ∅
• f n( i∈I ai .Pi ) = {a} ∪ i∈I f n(Pi )
• f n(P |Q) = f n(P ) ∪ f n(Q)
• f n((νX)P ) = f n(P ) \ X
Sui processi generati dalla sintassi è deﬁnita una relazione di congruenza
strutturale ≡ cosı̀ deﬁnita:
1. α .P + β .Q ≡ β .Q + α .P
Deﬁnizioni, regole di transizione etichettata
2. P |0 ≡ P, P |Q ≡ Q|P, P |(Q|R) ≡ (P |Q)|R
3. (νX)(P |Q) ≡ P |(νX)Q se f n(P ) ∩ X = ∅
(νX)0 ≡ 0, (νX)(νY )P ≡ (νX ∪ Y )P
La congruenza strutturale qui deﬁnita è uguale alla deﬁnizione standard eccetto per il fatto che non è ammesso nessun tipo di α-equivalenza. Questo
aspetto è molto importante in quanto, se l’operatore ν ha il compito di stabilire quali soggetti sono da dichararsi privati, eﬀettuare il renaming signiﬁca cambiare i soggetti (ovvero le azioni non polarizzate) da rendersi privati.
Tenendo conto di ciò, si ha la seguente semantica operazionale, data in forma
di LTS
(sumj )
αj
α
.P
→
P
j
i∈I i i
(a,i)
P → P
(a,i)
(νX)P → (νX)P
(pub)
a ∈ X, ∈ {+, −}
(a,i)±
P → P
(priv)
(a,i)±
(νX)P → (νX)P a∈X
α
P1 → P1
α
P1 |P2 → P1 |P2
(par − l)
α
P2 → P2
α
P1 |P2 → P1 |P2
α
(par − r)
α−
P1 → P1 , P2 → P2
α±
P1 |P2 → P1 |P2
6.1.1
(sync)
Bisimulazione
Occorre formalizzare una nozione di equivalenza osservazionale di due o
più processi che descrivono sistemi. Intuitivamente due processi sono osservazionalmente equivalenti se si comportano allo stesso modo, ovvero essi
si evolvono in egual maniera. Se un processo esegue una determinata azione e
95
96
CCS polarizzato
raggiunge uno stato allora anche l’altro processo esegue la stessa azione e raggiunge uno stato comparabile con quello raggiunto dal processo precedente.
Più formalmente si ha la seguente:
Deﬁnitione 6.1.1 (bisimulazione). Sia R una relazione binaria simmetrica fra processi. Si dice che R è una bismulazione se è soddisfatta la seguente
α
α
• nel caso P RQ e P → P allora esiste Q tale che Q → Q e P RQ
Due processi P e Q si dicono bismili e si scrive P ∼ Q se esiste una
bisimulazione che li contiene. Si noti che, in base alla deﬁnizione data qui
sopra, la relazione di bisimiarità gode delle seguenti proprietà
• ∼ è l’unione di tutte le relazioni di bisimulazione
• ∼ è una bisimulazione
• ∼ è una relazione di equivalenza
6.2
Typing system
In questa sezione si introdurrà un typing system per CCS lineare polarizzato. Esso si ispira al typing system lineare dato in [VY06] e garantisce in
particolare le stesse proprietà di conﬂuenza e non determinismo localizzato,
necessarie per poterlo modellare in strutture di eventi tipate. Si hanno
CAPABILITIES
σ, τ ::= +| − |±
ENVIRONMENTS/INTERFACCE
∆, Γ ::= ∅|a1 : τ1 , a2 : τ2 . . . ai ∈ N
L’insieme delle capabilities è denotato con C = {+, −, ±}. Per non appesantire la notazione, si è deciso di utilizzare la stessa notazione per denotare
capabilities e polarità delle azioni: ovviamente ∈ C è inteso come capability se usato in un ambiente, mentre è inteso come polarità se usato in una
azione.
Sulle capabilities è deﬁnita l’operazione di dualizzazione (τ ), dove + = −
e − = + e indeﬁnita per ±. Inoltre sui type environment sono deﬁnite le
seguenti operazioni:
dualizzazione (Γ):
Typing system
97
• ∅=∅
• Γ , a : τ = Γ , a : τ
neutralizzazione (Γ± ):
• ∅± = ∅
• (Γ , a : τ )± = Γ± , a : ±
Si hanno le seguenti regole di buona costruzione dei type environment
∅$
(empty)
Γ $ a ∈ Dom(Γ)
(single)
Γ, a : τ $
Dato un environment Γ $, l’insieme dei nomi che vi appaiono si denota con
Dom(Γ). Se Γ ≡ Γ , a : τ , si denota Γ(a) = τ . Dati due environment ∆ $ e
Γ $ essi si dicono disgiunti se Dom(∆) ∩ Dom(Γ) = ∅
Lemma 6.2.1 (unione). Siano Γ $ e ∆ $ disgiunti. Allora Γ, ∆ $.
Dimostrazione. Per induzione sul giudizio Γ $
caso (empty): Allora si conclude immediatamente
caso (single): In questo caso Γ = Γ , a : τ e Γ$ diretta conseguenza di Γ $
e a ∈ Dom(Γ ). Poichè Γ e ∆ sono disgiunti, anche Γ e ∆ lo sono e
dunque si può applicare l’ipotesi induttiva e si ha Γ , ∆$. Inoltre per il
fatto a ∈ Dom(Γ ) e poiche Γ e ∆ sono digiunti, si ha a ∈ Dom(Γ , ∆) e
dunque si può applicare la regola (single) per concludere a : τ, Γ , ∆ $
come si voleva
Lemma 6.2.2. Sia Γ $. Allora
• Γ$
• Γ± $
Dimostrazione. Diretto per induzione sul giudizio Γ $.
98
CCS polarizzato
Sia Γ $ e sia α con α = (a, i) un’azione polarizzata. Si dice che Γ
autorizza α se Γ(a) = .
Le regole di typing dei processi sono le seguenti
0∆
zero
P ∆ . . . Pn ∆
n 1
sum
i=1 (a, i) .Pi a : , ∆
Con ∆ $ e a ∈ Dom(∆).
P Γ, Ξ Q Ξ, ∆ X = Dom(Ξ)
comp
(νX)P |Q Γ, Ξ± , ∆
Con Γ $∆ $Ξ $ disgiunti.
Si notI che se, come caso particolare di (comp), se P Γ e Q ∆ con Γ $
e ∆ $ disgiunti allora P |Q Γ, ∆.
Si noti inoltre, che la regola (comp) forza un utilizzo controllato dell’operatore di parallelo, usato in combinazione con l’operatore di restrizione. Cio’ fa
si che le sincronizzazioni fra le azioni avvengano in un contesto locale, restringenedo tutti i nomi comuni ai due processi impendendone la sincronizzazione
con l’ambiente esterno (composizione con occultamento).
6.3
Risultati di type safety
In questa sezione si mostrerà che il typing è preservato in ogni passo di
transizione etichettata. In particolare si ha la seguente:
α
Proposizione 6.3.1. Sia P Γ e sia P → Q con Γ che autorizza α . Allora
Q Γ \ α (dove Γ \ α è lo stesso environment Γ senza il nome di α)
α
Dimostrazione. Per induzione sulla derivazione di P → Q e per casi sull’ultima regola utilizzata.
caso (sumj ) Quindi P = i∈I αi .Pi e Q = Pj con j ∈ I. P Γ può essere
derivato solamente da (sum) con Γ = Γ a : in cui fra le premesse
ﬁgura Pj Γ come si voleva.
α
caso (pub): Dunque P = (νX)P1 e Q = (νX)P2 e P → Q dove α = (a, i)
α
diretta conseguenza di P1 → P2 con a ∈ X e ∈ {+, −}. In questo
caso, (νX)P1 Γ deve essere stato derivato dalla regola (comp) con
La codiﬁca in strutture di eventi tipate di CCS polarizzato
99
Γ = Γ1 , Γ±
2 , Γ3 , P1 = P1 |P1 e con premesse P1 Γ1 , Γ2 e P1 Γ2 , Γ3 .
Poichè ∈ {+, −}, l’azione α può essere stata eseguita o da P1 o da P1 .
Si assume che sia stata eseguita da P1 (l’altro caso è analogo): allora α
è autorizzata in P1 e in particolare a ∈ Dom(Γ1 ) e quindi applicando
α
l’ipotesi induttiva su P1 → P2 (con P2 = P2 |P2 con P2 = P1 ) ho che
P2 Γ1 \α, Γ2 (per il fatto che a ∈ X = Dom(Γ2 )). Dunque riapplicando
la regola (comp) con premesse P2 Γ1 \ α, Γ2 e P2 Γ2 , Γ3 si ottiene
(νX)P2 |P2 Γ1 \ α, Γ±
2 , Γ3 come si voleva.
α±
caso (priv): Dunque P = (νX)P1 e Q = (νX)P2 e P → Q con α = (a, i)
α±
diretta conseguenza di P1 → P2 con a ∈ X. In questo caso, (νX)P1 Γ deve essere stato derivato dalla regola (comp) con Γ = Γ1 , Γ±
2 , Γ3 ,
P1 = P1 |P1 e con premesse P1 Γ1 , Γ2 e P1 Γ2 , Γ3 . Poichè l’azione
α
α−
è neutra, deve essere stato P1 → P2 e P1 → P2 dove P2 = P2 |P2 .
Osservando che a ∈ X = Dom(Γ2 ), per costruzione α (risp α− ) è
abilitata in Γ2 (risp Γ2 ), dunque applicando l’ipotesi induttiva si ha
P2 Γ1 , Γ2 \ α e P2 Γ2 \ α, Γ3 : Quindi riapplicado (comp) si ottiene
(νX)P2 |P2 Γ1 , Γ±
2 \ α, Γ3 come si voleva.
α
caso (par − l): Dunque P = P1 |P2 e Q = P1 |P2 e P → Q diretta conseguenα
za di P1 → P1 . P1 |P2 Γ deve essere conseguenza della regola (comp)
(con environment disgiunti) con P1 Γ1 e P2 Γ2 . Quindi per ipotesi
induttiva P1 Γ1 \ α e riapplicando (comp) si ottiene P1 |P2 Γ1 \ α, Γ2
come si voleva.
caso (par − r): Analogo al precedente
α
caso (sync): Si noti che questo caso non può mai accadere, in quanto P1 →
α
P1 e P2 → P2 implica che gli environment non sono digiunti, condizione
richiesta dalla regola (comp)
6.4
La codiﬁca in strutture di eventi tipate
di CCS polarizzato
In questa sezione si deﬁnirà una codiﬁca di CCS polarizzato in strutture di
eventi tipate. Esso si ispira alla codiﬁca per NCCS dato in [VY06], il quale
deriva dal modello intuitivo deﬁnito da Winskel in [Win82]. La funzione [[ · ]]
100
CCS polarizzato
mapperà environment ben formati in interfacce e processi CCS tipati con
dato environment in strutture di eventi di corrispondente interfacccia e il
risultato più importante che verrò nel seguito dimostrato sarà la validità del
modello, data nel teorema omonimo.
6.4.1
Deﬁnizione del modello
La semantica di CCS polarizzato in strutture di eventi tipate è descritta nel
seguito. In particolare verranno utilizzate le operazioni sulle strutture di
eventi deﬁnite nel capitolo 1 e la composizione parallela deﬁnita nel capitolo
3. Inoltre per quanto concerne i nomi, [[ · ]] interpreterà i nomi utilizzati per
identiﬁcare un cluster di azioni nella somma preﬁssata deﬁnita sui processi
CCS in nomi identiﬁcanti celle, nel contesto strutture di eventi tipate: conseguentemente le azioni polarizzate e non di CCS verranno interpretate nelle
etichette polarizzate e non usate nelle strutture di eventi etichettate. Si osservi anzitutto che vi è un’esatta corrispondenza fra nomi, polarità e azioni
nel contesto strutture di eventi (per tanto per essi [[ · ]] è la mappa identità).
Per le interfacce e i processi, essa è la seguente:
ENVIRONMENT/INTERFACCE
[[∅ $]] = I
[[Γ, a : τ $]] = aτ ∪ [[Γ]]
PROCESSI CCS/STRUTTURE AD EVENTI
[[
[[0 ∆]] = ∅
n
(a, i) .Pi a : , ∆]] =
(a, i) .[[Pi ∆]]
n
i=1
i=1
±
[[(νX)P |Q Γ, Ξ , ∆]] = [[P Γ, Ξ]][[Q Ξ, ∆]] con P Γ, Ξ e Q Ξ, ∆
Alcuni lemmi utili:
Lemma 6.4.1. Sia Γ $ un’interfaccia e sia a ∈ Dom(Γ). Allora [[a]] ∈ [[Γ]].
Dimostrazione. Per costruzione si ha Γ = Γ , a : τ . Inoltre
[[Γ]] = [[Γ , a : τ ]]
= aτ ∪ [[Γ ]]
Chiaramente [[a]] ∈ [[Γ]]
La codiﬁca in strutture di eventi tipate di CCS polarizzato
101
Lemma 6.4.2 (correttezza sui tipi). Sia Γ $ un environment ben formato. Allora [[Γ $]] è un’interfaccia.
Dimostrazione. Per induzione sulla derivazione di Γ $.
caso (empty): Ovvio
caso (single): quindi Γ = Γ , a : τ e Γ $ diretta conseguenza di Γ $ con
a ∈ Dom(Γ ). Per ipotesi induttiva [[Γ $]] = A, πA è un’interfaccia.
Inoltre per il fatto a ∈ Dom(Γ ) e per il lemma precedente si ha a ∈ A
e quindi aτ ∪ [[Γ ]] è un’interfaccia.
Lemma 6.4.3 (morﬁsmi sulle operazioni). Siano Γ $ e ∆ $ due
environment disgiunti. Allora
1. [[Γ, ∆]] = [[Γ]] ∪ [[∆]]
2. [[Γ]] = [[Γ]]⊥
3. [[Γ± ]] = [[Γ]]±
Dimostrazione.
1. Conseguenza diretta dei lemmi 6.2.1 e 6.4.1
2. Conseguenza diretta del lemma 6.2.2 e per costruzione
3. Conseguenza diretta del lemma 6.2.2 e per costruzione
6.4.2
Teorema di validità
Siamo ora in grado di dare il risultato più importante, concernente la semantica di CCS polarizzato, ovvero che i processi CCS tipati vengono interpretati
in strutture di eventi tipate con la corrispondente interfaccia. Si ha dunque
Teorema 6.4.1 (validità). Sia P Γ. Allora [[P Γ]] : [[Γ]].
Dimostrazione. Per induzione sul giudizio P Γ.
caso (zero): Ovvio.
n
caso (sum): Quindi P =
i=1 (a, i) .Pi , Γ = a : , ∆ e P Γ diretta
coseguenza
di Pi ∆. Per ipotesi induttiva [[Pi ∆]] : [[∆]]. Quindi
(a,
i)
.[[P
i ∆]] senza confusione poichè la somma di strutture di
i∈I
eventi preserva la classe delle strutture
di eventi senza confusione. Si
noti inoltre che per costruzione i∈I (a, i) .[[Pi ∆]] : [[Γ]] come si voleva.
102
CCS polarizzato
caso (comp): Quindi P = (νX)P1 |P2 , Γ = Γ1 , Γ±
2 , Γ3 e P Γ diretta conseguenza di P1 Γ1 , Γ2 e P2 Γ2 , Γ3 . Per ipotesi induttiva e per il lemma
6.4.3 [[P1 Γ1 , Γ2 ]] : [[Γ1 ]] ∪ [[Γ2 ]] e [[P2 Γ2 , Γ3 ]] : [[Γ2 ]]⊥ ∪ [[Γ3 ]] e si conclude
per il teorema 4.4.1.
6.4.3
Corrispondenza fra le semantiche
In questa sezione si mostrerà il risultato di full-abstraction relativo al modello dato. Per farlo, ci si servirà di una nozione di ‘transizione etichettata’
deﬁnita sulle strutture di eventi tipate. Ciò è fondamentale, in quanto permette di deﬁnire nel modello una relazione di bisimulazione, che sarà utile
per mostrare la proprietà desiderata.
Transizioni etichettate di strutture di eventi
In questa sezione si deﬁnisce un sistema di transizione etichettato sulle strutα
ture di eventi. Intuitivamente, se E1 → E2 signiﬁca che α è l’etichetta di un
evento minimale in E1 e che quindi E1 puo ‘eseguire’ α e ridursi ad una sua
sottostruttura, in cui α è stato tolto e, con lui tutti gli eventi in conﬂitto con
α. Formalmente si ha
Deﬁnitione 6.4.1. Sia E = E, ≤, , λ una struttura di eventi e sia e ∈ E
un evento minimale. Si deﬁnisce E %e = E , ≤ , , λ dove:
• E = {d ∈ E|d e}
• ∀d1 , d2 ∈ E .d1 ≤ d2 ⇐⇒ d1 ≤ d2
• ∀d1 , d2 ∈ E .d1 d2 ⇐⇒ d1 d2
• ∀d ∈ E .λ (d) = λ(d)
Informalmente, E %e è la struttura di eventi E senza l’evento e e senza
tutti gli eventi in conﬂitto con lui. E’ possibile generare un LTS di strutture
di eventi come segue. Sia e ∈ E evento minimale con λ(e) = β . Allora
β
E → E %e
La relazione fra l’LTS nel linguaggio e nel modello è dato dalle seguenti
proposizioni
α
Proposizione 6.4.1. Sia P Γ e sia P → Q con Γ che autorizza α . Allora
α
[[P Γ]] → [[Q Γ \ α]]
La codiﬁca in strutture di eventi tipate di CCS polarizzato
103
α
Dimostrazione. Per induzione sulla derivazione di P → Q
α
Proposizione 6.4.2. Sia P Γ. Se [[P Γ]] → E : A allora esiste Q ∆
α
tale che P → Q con [[Q ∆]] = E
Dimostrazione. Per induzione sulla derivazione del giudizio P Γ
Entrambe le prove sopra citate utilizzano il seguente lemma:
Lemma 6.4.4. Siano E1 : A ∪B e E2 : B⊥ ∪C due strutture di eventi. Allora
α
α−
α±
E1 → E1 %e1 e E2 → E1 %e2 se e solo se E1 E2 → E1 E2 %v (dove λ(v) = α± ).
Inoltre, in questo caso E1 %e1 E2 %e2 = E1 E2 %v .
Esso si dimostra utilizzando la deﬁnizione di composizione per slice.
In modo analogo con gli LTS standard, deﬁniamo una nozione di bisimulazione di strutture di eventi.
Deﬁnitione 6.4.2 (Bisimulazione di strutture di eventi). Sia R una
relazione binaria simmetrica fra strutture di eventi. R è una bisimuazione se
vale la seguente:
β
β
se E1 RE2 ed E1 → E1 allora esiste E2 tale che E2 → E2 e E1 RE2
Due strutture di eventi E1 , E2 si dicono bisimili e si scrive E1 ∼ E2 se
esiste una bisimulazione di strutture di eventi che le contiene.
Si può dimostrare il seguente teorema chiave:
Teorema 6.4.2. Siano E1 , E2 : A. Allora
E1 ∼ E2 ⇐⇒ E1 = E2
Dimostrazione. Poichè E1 ∼ E2 allora esiste una relazione R che è una
bisimulazione tale che E1 RE2 .
Il risultato si ottiene per induzione sulla struttura di E1 e E2 , sfruttando
il fatto che se E1 ed E2 sono bisimili, hanno gli stessi elementi minimali.
A questo segue il seguente
Teorema 6.4.3 (full abstraction). P Γ ∼ Q Γ ⇐⇒ [[P Γ]] = [[Q Γ]]
Dimostrazione. (⇒): Se P ∼ Q allora esiste una bisimulazione R che contiene (P, Q). Ma allora per la proposizione 6.4.1 posso costruire una bisimulazione di strutture di eventi che contiene ([[P ]], [[Q]]). Ma allora per il teorema
6.4.2, [[P ]] = [[Q]].
(⇐): Se [[P ]] = [[Q]] allora per il teorema 6.4.2, esite una bisimulazione di
strutture di eventi. Ma allora per la proposizione 6.4.2, posso costruire una
relazione che contiene (P, Q) e mostrare che è una bisimulazione
104
CCS polarizzato
6.5
Conclusioni
In questo capitolo, si è introdotto un frammento di CCS, detto appunto
CCS polarizzato. Si è deﬁnito un typing system che garantisce l’assenza
di confusione, ovvero un processo ben tipato ha la proprietà che la scelta
non deterministica è localizzata in un ben preciso punto del processo e non
dipende dalle politiche di schedulazione adottate per farlo eseguire. Si è
mostrato che il tipaggio è preservato per riduzione. Inﬁne per dimostrare la
presenza di questa proprietà si è pertanto deﬁnito un modello a strutture ad
eventi tipate e si è fatto vedere che il modello dato è corretto e si è dato un
risultato di full abstraction (vedi Sezione 3).
Un typing system che garantisce questa proprieta era già stato dato in
[VY06] sia per CCS che per π-calcolo (e per quanto concerne CCS, per un
frammento più ampio rispetto a quello coperto da CCS polarizzato)1 . Ciò
che è nuovo qui è l’approccio: si sono applicate tecniche provenienti dalla
semantica dei giochi e in particolare dalle strategie lineari in un contesto di
teoria della concorrenza, in particolare per dare una semantica a strutture
di eventi di un frammento di CCS. Inoltre il typing system dato qui è una
sempliﬁcazione del typing system lineare dato in [VY06].
In questa tesi, è stata introdotta una struttura generale, che se portata
in un contesto teoria della concorrenza, è una struttura di eventi senza confusione e se portata in un contesto semantica dei giochi è un’estensione delle
L-net. Tale struttura comune apre la strada ad un trasferimento di tecnologie
tra le due aree.
Il lavoro presentato in questo capitolo rappresenta una prima tappa verso
la costruzione di modelli fully asbstract per (frammenti di) CCS o π-calcolo.
Per raggiungere questo ﬁne, ci proponiamo in lavoro futuro di:
• ampliare il frammento di CCS qui studiato, includendo l’operatore di
replicazione oppure la ricorsione
• estendere il lavoro ad un frammento di π-calcolo, per esempio il πcalcolo polarizzato in [Bef05]
Il lavoro presentato nel capitolo 4 apre la strada anche ad una trasferimento di tecnologie dalla teoria della concorrenza alla semantica dei giochi: lo
scopo di ottenere una generalizzazione del concetto di strategia, che permetta
di studiare il non determinismo e la concorrenza in semantica dei giochi.
1
In realtà nel lavoro di Daniele Varacca e Nobuko Yoshida è dato un risultato di
adequacy, per quanto concerne la corrispondenza fra le semantiche
Conclusioni
105
Inﬁne un altro ambito che ci interessa investigare, anche se non approfondito qui, è la connessione fra teoria della concorrenza e teoria della dimostrazione: vi sono infatti interessanti techiche delle reti di prova concernenti criteri di correttezza e deadlock il cui proposito è che possano essere
applicate per mostrare proprietà analoghe in teoria della concorrenza.
106
CCS polarizzato
Bibliograﬁa
[AJM00] S. Abramsky, R. Jagadeesan, and P. Malacaria. Full abstraction
for PCF. Information and Computation, 2000?
[AM99]
S. Abramsky and P.-A. Mellies. Concurrent games and full completeness. In Proceedings 15th Annual Symposium on Logic in
Computer Science, 1999.
[And92]
J-M. Andreoli. Logic programming with focusing proofs in linear
logic. Journal of Logic and Computation, 2(3), 1992.
[Bef05]
E. Beﬀara. Logique, Réalisabilité et Concurrence. PhD thesis,
UFR d’Informatique, Université Paris 7 - Denis Diderot, 2005.
[CF]
P.-L. Curien and C. Faggian. An approach to innocent strategies
as graphs. submitted to journal.
[CF05]
P.-L. Curien and C. Faggian. L-nets, strategies and proof-nets. In
CSL 05 (Computer Science Logic), LNCS. Springer, 2005.
[Cur06]
P. L. Curien. Semantica dei giochi. Note del corso di Semantica
dei giochi, 2006.
[Fag]
C. Faggian. Linear games: sequential and parallel. submitted.
[Fag02]
C. Faggian. Travelling on designs: ludics dynamics. In CSL’02
(Computer Science Logic), volume 2471 of LNCS. Springer Verlag,
2002.
[FM05]
C. Faggian and F. Maurel. Ludics nets, a game model of concurrent
interaction. In Proc. of LICS’05 (Logic in Computer Science).
IEEE Computer Society Press, 2005.
[Fra96]
J. Frakes. Star trek 7: First contact. con P. Stewart, J. Frakes.
Soggetto: R. Berman, B. Braga, R. D. Moore. Sceneggiatura: B.
Braga, R.D. Moore, 1996.
107
108
BIBLIOGRAFIA
[Gir87]
Jean-Yves Girard. Linear logic. Theoretical Computer Science,
50:1–102, 1987.
[Gir01]
Jean-Yves Girard. Locus solum. Mathematical Structures in
Computer Science, 11:301–506, 2001.
[GM04]
Dan R. Ghica and Andrzej S. Murawski. Angelic semantics of
ﬁne-grained concurrency. In FOSSACS, 2004.
[Har05]
Russ Harmer. Innocent game semantics. CNRS & PPS, 2005.
[HO00]
M. Hyland and L. Ong. On full abstraction for PCF. Information
and Computation, 2000.
[HS02]
M. Hyland and A. Schalk. Games on graphs and sequentially
realizable functionals. In LICS 02, pages 257–264. IEEE, 2002.
[Lai05]
J. Laird. A game semantics of the asynchronous pi-calculus. In
Concur 05, volume 3653 of LNCS, 2005.
[Lau04]
Olivier Laurent. Semantique des jeux. Note du cours de semantique
des jeux du DEA de Programmation, page 43 pages, 2004.
[Lor60]
P. Lorenzen. Logik und agon. In Atti del Congresso Internazionale
di Filosoﬁa, pages 193–200. Sansoni, 1960.
[Lor61]
P. Lorenzen. Ein dialogisches konstruktivitätskriterum. In Inﬁnitistic Methods, pages 193–200. PWN. Proceed. Symp. Foundations
of Math, 1961.
[Mel04]
P.-A. Mellies. Asynchronous games 2 : The true concurrency of innocence. In CONCUR 04, volume 3170 of LNCS. Springer Verlag,
2004.
[MW05] G. McCusker and M. Wall. Categorical and game semantics for
scir. In Galop 2005, pages 157–178, 2005.
[NPW81] M. Nielsen, G. Plotkin, and G. Winskel. Event structures and
domains 1. Theoretical Computer Science, 13:85–108, 1981.
[Pic06]
M. Piccolo. Event structures and strategies. Master’s thesis, Dip.
Matematica Pura e Applicata, Universitá di Padova, 2006.
BIBLIOGRAFIA
109
[RBM06] Hernan Melgratti Roberto Bruni and Ugo Montanari. Event
structure semantics for nominal calculi. In Proceedings of CONCUR 2006, 17th International Conference on Concurrency Theory,
LNCS, page 15 pages. SV, 2006. To Appear.
[RN05]
S. Russel and P. Norvig. Intelligenza Artiﬁciale: un Approccio Moderno. Seconda Edizione, volume 1, chapter Agenti Logici.
Pearson Prentice Hall, 2005.
[SPP05]
A. Schalk and J.J. Palacios-Perez. Concrete data structures as
games. In CTCS 04, volume 122 of Electr. Notes Theor. Comput.
Sci., 2005.
[VY06]
D. Varacca and N. Yoshida. Typed event structures and the picalculus. In MFPS, 2006.
[Win80]
G. Winskel. Events in computation. PhD thesis, Dept. of
Computer Science, University of Edinburgh, 1980.
[Win82]
G. Winskel. Event structure semantics for ccs and related languages. In Proceedings of 9th ICALP, volume 140 of LNCS, pages
561–576. Springer, 1982.
[Win87]
G. Winskel. Event structures. Advances in Petri Nets 1986, Part
II, volume 140 of LNCS:561–576, 1987.
[WN95]
G. Winskel and M. Nielsen. Handbook of Logic in Computer Science, volume 4, chapter Models for concurrency. Clarendon Press,
1995.
110
BIBLIOGRAFIA
Appendice A
A Graph Abstract Machine
Describing Event Structure
Composition
Claudia Faggian and Mauro Piccolo
Questo è l’articolo inerente alla parte inizile di questa tesi. Esso è stato
presentata a GT-VC (Graph Transformation for Veriﬁcation and Concurrency) che è un workshop satellite della conferenza internazionale CONCUR’06
sulla teoria della concorrenza, svoltasi a Bonn (Germania) dal 27 al 30 agosto.
Abstract: Event structures, Game Semantics strategies and Linear Logic
proof-nets arise in diﬀerent domains (concurrency, semantics, proof-theory)
but can all be described by means of directed acyclic graphs (dag’s). They
are all equipped with a speciﬁc notion of composition, interaction or normalization.
We report on-going work, aiming to investigate the common dynamics
which seems to underly these diﬀerent structures.
In this paper we focus on confusion free event structures on one side, and
linear strategies [Gir01, FM05] on the other side. We introduce an abstract
machine which is based on (and generalizes) strategies interaction; it processes labelled dag’s, and provides a common presentation of the composition at
work in these diﬀerent settings.
111
112
A Graph Abstract Machine Describing Event Structure Composition
A.1
Introduction
Event structures [NPW81], Game Semantics strategies and Linear Logic
proof-nets [Gir87] arise in diﬀerent domains (concurrency, semantics, prooftheory) but can all be described by means of directed acyclic graphs (dag’s).
They are all equipped with a speciﬁc notion of composition, interaction or
normalization. In this paper we report ongoing work whose ﬁrst aim is to
investigate the common dynamics which appears to underly all these diﬀerent structures, and eventually to transfer technologies between these settings.
As a ﬁrst step in this direction, here we present an abstract machine which
processes labelled dag’s. The machine is based on the dynamics at work when
composing Game Semantics strategies. When applied to linear strategies (in
the form introduced in [Gir01] or [FM05]) the machine implements strategies
composition. When applied to event structures, the result is the same as the
paralle composition of event structures deﬁned by Varacca and Yoshida in
[VY06].
Event structures.
Event structures are a causal model of concurrency
(also called true concurrency models), i.e. causality, concurrency and conﬂict
are directly represented, as opposite to interleaving models, which describe
the system by means of all possible scheduling of concurrent actions.
An event structure models parallel computation by means of
• occurrence of events;
• a partial order expressing causal dependency.
Non-determinism is modelled by means of:
• a conﬂict relation, which expresses how the occurrence of certain events
rules out the occurrence of others.
Two events are concurrent if they are neither causally related, nor in conﬂict.
Events which are in conﬂict live in diﬀerent possible evolutions of the system.
In this paper we will consider two classes of event structures:
confusion free event structure (where conﬂict, and hence non-determinism,
is well behaving)
conﬂict free event structures (where there is no conﬂict, and hence no
non-determinism).
Introduction
113
Confusion free event structure, are an important class of event structures
because the choices which a process can do are “local” and not inﬂuenced by
independent actions. In this sense, confusion freeness generalizes conﬂuence
to systems that allow nondeterminism.
A point which is central to our approach is that a confusion free event
structure E can be seen as a superposition of conﬂict-free event structures
(which we will call the slices of E): each slice represents a possible and
independent evolution of the system.
Because of this, if E is confusion free, the study of several properties can
be reduced to the study of such properties in conﬂict free event structures.
Game Semantics Games and strategies provide denotational models for
programming languages and logical systems; games correspond to types (formulas), and strategies to programs (proofs). The central notion is that of
interaction, which models program composition (normalization of proofs).
A distinction between causal and interleaving models is appearing also
in Game Semantics. In this setting, a strategy describes in an abstract way
the operational behaviour of a term. In the standard approach, a strategy is described by sequences of actions (plays), which represent the traces
of the computation. However, there is an active line of research in Game
Semantics aiming at relaxing sequentiality, either with the purpose to have
“partial order” models of programming languages or to capture concurrency [AM99, Mel04, HS02, MW05, SPP05, FM05, CF05, Lai05, GM04]. The
underlying idea is to not completely specify the order in which the actions
should be performed, while still being able to express constraints. Certain
tasks may have to be performed before other tasks; other actions can be
performed in parallel, or scheduled in any order. A strategy of this kind can
be presented as a directed acyclic graph.
Confusion free event structures and linear strategies We are interested in relating strategies and event structures. Abramsky, Mellies, Schalk
have already used event structures in Game Semantics as arenas (i.e. types,
or objects). However, our aim is to see event structures as strategies (i.e. as
morphisms).
We focus on the class of linear strategies, i.e. strategies which correspond
to the multiplicative-additive structure of Linear Logic. Linear strategies (as
deﬁned in [Gir01] and then [FM05]) can be described as partial orders with
a conﬂict relation, i.e. as a sort of event structures, which satisfy a number
114
A Graph Abstract Machine Describing Event Structure Composition
of conditions. In particular, they are confusion free. Many of the properties which make the composition work appear to depend only on confusion
freeness .
Our aim is therefore to see confusion free event structures as a generalization of strategies, and the composition of such event structures as strategies
composition.
An idea which underlies the work on types by Honda and Yoshida is that
typed processes should be seen as a sort of Hyland-Ong strategies; this is
implicit also in [VY06], on which our work builds.
In [VY06], Varacca and Yoshida provide a typing system which guarantees that the composition of confusion free event structures is confusion free.
The typing is inspired by Linear logic and Hyland-Ong strategies, and allows
the authors to give an event structure semantics for (a variant of) Sangiorgi’s
πI-calculus.
In this paper we deﬁne composition “operationally”, in such a way that
when restricted to strategies the machine implements strategies composition.
Applied to confusion free event structures, the result is the same as the
composition obtained in a more standard way. In particular, we prove the
equivalence with the composition in [VY06].
We believe that the machine provides a simple and direct implementation
of event structures composition.
A.2
A.2.1
Background
A sketch of strategies composition
In Game Semantics, the execution of a program is modelled as interaction
between two players; let us call them P (Proponent) and O (Opponent).
The role of a strategy is to tell the player how to respond to a counter-player
move. The dialogue between the two players will produce an interaction (a
play).
Figure ?? presents a simpliﬁed example of two (sequential) strategies. A
speciﬁc move is played by (belongs to) only one of the players, so there are
P-moves and O-moves. The active (positive) move of P are those that P
plays, while its passive (negative) moves are those played by O, and to which
P has to respond. In the picture, for each player strategy we distinguish the
actives (positive) moves, i.e. those which belong to that player, with circles.
Background
115
Let us look at the strategies (1). According to the P-player strategy, it
will start with b0 , then respond with a0 to Opponent move b1 , and with †
(termination) to Opponent move b2 . Let us make it interact with the Oplayer strategy. The interaction goes as follows: O answer to b0 is b1 , P
answer to b1 is a0 , O answer to a0 is a1 , and so on.
The algorithm to calculate the interaction is simple. (i.) Start from Pplayer initial move, (ii.) Check counter-player answer to that move, that is,
go to the corresponding opposite action, and take the following move. (iii.)
Repeat step (ii.) until terminating on †.
Figure A.1 illustrates the same ideas for more parallel strategies [FM05].
Interaction :
Strategies :
Player:
Opponent:
†
b3
a1
a0
b1
b2
b0
b3
a1
a0
†
b2
b2
..
.
b1
b0
b3
a1
a0
..
.
b1
b0
Figura A.1: Graph strategies
The strategies are here graphs. The way to make them interact is similar
to the previous one, but (1.) there are several threads running in parallel,
(2.) on certain moves we need to synchronize.
116
A Graph Abstract Machine Describing Event Structure Composition
A.2.2
Event structures
Event structures were introduced by Nielsen, Plotkin, and Winskel [NPW81,
Win87, WN95], as a theory combining Petri nets and domain theory.
Let E, ≤ be a partially ordered set. Elements of E are called events; we
assume that E is at most countable. The order relation is called causality
relation.
The downward closure of a subset S ⊆ E is deﬁned by S
= {e : e ≤
e, e ∈ S}. For a singleton, we write e
.
An event structure1 is a triple E, ≤, such that
• E, ≤ is a partial order, as above;
• For every e ∈ E, e
is ﬁnite.
• is an irreﬂexive and symmetric relation, called conﬂict relation,
which satisﬁes the following:
for every e1 , e2 , e3 ∈ E, if e1 ≤ e2 and e1 e3 then e2 e3 .
If e1 ≤ e2 we say that the conﬂict e2 e3 is inherited from the conﬂict
e1 e3 . If a conﬂict is not inherited, we say that it is immediate, written
µ
Causal order and conﬂict are mutually exclusive.
With a slight abuse of notations, we identify an event structure E, ≤, and its set E of events.
A labelled event structure is an event structure E together with a labelling
function λ : E → L, where L is a set of labels.
Conﬂict free A set S ⊆ E is conﬂict free if it does not contain any two
elements in conﬂict; in particular, an event structure E is conﬂict free if its
conﬂict relation is empty.
Hence, a conﬂict free event structure is simply a partial order.
Observe that, if e ∈ E, then e
is conﬂict free.
1
In this paper we say event structures always meaning prime event structures.
Background
117
Parents and enabling set. Let us introduce two notations that will be
useful.
Given e ∈ E
• Parents(e) denotes the set of immediate predecessors of e w.r.t. ≤ (the
preconditions of that event);
• [e) = e
\ {e} is the enabling set of e.
A.2.3
Confusion free event structures
Confusion free event structures are a class of event structures where every
choice is localized to cells, where a cell is a set of events that are pairwise in
immediate conﬂict, and have the same enabling set.
Deﬁnition A.2.1 (Cell). A cell c is a maximal set of events such that
e, e ∈ c implies e m e and [e) = [e ).
Deﬁnition A.2.2 (Confusion free). E is confusion free if the following
holds:
(a.) for all distinct e, e , e ∈ E, e µ e and e µ e implies e µ e
(b.) for all e, e ∈ E, e µ e implies [e) = [e )
The notion of cell express the idea that choices are local.
Example.
Below, we give an example (1.) of event structure which is confusion free,
and an example (2.) of an event structure which is not. Waved lines denote
conﬂict. The event structure in (2.) is not confusion free because t4 is in
conﬂict with t2 , t3 , but fails to have the same parents.
(1.) Senza confusione
t3
t4
(2.) Confusione
t5
t3
t4
t2
t2
t1
t1
t5
118
A Graph Abstract Machine Describing Event Structure Composition
The intuition behind. Let T = {t1 , t2 , t3 , t4 , t5 } be a set of tasks on
which an order (propedeuticity) and a conﬂict relation are deﬁned. We have
to schedule them.
In the confusion free case (1.), the scheduler must start with t1 . Then the
situation is the following:
• after t1 , the scheduler can choose t5 or either one of t2 , t3 , t4 .
• if the scheduler choose t1 and then one of t2 , t3 , t4 , then it can still
schedule t5 .
• if the scheduler choose t1 and then t5 , then it can still choose to schedule
either of t2 , t3 , t4 .
The case (2.), instead, describe a state which is confused: changing the
scheduling of the tasks, some choices which were available may be no longer
available.
If we look at the picture, we see that both t1 and t4 have no precondition,
and hence can be scheduled ﬁrst. After t1 , we can schedule either of t2 , t3 , t4
if we start with t1 . However, if we schedule t4 ﬁrst, and then t1 , after t1 the
choices t2 , t3 are no longer available.
Proof-theoretical intuition A cell, being a set of events in conﬂict and
with the same preconditions, closely correspond to the notion of additive
choice in Linear Logic.
A.3
Typed event structures
In this section we introduce a notion of labelled event structure, where the
labelling guarantees that the composition of confusion free event structures
is a confusion free event structure.
Our labelling can be seen as a minimalist variant of the typing in [VY06],
without the whole setting of linear types and morphisms; this because here we
are only interested in the preservation of confusion freeness via composition.
Our labelling is indeed a straightforward generalization of the technique
developed in [Gir01] to deal with additive strategies.
A key features of the labelling is that a name identiﬁes a cell (rather than
a single event).
Typed event structures
A.3.1
119
Names and actions.
We assume a countable set of names N, ranged over by α, β, . . . . We are
going to label a confusion free event structure with actions on these names.
Let S be an index set. We deﬁne the alphabet N as follows:
N=
Ni = {(α, i) : α ∈ Nand i ∈ S}
i∈S
We say that a = (α, i) uses the name α, and also write name(a) = α.
A (polarized) action is given by an element a ∈ N and a polarity, which
can be positive (a+ ), negative (a− ), or neutral (a± ).
Remark A.3.1. Actions of opposite polarity (a+ , a− ) denote matching dual actions, such as c and c in CCS, or Player/Opponent moves in Game
Semantics.
We think of a± as a pair of matching actions a+ , a− which have synchronized. A more traditional and suggestive denotation for a± would be
τa .
We use the variable to vary over polarities: ∈ {+, −, ±}. When
clear from the context, or not relevant, we omit the explicit indication of the
polarity.
The polarities + and − are said opposite. If a is a positive or negative
action, a will denote its opposite action.
A.3.2
Interfaces.
We are going to type event structures with an interface. The interface provides in particular the set of names on which the event structure communicate, and their polarity.
An interface A, πA is given by a ﬁnite set of names A, and a polarity
(positive, negative, neutral) for each name. The polarization partitions A
into three disjoint sets: positive, negative and neutral names.
Remark A.3.2. The positive names can be thought of as sending, the negative name as receiving, and the neutral names as private.
The interface (A, π) generates the set of actions A = i∈S Ai = {(α, i) :
α ∈ A}. The polarization of the names extends to the actions with that
name.
120
A Graph Abstract Machine Describing Event Structure Composition
A.3.3
Typed event structures.
An event structure of interface A is a tuple E, A, λ, π where
• E is an event structure;
• A = (A, πA ) is an interface;
• λ : E → {(α, i) : α ∈ A, i ∈ S} is a labelling function;
• π : E → {+, −, ±} is the polarization induced on the actions by πA .
If λ(e) = (α, i), we say that the event e uses the name α, and write
name(e) = α.
Remark A.3.3. If λ(e) = a, with a = (α, i), and πA (α) = , then e is
labelled by the action a .
We type an event structure of interface A only when it is confusion free;
we ask that:
• all the events in the same cell use the same name (and hence also have
the same polarity).
• two events which use the same name (and the same polarity) are in
conﬂict.
Deﬁnition A.3.4. An event structure E of interface A has type A, written
E : A if it satisﬁes the following, for all distinct e1 , e2 ∈ E.
1. if e1 µ e2 and λ(e1 ) = (α, i), then λ(e2 ) = (α, j), with i = j.
2. if name(e1 ) = name(e2 )then e1 e2 .
3. e1 µ e2 ⇒ Parents(e1 ) = Parents(e2 )
Remark A.3.5. E can receive a type if and only if it is confusion free.
Properties 1. and 2. imply A.2.2.i; property 3. is equivalent to A.2.2.ii.
A.3.4
Properties of the labelling
Given a labelled event structure E, and a set of events S ⊆ E, we use the
notation λS = {λ(s)|s ∈ S}.
Typed event structures
121
Set of labels identify events
Each event e ∈ E is uniquely identiﬁed by the set of labels λ e
= {λe , e ≤
e}.
Proposition A.3.6. Given e1 = e2 ∈ E, we have that λ e1 = λ e2 Conﬂicts
The conﬂict relation in typed event structures can be inferred from the labels:
Proposition A.3.7. Let E : A a typed event structure and let e1 , e2 ∈ E.
Then the following holds:
(∗∗) e1 e2 ⇐⇒ ∃e1 ≤ e1 , e2 ≤ e2 : name(e1 ) = name(e2 )
Since in a typed event structure the labels carry all the information on
the conﬂict relation, from now on, we deal with the conﬂict implicitly: two
distinct events e1 and e2 are in conﬂict iﬀ (**) holds.
This allows us to only focus on the partial order.
It is easy to see that
Proposition A.3.8. Given e1 = e2 ∈ E : A, we have that e1 µ e2 iﬀ
• e1 , e2 use the same name
• [e1 ) = [e2 )
Typed event structures as dag’s
As seen in the previous section, given a typed event structure, we can deal
with the conﬂict implicitly; we are left to deal only with the partial order
E, ≤.
In the following, it will be convenient to identify the partial order on E : A
with the associated dag. This in particular allows us to describe composition
in terms of graph rewriting.
A directed acyclic graph (dag) G is an oriented graph without (oriented)
cycles. We will write c ← b if there is an edge from b to c. It is standard
to represent a strict partial order as a dag, where we have a (non transitive)
edge a ← b whenever there is no c such that a < c and c < b. Conversely
(the transitive closure of) a dag is a strict partial order on the nodes.
In the following, we will identify the partial order on E : A with the
associated dag. We take as canonical representative of E its skeleton (the
minimal graph whose transitive closure is the same as that of E).
122
A Graph Abstract Machine Describing Event Structure Composition
Remark A.3.9. Observe that, by construction, the skeleton is always deﬁned, even if E can have a countable number of events (in particular, a cell
can have a countable number of events). In fact, for each event e ∈ E, e
does not contain any conﬂict, and it is ﬁnite.
A.4
Composition
We deﬁne composition “operationally”, in such a way that when restricted
to strategies this procedure produces strategies composition.
Composition between event structures relies on two notions: synchronization and enabling (reachability). Intuitively, to compose, we synchronize
(match) events which are labelled by the same action, and opposite polarity. The synchronization is possible only between events which have been
enabled. We enable (reach) an action only if all the actions before it have
been enabled (reached). We better illustrate this in Section A.4.2.
A.4.1
Compatible interfaces
We compose two event structures when their interfaces are able to communicate.
Deﬁnition A.4.1 (Compatible interfaces). Let A, πA and C, πC be
two interfaces. The interfaces A and C are compatible if
for all b ∈ A ∩ C, the polarity of b in A is opposite to the polarity of b in C.
If the interfaces are compatible, we
A ∪ C, π where
⎧
⎨ πA (α)
πC (α)
π(α) =
⎩
±
deﬁne their composition A & C =
if α ∈ A \ C
if α ∈ C \ A
otherwise
Deﬁnition A.4.2 (Private and public names). Given two compatible
interfaces A, C, we say that the name α is private if α ∈ A ∩ C, public
otherwise.
Example. If A = {a− , b+ } and C = {b− , c+ }, then A & C = {a− , c+ , b± }.
The name b is private, while the names a, c are public.
Composition is only deﬁned on event structures which have compatible
interfaces.
Composition
A.4.2
123
Conﬂict free composition
Let us ﬁrst analyze composition in the case of conﬂict free event structures,
i.e. when no two events are in conﬂict. This case is very simple and clear,
but contains all the dynamics of the general case.
The key property of this case is the following
If E : A is conﬂict free, no two events use the same name.
Through this section, let us assume that E1 : A and E2 : C are conﬂict
free and have compatible interfaces. Their composition E1 E2 is a conﬂict
free event structure of interface A & C.
Let us describe the composition by means of a wave of tokens travelling
up on E1 E2 . When a private action is reached, to continue, it is necessary to synchronize it with an action of opposite polarity. Observe that, by
construction, there is at most one such action.
Remark A.4.3. In E1 E2 there is only one occurrence of each polarized
action. For this reason, in this section, we can identify each event with the
polarized action which labels it.
1. If a is public, and its parents have been enabled, then a is enabled. We
illustrate this in the picture below, where the squares mark the enabled
nodes.
→
a
a
2. If a is private, a+ , a− are both present, and their parents have been
enabled, then a is enabled, and the graph is transformed as follows:
a
a
→
τa
end: The actions which have not been enabled are deleted (garbage collection).
124
A Graph Abstract Machine Describing Event Structure Composition
The process described above generates a new conﬂict free event structure
E, ≤, where E is a set of events labelled by the actions which have been
enabled; the actions have the polarity induced by the new interface A & C.
It is straightforward to give a direct recursive deﬁnition of E1 E2 . We
do not do this in this Section, but in Section A.4.5 we use a deﬁnition of
this kind to describe composition in the general case, and to establish the
equivalence of our procedure with more standard deﬁnitions.
A.4.3
Local rewriting rules
The process described in Section A.4.2 can be expressed by means of a set
of local graph rewriting rules on E, which we describe in FigureA.4.3.
Private a:
1. There are a, a, parallel
a
a
→
τa
2. Otherwise:
a
→
Figura A.2: Graph Rewriting Rules
It is straightforward to show these rules are conﬂuent. By using this fact,
one can prove associativity for the composition.
Proposition A.4.4 (Associativity). Let E1 : A, E2 : C, E3 : D be conﬂict
free event structures. If the interfaces allow the composition, we have that
(E1 E2 )E3 = E1 (E2 E3 )
A.4.4
Reducing composition to conﬂict free composition
A confusion free event structures E can be seen as a superposition of conﬂictfree event structures (which we call the slices of E). The study of confusion
Composition
125
free event structures can be reduced to the study of conﬂict free event structures. In particular, composition of confusion free event structure can be
reduced to the composition of its slices.
Slices
A slice S of E is a downward closed, conﬂict free subset of E, with the order
induced by E.
To choose a (maximal) slice of E corresponds to the selection of a single
element in each cell of E.
Studying composition by slices
A key feature of the composition is that it takes place independently inside
each single slices (Proposition A.4.10) .
Several interesting properties of the composition of two event structures
(such as conﬂuence, or deadlocks) can be analyzed as properties of their slices
(see A.4.9).
Actually, following an approach which is well studied for proof nets and
linear strategies, the process of composition itself could be reduced purely to
conﬂict free composition:
• decompose E into its slices
• compose all slices pairwise
• superpose the composed slices
Proposition A.3.6 allows us to perform the superposition, by using the same
technique developed in [Gir01, FM05].
We do not give details here; however, after providing a direct description
of composition in the general case, we show that the study of the composition
can be reduced to the study of conﬂict free composition (Proposition A.4.10).
A.4.5
Global composition
In this section, we provide a direct description of composition of typed event
structures, in the general case.
Let E1 : A and E2 : C be typed event structures with compatible interfaces. E1 E2 is an event structure of interface A & C, obtained as follows.
126
A Graph Abstract Machine Describing Event Structure Composition
Case 1. Let e ∈ Ei such that λ(e) = a and name(a) is public.
If S ⊆ E satisﬁes the following conditions:
parent condition: λS = λ[e).
conﬂict condition: the set S is conﬂict free
add to E an event v such that
label: λ(v) = a
edges: for all vi ∈ S
we have vi ← v
Case 2. Let e1 ∈ E1 and e2 ∈ E2 such that λ(e1 ) = λ(e2 ) = b and name(b)
is private.
If S = S1 ∪ S2 where S1 , S2 ⊆ E satisfy the following conditions
parent condition: λS1 = λ[e1 ), λS2 = λ[e2 ).
conﬂict condition: the set S is conﬂict free
add to E an event v such that
label: λ(v) = b (this should be thought as τb , since π(b) = ± )
edges: for all vi ∈ S
we have vi ← v
Remark A.4.5. The parent condition checks that the enabling set of e ∈
Ei has been considered, and relies on Proposition A.3.6.
Remark A.4.6. The conﬂict condition says that in S
there are no two
events using the same names (we are using Proposition A.3.7. )
The conﬂict condition, essentially guarantees that we are working slice by
slice, i.e. independently in each slice (see Proposition A.4.10)
The machine generates E = E1 E2 step by step; each time we add to E an
event v which refers to [comes from] an event (or a pair of matching events)
x in E1 E2 . We add v to E only if:
• the enabling set of x has already an “image” in E;
• this image is conﬂict free.
To understand the conﬂict condition, remember that events in conﬂict
are events which are mutually exclusive. If we need a set of precondition to
occur together, they must live in a conﬂict free event structure S ⊆ E.
In fact, we can analyze, and even calculate, composition, only by means
of conﬂict free event structures, as we see in Section
Composition
127
Example of composition
Consider the following event structures
• E1 = {e1 , e2 , e3 , e4 } with e1 < e3 , e2 < e4 and e1 µ e2 .
• E2 = {e5 , e6 } with e5 < e6
and the interfaces A = {α− , β − } and C = {β + , γ − }.
We abbreviate (α, i) into ai , and similarly use bj , ck for actions on β, γ.
Let us consider
• E1 : A with λ(e1 ) = a1 , λ(e2 ) = a2 , λ(e3 ) = λ(e4 ) = b1
• E2 : C with λ(e5 ) = b1 , λ(e6 ) = c1 .
Here is a graphical representation of the two event structures:
e3
b1
e1
a1
e4
b1
a2
E1
e2
e6
c1
e5
b1
E2
And here we run the machine:
E 1 E 2
∅
e1 ∈ E 1
name(λ(e1 )) ∈ A
S =∅
v1
a1
v1
v3
v6
c1
v3
τb
v4
τb
v1
a1
a2
v2
v2
a2
name(λ(v1 ) = name(λ(v2 ))
e3 ∈ E 1 e5 ∈ E 2
λ(e3 ) = λ(e5 ) = b1
S1 = {v1 } S2 = ∅
v5
c1
v3
τb
a1
v1
e6 ∈ E 1
name(λ(e6 )) ∈ C
S = {v3 , v1 }
v3
τb
v4
τb
a2
v2
v4
τb
τb
a1
v1
c1
e6 ∈ E 1
name(λ(e6 )) ∈ C
S = {v2 , v4 }
e2 ∈ E 1
name(λ(e2 )) ∈ A
S =∅
a1
v5
a2
v2
e4 ∈ E 1 e5 ∈ E 2
λ(e4 ) = λ(e5 ) = b1
S1 = {v2 } S2 = ∅
a1
v1
a2
v2
128
A Graph Abstract Machine Describing Event Structure Composition
Composition is well deﬁned and associative
Composition of typed event structures produces a typed event structure.
Moreover, composition is associative.
Theorem A.4.7. E1 E2 : A & C
Dimostrazione. W.r.t. deﬁnition A.3.4, conditions 1. and 2. (the properties
of the labelling) hold by construction. We have to verify 3., i.e. that u µ v
implies [v) = [v). Let Su , Sv the two subset of the labelled parent condition.
[u) = [v) if and only if Su = Sv . By labelling we have that name(λ(u)) =
name(λ(v)) public or private. We develop the public case: the other is
analogous. Without loss of generality we can assume name(λ(u)) ∈ A. Hence
there exists e, d ∈ E1 such that λSu = λ[e) and λSv = λ[e). We have that
e µ d: this holds (by 1. and 2.) and this conﬂict cannot be inherited
because otherwise also u v should be inherited. Hence we have λSu = λSv
by confusion freeness of E1 and as immediate consequence of Proposition
A.3.6, we have Su = Sv , as required.
Remark A.4.8. As a consequence, composition of confusion free event structures is confusion free.
Proposition A.4.9 (Associativity). Given E1 : A, E2 : C, E3 : D, if the
interfaces allow the composition, we have that
(E1 E2)E3 = E1 (E2E3 ) =
Dimostrazione. The result follows from Proposition A.4.4 and Proposition
A.4.10.
Working by slices
Proposition A.4.10 (Slices). Let E = E1 : AE2 : C. We have the
following.
• If S ⊆ E is a slice of E, then there exist two slices S1 ⊆ E1 and S2 ⊆ E2
such that S = S1 : AS2 : C.
• If S1 ⊆ E1 and S2 ⊆ E2 are slices, then S = S1 S2 is a slice of E.
By reducing composition to composition of conﬂict free event structures,
we can easily prove associativity.
Discussion
129
A.5
Discussion
A.5.1
Relating with standard event structure composition
In this section we want to argument that the abstract machine we have
deﬁned produces the same result as a “standard” approach to event structure
composition. To do this, we choose a speciﬁc synchronization algebra, which
is that deﬁned in [VY06].
The typing deﬁned by Varacca and Yoshida guarantees that the composition preserves confusion freeness, and allows the interpretation of a linear
fragment of the π calculus.
The labelling induced by their typing is easily seen as a case of the
labelling we deﬁne here, hence in particular we can apply our machine.
We have that
Proposition A.5.1. If E1 , E2 are confusion free event structures typed in
the sense of [VY06], they are also typed in the sense deﬁned here, and their
composition E1 E2 as deﬁned here is isomorph to the parallel composition as
deﬁned in [VY06].
The details are given in [Pic06]
Let as brieﬂy resume what a “standard approach” looks like.
Parallel composition of event structures
A more standard deﬁnition for the parallel composition of event structures
is that used [VY06], based on the following ingredients:
1. ﬁx through a synchronization algebra the events which will synchronize
and those which will not. Two events synchronize if they have dual
labels (for example one event has label a and the other a);
2. build the categorical product of the event structures
3. discard some events, and everything above them:
(a) discard all the events of the product which are generated from
pair which are not able to synchronize because they do not have
matching labels
(b) discard all the events of the product which are generated from a
single private event: these are events which are private but not
“consumed”.
130
A Graph Abstract Machine Describing Event Structure Composition
A.5.2
Linear strategies with parallel composition are
a sub-class of typed event structures
Linear strategies as introduced in [Gir01] and extended to dag’s in [FM05]
are labelled dag’s. The labels are taken in
Ni = {(α, i) : α ∈ Nand i ∈ Pf in (N)}
i∈Pf in (N)
where N are the strings of natural numbers.
The labelling satisﬁes a certain discipline, which in particular satisﬁes all
the constraints in Deﬁnition A.3.4.
As for composition, the machine introduced here extends the LAM machine deﬁned in [Fag02, FM05] to implement the composition of linear strategies. The new machine has the same behaviour of the LAM when restricted
to strategies. This in particular means that there is a morphism from strategies to typed event structures, which preserves the parallel composition.
More precisely, strategies composition decomposes into parallel composition plus hiding, where parallel composition is the operation we have described here, and the hiding concerns the τ actions.
A.5.3
More comments and future work
The dynamics The machine we have presented makes it immediate what
is going on when composing two labelled event structures E1 , E2 : we merge
together the structure (events, order and conﬂicts) of E1 , E2 to create a new
event structure E. The dynamics appears the same as that which takes place
when composing strategies, λ-terms or Linear Logic proof-nets.
Bridging Game Semantics and event structures. In future work, we
plan to use event structure as a guide to generalize the deﬁnition of strategies.
We hope to build on the work on event structures to extend the approach
of Game Semantics, in order to deal with non determinism, concurrency and
process calculi.
Event structures and proof-nets This work meet also another line of
research, which is bringing together graph strategies and proof-nets. Proofnets are a graph representation of proofs introduced by Girard in Linear
Logic [Gir87] and which are powerful tool for the analysis of normalization.
Discussion
131
In particular, they have been a fertile tool in the study of functional programming, in particular for optimization. Observe that proof-net normalization
is performed via local rewriting rules.
We see event structures as a form of multiplicative-additive proof-nets,
and hope to be able to apply some of the technology developed for proofnets. For example, a key notion in proof-nets is that of correctness criterion,
which states that there are no cyclic path, for a certain deﬁnition of path
which is sensitive to the polarity of the nodes. The correctness criterion has a
crucial role in guaranteeing that the normalization (composition) works, and
in fact it guarantees that there are no deadlocks. We intend to investigate if
a similar notion could be used on event structure, for an opportune typing,
to guarantee that there are no deadlocks.
Acknowledgments
This work was motivated from discussion with Nabuko Yoshida and Daniele
Varacca.
We are in debt with Daniele Varacca for many explanations, comments,
and suggestions. We are grateful to Martin Hyland, Emmanuel Beﬀara, and
Pierre-Louis Curien for interesting discussions.
We also wish to thank the referees for many usefull remarks and suggestions.
RINGRAZIAMENTI
Questo è il capitolo più importante della mia tesi, checché ne dicano dotti e tonti.
Ringrazio anzitutto la mia relatrice Claudia Faggian per tutti gli aiuti, i consigli, le opportunità e
l’assistenza che mi ha dato (e per avermi sopportato, nel bene e nel male). Ringrazio inoltre il mio
co-relatore Daniele Varacca, il cui apporto a questa tesi è stato fondamentale.
Ringrazio inoltre tutti i componenti del laboratorio PPS di Chevaleret a Parigi, in particolare Ugo
dal Lago, Fabio Mancinelli, Luca Fossati, Giulio Manzonetto, Emmanuel Beffara, Russ Harmer,
l’olandese compagno di ufficio di Fabio di cui non mi ricordo il nome, eccetera eccetera. Ringrazio
Pierre-Louis Curien che mi ha dato la possibilità di lavorare a Parigi 7. Ringrazio l’ufficio 5A16,
del quale ho potuto vantarmi presso i miei amici padovani. Ringrazio inoltre Paolo di
Giamberaldino, il quale mi ha dato una settimana di vita sociale parigina. Un ringraziamento
particolare va alla macchinetta del caffè del sesto piano che mi ha sostenuto nei momenti di
sconforto e stanchezza nella redazione della tesi.
Ringrazio inoltre tutti i Bruxellesi compagni di ufficio di mia sorella e compagni di appartamento.
In particolare ringrazio Sara per avermi fatto innamorare anche se poi non ho concluso niente.
Per i miei viaggi, ringrazio Trenitalia, Ryan Air, My Air, SNCF, Germanwings e Thalyss.
Di quel di Padova, ringrazio anzitutto la segreteria didattica dell’Università, che al modico prezzo di
una giornata infernale e colma di umiliazione, ha acconsentito di soprassedere ad una mia
popotaggine e di permettere la mia laurea.
Ringrazio quindi tutti i miei parenti, mamma Fiorenza, papa Giancarlo, Claudio, Mara, gli zii, i
cugini, i nonni e tutti i professori del corso di laurea in informatica.
And last but not least tutti i miei amici, in particolare il Macca, Giulio, Arturo, Mahesh, Alberto,
Milo, Riccardo, Matteo, Marco e Marco, Elisa, Silvia, Nicodemo, il Peroni, Jari, Stefania, Valentina
e tutti quelli che avrei dovuto ringraziare e che non sono qui nominati.
Scarica
un ponte fra teoria della concorrenza e semantica dei giochi

Diapositiva 1

un ponte fra teoria della concorrenza e semantica dei giochi

Diapositiva 1

Scarica la presentazione in Power Point dell` Event Recorder

AVVISO n.10640 - Societe Generale

4 - La gestione degli eventi

Present Perfect

EstrazioneTerminologia - Università degli Studi di Roma Tor
