2 dicembre 2011 Introduzione. La corrispondenza di Curry-Howard
tra la logica intuizionistica ed il lambda calcolo tipato con tipi semplici.
La deduzione naturale NJ, frammento implicativo.
Concetto fondamentali, regole di introduzione ed eliminazione.
Deduzioni e normalizzazione di deduzioni.
Il lambda calcolo puro e tipato con tipi implicazione: sintassi,
beta riduzione.
Corrispondenza tra prove e lambda termini.
La logica intuizionistica come logica delle asserzioni e
delle loro giustificazioni.
6 dicembre 2011 Teoria della dimostrazione.
Girard, ch3-4
Il sistema di deduzione naturale intuizionistico
NJ con la sola implicazione. Esempi.
13 dicembre 2011 Teoria della dimostrazione.
Il sistema di deduzione naturale intuizionistico
NJ con la sola implicazione.
teorema di normalizzazione debole, enunciato e dimostrazione.
16 dicembre 2011 Lambda calcolo.
Il lambda calcolo concetti fondamentali
J-L.KrivineLambda calculus: Types and models
Alfa equivalenza e concetti di sostituzione; preliminari sulla
dimostrazione della proprieta` di Church-Rosser.
20 dicembre 2011 Lambda calcolo.
La proprieta` di Church Rosser del lambda calcolo.J-L.Krivine Cap 1.
Vacanze invernali
10 gennaio 2012 Lambda calcolo
La rappresentabilita` delle funzioni parziali ricorsive nel lambda calcolo.
J-L.Krivine, Capitolo 2.
13 gennaio 2012 Teoria delle categorie.
Concetti elementari. Categorie, in particolare pagine 1-4 di
Lambek e Scott.
Per approfondimenti, altamente raccomandabileTom Leinster Corso di
Teoria delle categorie 2007-8.
17 gennaio 2012 Teoria delle categorie.
Funtori. Esempi, in particolare F1-F3 p.6-7 in Lambek e Scott
20 gennaio 2012 Teoria delle categorie.
Trasformazioni naturali. Concetto di aggiunzione: Esempio G1 p.11 in
Lambek e Scott.
24 gennaio 2012 Teoria delle categorie.
Illustrazione di argomenti da presentare
per credito. Fine corso.
Esame scritto:E` possibile, come opzione, sostenere un esame scritto anche sugli
argomenti di teoria della dimostrazione, lambda calcolo e categorie
invece che fare una presentazione orale.
Le domande riguarderanno soprattutto
la capacita` di scrivere semplici prove
in deduzione naturale, la comprensione dei concetti di deduzione normale,
normalizzazione debole e forte;
la conoscenza della proprieta` di Church-Rosser (senza prova);
la rappresentazione delle operazioni successore, somma e prodotto
negli interi di Church;
la corrispondenza tra dimostrazioni in deduzione naturale ed i termini
del lambda calcolo tipato.
Concetti fondamentali di teoria delle categorie, categorie, funtori,
trasformazioni naturali, prodotti categorici ed esponenti.
La presentazione equazionale delle categorie cartesiane chiuse e la
corrispondenza con il lambda calcolo.
Presentazioni studenti per credito:
J-Y. Girard The Blind Spot III: Linear logic Capitoli 8 e 9
Categorie cartesiane chiuse presentate equazionalmente
e sistemi di Gentzen: Lambek e Scott:
Introduction to higher order categorical logicPart 0-1 Tom Leinster's CoursesCategory theory 2007-8
1.Categorie cartesiane, regole della congiunzione
nella deduzione naturale e nel calcolo dei sequenti;
corrispondenze sintattiche, normalizzazione ed eliminzione del taglio.
2.Categorie cartesiane chiuse, regole dell'implicazione
nella deduzione naturale e nel calcolo dei sequenti; corrispondenze
sintattiche, normalizzazione ed eliminzione del taglio.
3.Categorie bicartesiane, regole della disgiunzione
nella deduzione naturale e nel calcolo dei sequenti; corrispondenze
sintattiche, normalizzazione ed eliminzione del taglio.
4.Le categorie bicartesiane chiuse sono degenerate
5.Nella categoria Sets il coesponsnte e` degenerato
(T.Crolard Substractive Logic)
6.Categorie monoidali chiuse. Definizione e confronto
con le CCC.
7.Definizione di una coategoria monoidale come invariante
della normalizzazione dalla logica lineare intuizionistica
8.Il teorema di coerenza nelle categorie monoidali
(McLane Categories for the working mathematician)