[1] lunedì 25 settembre
Presentazione del corso: cenni alle motivazioni all'introduzione del
lambda calcolo e alle sue applicazioni:
teoria dei linguaggi di programmazione
fondamento della programmazione funzionale
semantica dei linguaggi di programmazione
rapresentazione della logica intuizionista.
Parte I: Sintassi e Lambda definibilità
[2] lunedì 2 ottobre
Sintassi. Teoria equazionale sui lambda termini. Variabili libere e
legate.
Sostituzioni: cattura di variabili libere. Teorema Fallace.
Teorema di Punto Fisso e esistenza di un combinatore di punto fisso.
[3] mercoledì 4 ottobre
Definizione formale di sostituzione.
Concetto di riduzione. Definizione di forme normali.
Curryficazione.
[4] lunedì 9 ottobre
Definizioni della nozione di funzione computabile.
Detour: nozione di cardinalità di insiemi.
Esistenza di funzioni non computabili.
[5] mercoledì 11 ottobre
Richiami di teoria della computabilità
esempi di modelli di Calcolo: MdT, RAM, TinyC.
aritmetizzazione dei programmi ed esistenza della funzione universale
e non decidibilita' del problema della fermata. Teorema di Rice.
Rappresentazione dei numeri naturali nel lambda calcolo.
[6] lunedì 16 ottobre
Numerali di Church: successore, predecessore, test per zero.
Definizione della classe R delle funzioni ricorsive
parziali.
[7] mercoledì 18 ottobre
Operatore di punto fisso di Turing.
Dimostrazione che ogni funzione ricorsiva parziale è lambda
definibile.
Parte II: Consistenza della Teoria: Teorema di Church-Rosser
[8] lunedì 23 ottobre
Sistemi di riduzione astratti: definizione di forma normale,
normalizzazione, compatibilità, convertibilità.
Definizione di proprietà di confluenza: (Weakly) Church-Rosser,
Diamond Property.
Rapporto tra confluenza di una relazione di riduzione e consistenza della
teoria equazionale associata.
Lemma di Newmann
Substitution Lemma.
[9] mercoledì 25 ottobre
Parallel reduction: equivalenza tra chiusura riflessiva e transitiva
di beta riduzione e parallel reduction.
Proprietà di parallel reduction.
[10] lunedì 30 ottobre
Dimostrazione di diamond property per parallel reduction.
Estensioni della beta convertibilita': termini inconsistenti.
[11] lunedì 6 novembre
eta-riduzione ed eta-equivalenza.
Lemma di Hindley-Rosen e consistenza della beta-eta equivalenza.
Parte III: Solvibilità e Teorema di Bohm
[12] mercoledì 8 novembre
Definizione di termine solvable.
Definizione di head normal form.
Caratterizzazioni sintattiche di Forme Normali e Head Normal Form.
[13] lunedì 13 novembre
Caratterizzazione dei termini solvable, come termini aventi head normal
form.
Termini incompatibili.
Alberi di Boehm.
[14] lunedì 20 novembre
Teorema di Bohm: termini ready, Boehm-transformations e
proprietà
[15] mercoledì 22 novembre
Teorema di Boehm.
[16] lunedì 27 novembre
Teorema di Boehm.
Cenni alle principali varianti della teoria: logica combinatoria e
lambda-I calcolo.
Parte IV: Lambda calcolo tipato
[17] mercoledì 29 novembre
Introduzione al lambda calcolo tipato semplice:
sintassi dei tipi, definizione di base, dichiarazione, giudizio.
Regole formali di tipaggio.
Versione à la Curry e versione à la Church.
[18] lunedì 4 dicembre
Tipaggi dei numerali di Church con Tipi Semplici e
considerazioni sulle funzioni computabili nei sistemi tipati.
Enunciato delle principali proprietà dei sistemi tipati:
Basis Lemma, Generation Lemma, tipabilità dei
sottotermini, Substitution Lemma.
Teorema di Subject Reduction.
[19] mercoledì 6 dicembre
Tipi del second'ordine: sistema F.
Osservazioni sui tipaggi in F. Generation Lemma e Subject Reduction.
[20] lunedì 11 dicembre
Teorema di Normalizzazione Forte per il lambda calcolo tipato
semplice.
Generalizzazione al sistema F.
