Fondamenti (2010/2011)

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 Damiano Macedonio
LINGUAGGI 6 INF/01-INFORMATICA I semestre Massimo Merro

Obiettivi formativi

Modulo: LOGICA
-------
Il corso si propone di introdurre la logica matematica e di chiarire come essa sia ausiliaria alle altre materie. Temi centrali sono la distinzione tra sintassi e semantica, la formalizzazione di proprietà nel linguaggio logico e il concetto di dimostrazione corretta, basata su regole generali prefissate. Verranno presentate tecniche per produrre prove e contro-esempi.


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
-------
Livelli di riferimento. Linguaggio e meta-linguaggio.
Logica proposizionale e predicativa (classica e intuizionista).
Introduzione del calcolo dei sequenti con equazioni definitorie.
Sistemi LJ e LK. Teorema di eliminazione dei tagli. Ricerca delle prove.
Interpretazione classica delle formule, sia proposizionale che predicativa.
Teoremi di Correttezza, Completezza e Compattezza per il calcolo LK.
Problema della decisione per il calcolo predicativo.
Teoremi di incompletezza.


Modulo: LINGUAGGI
-------
Induction:
(i) Mathematical induction over the natural numbers;
(ii) Structural induction;
(iii) Rule induction.
Operational semantics:
Big step and small step semantics for simple languages including
• Exp, Bool, languages for arithmetic and Boolean expressions
• the imperative language of while commands While
• the functional languages Fun and Lambda and simple variations on them; call-by-name and call-by-value semantics.
Typing:
(i) Typing assignments for the languages Fun and Lambda
(ii) Progress and preservation.
(iii) For Lambda you should be familiar with the computational consequences of using types; in particular the need for explicit fixpoint operators.

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)

Statistiche esiti
Esiti Esami Esiti Percentuali Media voti Deviazione Standard
Positivi 48.95% 25 3
Respinti 20.83%
Assenti 8.33%
Ritirati 21.87%
Annullati --
Distribuzione degli esiti positivi
18 19 20 21 22 23 24 25 26 27 28 29 30 30 e Lode
2.1% 0.0% 2.1% 10.6% 6.3% 17.0% 12.7% 2.1% 12.7% 6.3% 12.7% 6.3% 2.1% 6.3%

Valori relativi all'AA 2010/2011 calcolati su un totale di 96 iscritti. I valori in percentuale sono arrotondati al numero intero più vicino.