Laurea e Diploma in Informatica

Corso di Metodi Formali dell'Informatica (IV anno) - a.a. 1998/99

• Ultima modifica: 29 Gennaio 1999
• Docente: Prof. Eugenio Moggi (email moggi@disi.unige.it)
• Orario (I semestre): Mer 11-13, Ven 11-13 (Aula 711) - inizio Venerdi' 06/11/1998
• Orario (II semestre): Lun 14-16, Gio 11-13 (Aula 710) - inizio Lunedi' 08/03/1999
• Informazioni generali: Prerequisiti, Obiettivi, Programma, Testi di Riferimento
• Informazioni on line: registro delle lezioni, note,
• Lista degli studenti
• ESAMI (VEDI e-mail di COSTA): situazione voti, compitino del 26/02/1999, Testi e soluzioni di esami precedenti

Prerequisiti

Obiettivi

Modalita' degli esami

Programma

• tipi di dato astratti (e richiami di LM):
  • strutture eterogenee totali (algebre totali): sintassi (segnatura,termini,formule), semantica (modelli ed interpretazione di termini e formule)
  • specifiche dei requisiti (loose)
  • sistemi deduttivi: soundness e completeness (relativamente ad un frammento)
  • specifiche design: modello iniziale, condizioni per l'esistenza del modello iniziale
  • regole di riscrittura: confluenza, normalizzazione forte, forme normali e decidibilita' dell'uguaglianza
• fondamenti di programmazione funzionale e tipi:
  • strutture applicative e algebre combinatorie parziali (pCA): teoria equazionale, modelli, riscrittura, potere espressivo, proprieta' aggiuntive (estensionalita', test di uguaglianza)
  • lambda calcolo non tipato: alpha-conversione, beta-riduzione, confluenza, relazioni con la logica combinatoria
  • estensioni del lambda calcolo (con costanti): semantica operazione, equivalenza osservazionale
  • type sistems: regole di assegnamento dei tipi, relazioni con la semantica operazionale (subject reduction), tipi come sottoinsiemi (di una pCA)
  • tipi: funzionali, record, variant, reference; subtyping; ricorsivi, polimorfi (universali), astratti (esistenziali)
• concetti di base per processi reattivi e concorrenti [M89,NOTE]:
  • sistemi di transizione etichettati (LTS)
  • CCS: sintassi, semantica operazionale, LTS dei processi
  • CCS ed LTS: esempi di specifica ed implementazione di sistemi
  • equivalenze: trace equivalence, strong bisimulation, weak bisimulation
  • strong bisimulation: proprieta' equazionali, alberi di sincronizzazione

  PARTE CALCOLABILITA' e COMPLESSITA'

• modelli di calcolo: TM, RAM, funzioni calcolabili, complessita' tempo e spazio, relazione tra i due modelli di calcolo, Tesi di Church e Tesi di Church estesa.
• calcolabilita': funzioni calcolabili, problemi/sottoinsiemi decidibili e semidecidibili, riducibilita' tra problemi, codifica delle TM, TM universale, esempi di problemi non (semi)decidibili, proprieta' di chiusura dei sottoinsiemi (semi)decidibili.
• complessita': classi di complessita', relazioni tra classi di complessita' ed O-notazione, classi naturali di complessita' (P, NP), teorema di Cook, esempi di problemi NP-completi.
• panoramica su altri argomenti di complessita': accenni ad altri modelli di calcolo (per algoritmi probabilistici e paralleli), e relative classi di complessita'.

Testi di Riferimento

• [HS86] J.R.Hindley, J.P.Seldin. Introduction to Combinators and Lambda-Calculus. Cambridge University Press, 1986. (CH 1-3, 6-10)
• [C97] L.Cardelli. Type Systems. Handbook of Comp. Sci. and Engineering, CRC Press, 1997.
• [M89] R.Milner. Communication and Concurrency. Prentice Hall International (series in computer science), 1989.
• [P94] C.Papadimitriou. Computational Complexity. Addision-Wesley, 1994. (CH 1-3, 7-9)