4 dicembre 2012 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.
7 dicembre 2012 Teoria della dimostrazione.
Girard, ch3-4
Il sistema di deduzione naturale intuizionistico
NJ con la sola implicazione: assegnazione di lambda termini.
14 dicembre 2012 Teoria della dimostrazione.
Deduzione naturale intuizionistica NJ con implicazione e
congiunzione: assegnazone di lambda termini con prodotti.
18 dicembre 2012 Teoria della dimostrazione.
Deduzione naturale intuizionistica con implicazione, congiunzione e
disgiunzione (cenni).
La struttura delle prove normali.
Teorema di normalizzazione debile, enunciato e idea della dimostrazione.
Vacanze invernali
8 gennaio 2013 Ricapitolazione teorema di normalizazione debole.
11 gennaio 2013
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.
15 gennaio 2013 Lambda calcolo.
La proprietà di Church Rosser del lambda calcolo.J-L.Krivine Cap 1.
18 gennaio 2013 Lambda calcolo
La rappresentabilita` delle funzioni parziali ricorsive nel lambda calcolo.
J-L.Krivine, Capitolo 2.
22 gennaio 2013
>
25 gennaio 2013
Fine corso.
Esame scritto:
>
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.
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)