Orario settimanale:
Mer 9-11, Ven 11-13 (I semestre),
Lun 10-13, Ven 11-13 (II semestre)
Registro delle Lezioni
Le lezioni sono tenute da Moggi se non altrimenti specificato.
03/11/99 (2h).
Definizioni induttive (vedi [Acz77, pp 739-745] e [Win93, Ch 3-4]):
insieme R-chiuso, insieme I(R) induttivamente definito e sua
caratterizzazione, albero di R-derivazione, R-induzione, induzione
sulla derivazione;
relazione ben fondata, definizione di funzione per induzione ben
fondata;
relazione <_R indotta da un insieme di regole, insieme di regole
deterministico e proprieta' di <_R;
05/11/99 (2h).
Definizioni induttive:
insieme di regole ben fondato (rispetto ad una relazione ben fondata)
e proprieta' di <_R; esempi.
Operatore monotono/continuo sui sottoinsiemi, caratterizzazione del
minimo punto fisso di un operatore continuo;
operatore continuo "conseguenza immediata" indotto da un insieme di
regole, caratterizzazione dei sottoinsiemi R-chiusi e di I(R) in
termini dell'operatore "conseguenza immediata".
R-derivazioni aperte ed "algoritmo" non-deterministico di ricerca di
una R-derivazione. Proprieta' dell'algoritmo di ricerca nel caso di R
deterministico e/o ben fondato.
10/11/99 (2h).
Sintassi e semantica operazione di IMP (vedi [Win93, Ch 2]):
sintassi astratta di IMP, dipendenza tra le categorie sintattiche;
dominio sematico degli stati, semantica operazione a grandi passi
delle espressioni, formalizzazioni di diverse strategie di valutazione
delle espressioni booleane, proprieta' della semantica operazionale
(dimostrabili per induzione sulla struttura delle espressioni);
semantica operazionale a grandi passi dei comandi, proprieta' della
semantica operazionale (dimostrabili per induzione sulla derivazione);
12/11/99 (3h).
Sintassi e semantica operazione di IMP (vedi [Win93, Ch 2]):
semantica operazionale a piccoli passi dei comandi, proprieta' della
semantica operazionale (dimostrabili per induzione sulla struttura dei
comandi).
Estensioni alla sintassi di IMP: espressioni con comandi e
ridefinizione della semantica operazionale; composizione parallela di
programmi, estensione della semantica operazionale a piccoli passi,
impossibilita' di una semantica operazionale a grandi passi.
Semantica operazione con errore: ridefinizione della semantica
operazionale, analisi statica (mediate regole ben fondate) per
identificare l'uso di variabili indefinite, correttezza dell'analisi
statica.
Esercizi: esempi di dimostrazioni di proprieta' della semantica
operazionale per induzione (ben fondata) sulla sintassi astratta o
sulle derivazioni.
16/11/99 (1h).
Esempi di dimostrazioni di proprieta' per induzione sulla derivazione:
univocita' del risultato per la semantica operazionale con asserzioni
mutuamente ricorsive (IMP con resultis), correttezza dell'analisi
statica rispetto alla semantica operazione con errore [da completare a
casa], corrispondeza tra semantica a piccoli passi e a grandi passi
[da fare a casa, anche in gruppo].
17/11/99 (2h).
Semantica denotazionale di IMP (vedi [Win93, Ch 5]):
Corrispondenza tra notazione BNF e segnature many-sorted. Segnature,
termini (chiusi), algebre, interpretazione dei termini in un algebra.
Segnatura per IMP e algebra per dare la semantica denotazionale
(problema della sematica dello while).
19/11/99 (2h).
Semantica denotazionale di IMP (vedi [Win93, Ch 5]):
cpo, funzione continua tra cpo, teorema del punto fisso per funzioni
continue; esempi di cpo; la semantica denotazionale di IMP usando cpo
e funzioni continue.
23/11/99 (1h).
Coincidenza della semantica operazionale (a grandi passi) e
denotazionaledi IMP, proprieta' del punto fisso dimostrate per
computational induction (induzione sulle approssimazioni).
24/11/99 (2h).
Confronto tra semantiche: osservazioni, computational adequacy,
contesti, congruenza osservazionale. Esempi di osservazioni:
terminazione, numero di passi. Coincidenza della terminazione per le
semantiche (operazione a grandi e piccoli passi, denotazionale) di
IMP. Coincidenza della equivalenza osservazionale e della equivalenza
denotazionale.
26/11/99 (2h).
Semantica operazionale linguaggio funzionale CBV (vedi [Win93, Ch 11]):
Espressioni, variabili libere, sostituzione (senza renaming), valori;
semantica operazionale CBV a grandi passi; univocita' della
valutazione.
Tipi, contesti, sistema (ben fondato) di assegnamento di tipo;
la valutazione rispetta il tipaggio.
30/11/99 (1h).
Dimostrazione della "type preservation" e proprieta' aggiuntive del
type system. Termini con informazione di tipo e variante del type
system.
01/12/99 (2h).
Semantica CBN, Programmi (ben tipati), osservazioni e congruenza
osservazione.
03/12/99 (2h).
Introduzione alla teoria delle categorie ([Ten91, Ch 8]):
definizione di categoria, terminologia e notazione; esempi di
categorie (Set, Rel, Cpo, Alg, pre-ordini, monoidi); categoria duale e
categoria prodotto; isomorfismo; oggetto terminale ed invarianza per
isomorfismo.
07/12/99 (1h).
Esercizi su semantica operazionale.
08/12/99 (vacanza).
10/12/99 (2h).
Introduzione alla teoria delle categorie ([Ten91, Ch 8], [Win93, Ch 8]):
nozione duale, proprieta' auto-duale degli isomorfismi, oggetto
iniziale (=duale di oggetto terminale), prodotti e somme. Descrizione
dei prodotti e somme in Set e Cpo.
14/12/99 (1h).
Introduzione alla teoria delle categorie ([Ten91, Ch 8], [Win93, Ch 8]):
esponenziali. Relazioni tra Cpo e Set: funtore dimenticante e funtore
inclusione, conservazione di prodotti/somme da parte del funtore
dimenticante/inclusione. Descrizione degli esponenziali in Set.
Descrizione degli esponenziali in Cpo, conservazione degli
esponenziali da parte dei funtore inclusione.
15/12/99 (2h).
Descrizione degli esponenziali in Cpo (completamento). Categorie
Cartesianamente Chiuse (CCC). Semantica denotazionale e Metalinguaggi.
Il lambda-calcolo (semplice) un metalinguaggio per CCC: sintassi e
interpretazione.
17/12/99 (2h).
Interpretazione dei termini ben tipati in una CCC con somme,
proprieta' distributiva. Semantica denotazionale mediante traduzione
in un metalinguaggio: motivazioni, passi della metodologia.
Esempi di segnature per metalinguaggio: naturali, liste, operatore di
punto fisso.
21/12/99 (1h).
Esercizi su semantica operazionale.
22/12/99 (2h).
Esercizi su semantica operazionale.
11/01/00 (1h+2h). compitino su semantica operazionale
12/01/00 (2h).
Tipi computazioni. Lifting e sue proprieta'.
Semantica denotazione CBV e CBN del linguaggio funzionale tipato
mediante traduzione in un metalinguaggio con tipi computazionali.
Proprieta' della traduzione rispetto al tipaggio.
14/01/00 (2h).
Assiomi equazionali per i tipi computazionali, ed esempi di
interpretazione. Proprieta' della traduzione rispetto alla sostituzione.
18/01/00 (1h+1h).
Proprieta' della interpretazione di PL dimostrate formalmente in ML.
Tipi ricorsivi e traduzioni CBV e CBN di HOFL non tipato.
19/01/00 (assenza docente). 21/01/00 (assenza docente).
25/01/00 (1h+1h).
Computational adequacy per la typed CBN denotational semantics.
26/01/00 (2h). CANCELLATA
28/01/00 (2h). CANCELLATA
INIZIO SECONDO SEMESTRE
06/03/00 (3h).
Esercizi: semantica denotazionale con errore, semantica denotazionale
con stato, semantica operazionale e denotazionale per input/output
in modalita' batche ed interattiva.
10/03/00 (2h).
Algebre con predicati (strutture del primo ordine) many-sorted: la
categoria delle segnature, la categorie delle algebra su una
segnatura, termini e formule, interpretazione in un algebra.
Invarianza della soddisfacibilita' di formule per iso.
Modelli di una specifica del primo ordine. Algebra iniziale dei
termini chiusi. Algebra term-generated. Sotto-algebra.
Caratterizzazioni alternative delle algebre term-generated:
mediante l'algebra iniziale, mediante la nozione di sotto-algebra.
13/03/00 (3h).
Accenni a Specifiche dei requisiti, specifiche design, raffinamento di
una specifica. Approccio loose ed approccio iniziale alla semantica
delle specifiche. Verita' minima e caratterizzazione dei modelli
iniziali e term-generated.
Costruzione di un modello iniziale term-generated per una classe C di
algebre. Sistemi deduttivi, soundness e completeness relative ad un
frammento (problema dei carrier vuoti). Specifiche condizionali,
sistema di Birkhoff e variante ristretta alle formule atomiche.
Completezza del sistema di Birkhoff, esistenza del modello iniziale
per specifiche condizionali.
17/03/00 (2h).
Logica equazionale (come restrizione del sistema di Birkhoff) e sua
completezza. Coppia usabile, relazione di riscruttura e relazioni
derivate. Proprieta' di confluenza. Relazioni tra riscrittura e
teoria equazionale in generale e nella ipotesi di sistema confluente.
20/03/00 (3h). compitino su semantica denotazionale
24/03/00 (2h).
Forme normali, proprieta' di terminazione, esistenza/unicita' delle
forme normali per un sistema di riscrittura terminante/confluente.
Caratterizzazione e decidibilita' della teoria equazionale nella
ipotesi di sistema terminante e confluente. Il modello iniziale delle
forme normali. Tecnica per dimostrare la terminazione
mediante una misura a valori nei naturali.
27/03/00 (3h). La nozione di coppia critica, unificazione ed mgu. I
sistemi ortogonali, la riscrittura in parallelo, e confluenza per i
sistemi ortogonali. Esempi e contro-esempi di sistemi ortogonali.
31/03/00. assenza (per ETAPS)
03/04/00 (3h).
Teoremi di Newman e Knuth-Bendix. Esercizi su sistemi di riscrittura.
Logica combinatoria (CL) come teoria equazionale, algoritmi di
astrazione in CL e loro proprieta'.
07/04/00 (2h).
strutture applicative parziali, algebre combinatorie parziali (pCA),
uguaglianza di Kleene. Modelli operazionali, modelli iniziali,
struttura di Kleene.
Algoritmo di astrazione per pCA. Algoritmi di astrazione e
sostituzione. Codifica di tipi di dato in una pCA: booleani, coppie,
naturali.
10/04/00 (3h).
Eercizi su specifiche e sistemi di riscrittura.
14/04/00 (2h).
Realizzabilita': categoria dei D-set, proprieta' dei D-set e codifiche
in pCL. Combinatori di punto fisso in CL.
Rappresentazione delle funzioni parziali calcolabili in CL
(indecidibilita'). Estensioni di CL e pCL: test di uguaglianza,
estensionalita'.
17/04/00. concorso
28/04/00 (2h)compitino su specifiche e sistemi di riscruttura
05/05/00 (2h). Modalita' di interazione tra sistemi concorrenti
(memoria condivisa - scambio di messaggi, comunicazione: sincrona -
asincrona, punto a punto - broadcast). Label Transition Systems (LTS)
ed esempi di descrizione sistemi interattivi:
cella di memoria, buffer di capacita' limitata, implementazione di
k-buffer componendo k 1-buffer.
Il CCS puro: sintassi, semantica operazionale (LTS), costrutti
dinamici e statici.
08/05/00 (3h).
CCS puro con costanti ricorsive o costrutto fix. LTS e relazioni
derivate. Rappresentazione di LTS in con agenti CCS (costrutti
dinamici). Riformulazione in CCS di esempi di LTS. Costrutti statici
e composizione di sistemi: implementazione di un k-buffer.
CCS value-passing (con espressioni aritmentiche e booleane), sintassi,
semantica operazionale, traduzione in CCS puro.
12/05/00 (2h).
Esercizio: rappresentazione di IMP in CCS.
Relazione di bisimulazione forte ed equivalenza forte per un LTS, e
loro proprieta'. Caratterizzazione della equivalenza forte come
massimo punto fisso. Tecnica di dimostrazione basata sulla
bisimulazione. Equivalenza forte nel caso di LTS a stati finiti.
15/05/00 (3h).
La equivalenza forte per il LTS del CCS e' una congruenza (rispetto
agli operatori del CCS). Congruenza forte per espressioni con
variabili.
Eccessivo potere discriminante della equivalenza forte:
equivalenza debole, congruenza debole.
Equivalenza tra specifica ed implementazione di un buffer.
19/05/00 (2h).
Alternating bit protocol: formalizzazione in CCS e dimostrazione di
correttezza.
22/05/00 (3h).
Varianti dell'alternating bit protocol: medium di capacita' 1 con
perdita di bit, medium di capacita' 1 senza perdita di bit.
Esercizi sul CCS.
26/05/00 (2h).
Corrispondenza tra lambda calcolo e logica combinatoria con
estensionalita'.
Semantica semplice e quoziente per i tipi, relazioni con la
realizzabilita', regole di sottotipaggio.