Prof. Claudio Sacerdoti Coen

Argomenti del programma: Il corso fornisce innanzitutto alcuni rudimenti di teoria della computabilità e della complessità: macchine di Turing, indecidibilità, tempo polinomiale e NP-completezza. Verso la fine del corso, daremo poi una panoramica sulla cosiddetta computational learning theory: PAC Learning, apprendimento tramite convergenza uniforme, VC-Dimension.

• Entrambi i testi coprono la maggior parte degli argomenti visti a lezione. Per i restanti (semantica intuizionista, BNF, ricorsione e induzione strutturale) viene fornito dal docente materiale integrativo.

Argomenti del programma: 1. Paradossi e loro risoluzione: Giustificazione della logica formale. Applicazione dei paradossi per dimostrare risultati negativi in informatica (cenni). 2. Cenni alla teoria assiomatica degli insiemi: ZF, relazioni, funzioni, quozienti, cardinalità. Teorema di Cantor. 3. Logica proposizionale: Sintassi e semantiche classica e intuizionista (cenni).

• H.P. Barendregt: The Lambda Calculus, Its Syntax and Semantics (Studies in Logic and the Foundations of Mathematics, Volume 103).
• Congiuntamente i due testi coprono tutti gli argomenti visti a lezione.
• Il testo copre i soli argomenti relativi a "Logica e Metodi Formali".
• Per quanto riguarda "Modellazione e analisi statica di sistemi distribuiti" il docente fornirà materiale didattico integrativo.

Argomenti del programma: Primo modulo: 1. Richiami di Logica Proposizionale e al Prim'Ordine. Sintassi, Semantica, Correttezza e Completezza, Indecidibilità della Logica al Prim'Ordine 2. Lambda Calcolo non tipato. Sintassi e Semantica Operazionale. Il Lambda Calcolo come linguaggio di programmazione: stategie di valutazione e rappresentazione dei dati; Turing completezza (cenni). 3. Meta-teoria del Lambda Calcolo non tipato. Confluenza. 4.