 |
|
Modelli di Calcolo
dott. Ivano Salvo
anno accademico 2006/07
|
Ultima modifica: 12 settembre 2006
Introduzione
Il corso è una introduzione al lambda calcolo [Church,
1936], visto sia come modello di calcolo fondazionale, sia come fondamento
del paradigma di programmazione funzionale, sia in relazione alla
rappresentazione della logica.
Scopo del corso sarà soprattutto gli studenti al
ragionamento formale e stimolare un approccio rigoroso ai problemi
computazionali.
Programma del corso
Introduzione [1]:
Sintassi e Computazione [2]: Cenni storici. Sintassi dei termini.
Variabili libere e legate. Sostituzioni. Teoria equazionale. Computazione:
beta regola e
forme normali.
Teoria Classica [4]:Confluenza. Teorema di Boehm. Strategie di
riduzione. Strategie normalizzanti.
Lambda-calcolo come modello di calcolo [2]: Numerali di Church.
Operatori di punto fisso. Turing-completezza
Sistemi di Tipi: Lambda Calcolo tipato semplice: versioni à
la Church e versioni à la Curry. Teoremi fondamentali:
unicità del tipo (Church), tipo principale (Curry), subject
reduction. Normalizzazione.
Semantica: Tipi intersezione. Filtri lambda modelli.
Materiale e testi di consultazione
L'opera più completa sulla sintassi e semantica del lambda-calcolo
è il libro:
 |
|
The Lambda-Calculus, its Syntax and Semantics
Henk Barendregt
North Holland, Amsterdam, 1984
|
Ulteriori materiali del corso, potranno essere articoli
scientifici che saranno via via distribuiti a lezione e/o resi disponibili
qui sotto:
Letture consigliate:
Orario
-
Lezioni:
lunedì 10:15-11:45 (Aula Alfa)
mercoledì 12:00-13:30 (Aula Alfa)
-
Ricevimento studenti (Via Salaria, stanza 310): mercoledì,
ore 11:30 - 12:30.
Modalità d'esame
L'esame sarà diviso in due parti:
- svolgimento e presentazione di una tesina da parte che
può avere sia carattere teorico (approfondimento di qualche
argomento del corso, attraverso la lettura di articoli scientifici) o
pratico/implementativo (case studies). La tesina costituisce 2/3
della
valutazione finale.
- superamento di un test con domande a scelta multipla e/o
aperta in cui verrà chiesto allo studente la conoscenza e la
capacita' di mettere in relazione le nozioni apprese a lezione, ed
eventuali esercizi. Vale 1/3 della valutazione finale.
Avvisi
La lezione di mercoledì 27 settembre è annullata causa
seduta di laurea.