Metodi Formali dell'Informatica - a.a. 1999/00

Registro delle Lezioni

Le lezioni sono tenute da Moggi se non altrimenti specificato.
  1. 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;
  2. 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.
  3. 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);
  4. 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.
  5. 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].
  6. 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).
  7. 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.
  8. 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).
  9. 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.
  10. 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.
  11. 30/11/99 (1h). Dimostrazione della "type preservation" e proprieta' aggiuntive del type system. Termini con informazione di tipo e variante del type system.
  12. 01/12/99 (2h). Semantica CBN, Programmi (ben tipati), osservazioni e congruenza osservazione.
  13. 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.
  14. 07/12/99 (1h). Esercizi su semantica operazionale.
    08/12/99 (vacanza).
  15. 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.
  16. 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.
  17. 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.
  18. 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.
  19. 21/12/99 (1h). Esercizi su semantica operazionale.
  20. 22/12/99 (2h). Esercizi su semantica operazionale.
  21. 11/01/00 (1h+2h). compitino su semantica operazionale
  22. 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.
  23. 14/01/00 (2h). Assiomi equazionali per i tipi computazionali, ed esempi di interpretazione. Proprieta' della traduzione rispetto alla sostituzione.
  24. 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. 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

  26. 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.
  27. 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.
  28. 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.
  29. 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.
  30. 20/03/00 (3h). compitino su semantica denotazionale
  31. 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.
  32. 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)

  33. 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'.
  34. 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.
  35. 10/04/00 (3h). Eercizi su specifiche e sistemi di riscrittura.
  36. 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

  37. 28/04/00 (2h)compitino su specifiche e sistemi di riscruttura
  38. 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.
  39. 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.
  40. 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.
  41. 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.
  42. 19/05/00 (2h). Alternating bit protocol: formalizzazione in CCS e dimostrazione di correttezza.
  43. 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.
  44. 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.
  45. 02/06/00 (2h). COMPITINO