Fondamenti (2011/2012)

Codice insegnamento
4S02789
Crediti
12
Coordinatore
Massimo Merro
L'insegnamento è organizzato come segue:
Modulo Crediti Settore disciplinare Periodo Docenti
LOGICA 6 INF/01-INFORMATICA I semestre Andrea Masini
LINGUAGGI 6 INF/01-INFORMATICA I semestre Massimo Merro

Obiettivi formativi

Modulo: LOGICA
-------
Il corso si propone di introdurre la logica matematica. Verranno introdotti e approfonditi i principali metodi semantici (teoria dei modelli) e sintattici (calcolo dei sequenti) per la logica dei predicati del primo ordine.


Modulo: LINGUAGGI
-------
L'obiettivo del corso è quello di presentare le basi teoriche dei linguaggi di programmazione. A tale scopo verranno introdotti vari linguaggi sequenziali paradigmatici anche di ordine superiore. Tutto il corso sarà incentrato sui concetti di semantica operazionale e di sistema di tipo. Verranno introdotte alcune tecniche formali per la verifica del comportamento dei programmi.

Programma

Modulo: LOGICA
-------
Strutture e Linguaggio del Primo Ordine:
connettivi,variabili, quantificazione. Semantica di Tarski del linguaggio del primo ordine. Concetto di modello. Identità.

Teoria dei Modelli:
omomorfismi, equivalenza elementare, strutture e sottostrutture.

Teoria della dimostrazione:
Il problema dell’assiomatizzazione. Il calcolo dei sequenti LK. L'eliminazione del taglio. Proprietà della sottoformula e consistenza del calcolo puro dei predicati. Eliminazione del taglio per teorie matematiche del I ordine.

Semantica e Sintassi a confronto: Teroremi di correttezza, e completezza. Teorema di compattezza. Teoremi di Löwenheim-Skolem (Upward e Downward)


Modulo: LINGUAGGI
-------
Induzione:
(i) Induzione matematica sui numeri naturali;
(ii) Induzione strutturale;
(iii)Induzione su un sistema di inferenza.

Semantica operazione:
Semantica big step e small step per semplici linguaggi sequenziali, tra cui:
(i) Exp, Bool, linguaggi per espressioni aritmetiche e booleane.
(ii) Il linguaggio imperativo While dei comandi while
(iii)I linguaggi funzionali Fun e Lambda e loro variazioni; semantiche call-by-name e call-by-value.

Sistemi di tipo
(i) Assegnamenti di Tipo per i linguaggi Fun e Lambda
(ii) Le proprieta' di Progress and preservation.
(iii) Per il linguaggio Lambda lo studente dovra' conoscere le consequenze computazionali dell'uso dei tipi; in particolare la necessita' di usare operatori espliciti di punto fisso.

Modalità d'esame

Modulo: LOGICA
-------
Prova scritta.


Modulo: LINGUAGGI
-------
L'esame consiste in una prova scritta e una eventuale prova orale, a discrezione del docente.

Statistiche per i requisiti di trasparenza (Attuazione Art. 2 del D.M. 31/10/2007, n. 544)

I dati relativi all'AA 2011/2012 non sono ancora disponibili