30214 - FONDAMENTI LOGICI DELL'INFORMATICA

Conoscenze e abilità da conseguire

Al termine del corso, lo studente conosce le basi logico formali dell'informatica, in particolare, il lamb da calcolo e la sua teoria, corrispondenza tra programmi e dimostrazioni, il lamb da calcolo tipato semplice, i sistemi T ed F. È in grado di descrivere semplici funzioni numeriche in lamb da calcolo e di derivarne i tipi.

Contenuti

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; teorema di separazione di Bohm.

4. Lambda Calcolo Tipato Semplice e Isomorfismo di Curry-Howard

Sintassi alla Curry e alla Church. Isomorfismo con la logica proposizionale minimale. Algoritmi per il type-checking e la type-inference.

5. Meta-teoria del Lambda Calcolo tipato semplice.

Teoremi di normalizzazione debole e forte.

6. Isomorfismo di Curry-Howard ed estensioni del sistema di tipi.

Tipi prodotto, coprodotto, vuoto e singleton. Polimorfismo parametrico (cenni al System F). Cenni ai sistemi di tipi dipendenti e al tipaggio alla Hindley-Milner.

Secondo modulo:

1. Logica e Basi di Dati

Algebra Relazionale, FO come Linguaggio di Query, Algebre
Cilindriche, Aspetti Implementativi

2. Logica e Complessità Computazionale

Strutture Finite e Problemi Decisionali, Caratterizzazione di NP e
PSPACE tramite logiche al Prim'Ordine. SAT Solving.

3. Logica e Intelligenza Artificiale

Logica epistemica: sintassi, semantica, Esempi di Applicazione

4. Logica e Metodi Formali

LTL e CTL: sintassi e semantica. Sistemi Reattivi e Loro Verifica.
Model Checking.

Testi/Bibliografia

Per il primo modulo:

- H.P. Barendregt: The Lambda Calculus, Its Syntax and Semantics (Studies in Logic and the Foundations of Mathematics, Volume 103). Available on-line at http://www.cs.unibo.it/~sacerdot/fli1718/barendregt.pdf

- J.Y. Girard, Y. Lafont, P. Taylor: Proof and Types. Available on-line at http://www.paultaylor.eu/stable/Proofs+Types.html

 

Gli argomenti del libro di Barendregt che saranno presentati a lezione sono già contenuti nella seguente dispensa dello stesso autore:

http://www.cs.unibo.it/~sacerdot/fli1718/IntroductionToLambdaCalculus.pdf

Metodi didattici

Il corso si svolge al primo semestre e prevede in lezioni frontali in aula. Durante le lezioni frontali vengono trattati esaustivamente tutti gli argomenti del corso, fornendo dimostrazioni dettagliate della maggior parte dei teoremi.

A seconda dell'argomento trattato si utilizzeranno lucidi oppure la lezione verrà svolta alla lavagna.

Modalità di verifica e valutazione dell'apprendimento

Esame orale.

Strumenti a supporto della didattica

Verranno forniti i lucidi presentati a lezione. Si daranno inoltre puntatori ad articoli scientifici e testi divulgativi scaricabili liberamente dal Web.

Orario di ricevimento

Consulta il sito web di Claudio Sacerdoti Coen

Consulta il sito web di Ugo Dal Lago