La lista degli argomenti del corso e l'indicazione del materiale da studiare.
Elementi di Teoria dei linguaggi formali:
- Alfabeto, stringa, linguaggio. Operazioni tra linguaggi. Espressioni regolari. Cardinalita' dei linguaggi.
[AAG].(1.3)
- Grammatiche di Chomsky. Grammatiche ti tipo 0, 1, 2 e 3. Gerarchia di Chomsky. Forma normale di Bakus.
[AAG].(Intro 2, 2.1, 2.4, ultime 6 righe di 2.2)
- Accettazione e riconoscimento di linguaggi. Automi.
[AAG].(2.5)
- Automi a stati finiti deterministici e non deterministici.
[AAG].(3.1, 3.2, 3.3(solo Teoremi 3.1 e 3.3, senza dimostrazioni) )
- Nota sugli Automi a Stati Finiti [AAVV] (sez.1.1)
- Pumping Lemma per Automi a stati finiti.
[MM]
- Cenni di linguaggi non contestuali.
[AAG].(Intro 4; prime 5 righe di 4.5; pag. 155 e 156 di 4.7; 4.8 fino a 4.8.1 escluso)
Modelli computazionali :
- Macchine di Turing. Maccchina di Turing Universale.
[AAG].(Intro 5, 5.1, 5.2, 5.3, Intro 5.4, pag.210 righe 10-20); [AAVV] (sez.1,2)
- Introduzione alla programmazione funzionale ed al linguaggio Haskell. Introduzione al Lambda-calcolo
[FBb]
- Variabili libere e legate, alfa-equivalenza, sostituzione, beta-riduzione. Definizione di sistema formale. Numerali di Church, funzioni lambda-definibili.
[FBh],[PS].(Intro 3, 3.1, 3.2)
- Lambda-definibilita' di funzioni ricorsive. Il teorema di Church-Rosser; unicita' della forma normale, consistenza della teoria della beta-equivalenza.
[FBd] [PS].(3.3)
Codici e rappresentazione informazione numerica:
- Codici e rappresentazione in complemento a due.
[CB]
- Strings vs Numbers
[FBa].
Macchine astratte
- Macchine astratte:
[AAVV]
- Realizzazione di macchine astratte; organizzazione a livelli dei sistemi di calcolo.
[AAVV]
Logica:
- Sistemi formali. Regole derivabili ed amissibili. Alcune proprieta' dei sistemi formali. Consistenza.
[SM](Cap.2)
- La Logica Proposizionale. Principali definizioni e proprieta'.
Teorema di deduzione.
[SM](Sez. 3.1 e 3.2; convincersi della correttezza delle le proposizioni da 3.2 a 3.12); [FBi]
- Semantica della Logica Proposizionale. Correttezza e completezza.
[SM](Sez. 3.3 (tutta). Sez.3.4 Teorema 3.5 (no dimostrazione), Corollario 3.3, Prop.3.15, Lemma 3.3 (no dimostrazione), Teorema 3.6 (no dimostrazione), Corollario 3.5.)
- La Deduzione Naturale per la logica proposizionale.
[FBe] e ([AU](pag.1-11) oppure [AA], farli entrambi puo' aiutare la comprensione).
- La corrispondenza dimostrazioni-programmi [FBg]
- La logica dei predicati: linguaggio e semantica.
[SM](4.1).
- La logica dei predicati in deduzione naturale.
[FBe] e [AU](pag.1-17).
- Enunciati di alcuni teoremi fondamentali.
[SM](Enunciati teoremi 4.3, 4.4, 4.5 ed osservazione seguente, Corollario 4.5 con dim.).
- Formalizzazione dell'aritmetica e della teoria dei gruppi.
[FBf],[AAb]
- Induzione, induzione completa loro utilizzo nelle dimostrazioni di correttezza dei programmi
[VS] (Sez.1, Sez.2, Sez.3)(escluso cio' che riguarda l'induzione ben-fondata), [FBh]
- Corrispondenza tra Induzione e Ricorsione: un breve cenno
[FBi]
Semantica dei linguaggi di programmazione:
- Introduzione alla semantica formale; Semantica Operazionale Strutturata
[SC](solo pag.1), [RR] (tutto fino al Teorema escluso).
Fondamenti generali:
- Il lavoro dell'informatico nel mondo globalizzato. L'importanza di acquisirne una visione non "localistica" e di cogliere tutte le opportunita' per aprire i propri orizzonti nel mondo del lavoro (Erasmus, tirocini all'estero ecc.) [AF] (esclusa sezione Il finale dopo il finale)
Reading Material
-
[AA] A.Asperti Sistemi deduttivi: la deduzione naturale (pdf file)
-
[AAb] A.Asperti Formalizzazione dell'aritmetica e della teoria dei gruppi (pdf file)
-
[AAG] G. Ausiello, F. d'Amore, G. Gambosi.
Linguaggi, Modelli, Complessita'
(pdf file)
-
[AAVV] Introduzione alle Macchine Astratte
(pdf file) LaTeX source
-
[AF] Alberto Forchielli, Muovete il culo! Baldini+Castoldi
-
[AU] A.Ursini La deduzione naturale (pdf file)
Soluzioni esercizi logica proposizionala (.pdf. by Giorgio Buzzanca) LaTeX source
-
[CB] G.Chiola, F.Barbanera. Codici e Rappresentazione in complemento a due
(html file; updated 6 Nov 2013)
-
[FBa] F.Barbanera Strings vs Natural Numbers
(html file)
-
[FBb] F.Barbanera Computazioni, Programmazione funzionale e Preludio al lambda-calcolo (file .pdf, updated 14 Dic 2018) (LaTeX source)
-
[FBc] F.Barbanera Cos'e' un Sistema Formale ed un esempio:
il sistema formale per l'alfa-equivalenza
(html file, updated 11 Nov 2019)
-
[FBd] F.Barbanera Piccole note sul lambda-calcolo.
(html file)
-
[FBe] F.Barbanera Due parole introduttive alla deduzione naturale (html file; updated 14 Jan 2019)
-
[FBf] F.Barbanera Introduzione all'aritmetica di Peano (html file)
-
[FBg] F.Barbanera
Corrispondenza tra Deduzioni e Programmi: un cenno
(html file; updated 22 Mag 2023)
-
[FBh] F.Barbanera Overview of the Lambda Calculus
(html file)
-
[FBi] F.Barbanera
Nota sull'uso dell'Induzione sulla lunghezza delle deduzioni.
(pdf file) (LaTeX source)
-
[FBi] F.Barbanera Corrispondenza Induzione-Ricorsione: un breve cenno (html file)
-
[HFP] P.Hudak et al. A gentle introduction to Haskell (pdf file)
-
[MM] Marina Madonia Dimostrazione del Pumping Lemma (.pdf file, updated 26 Nov 2019)
-
[PS] P.Selinger Lecture Notes on the Lambda Calculus
(pdf file)
-
[RR] S.Ronchi della Rocca Semantica del linguaggio WHILE (pdf file)
-
[SC] S.Chong Intro to Semantics (pdf file)
-
[SM] S.Martini et al. Appunti di Logica Matematica (pdf file) (with some typos corrected by Giuseppe Pulvirenti)
-
[VS] V.Sassone Induzione (pdf file)
-
[XX] Basic Tips for Haskell installation and use (.txt file)
Testi facoltativi
(per approfondire o avere punti di vista differenti)
-
[Hask] Haskell.org An introduction to the Lambda Calculus
-
[CB] C.Baker-Finch. An introduction to the Lambda Calculus
(pdf file)
-
[AC] A. Asperti, A. Ciabattoni. Logica a informatica, McGraw-Hill,
ISBN: 9788838672002. (Nella nostra biblioteca sono a disposizione due copie,
con collocazione AC/2-000162 e AC/2-000163)
-
[SFPW] Sannella, Fourman, Peng, Wadler Introduction to computation : haskell,logic and automata. (Una copia disponibile in biblioteca,
collocazione AC-2/186).
-
[VM] V. Manca. Logica matematica, Bollati Boringhieri (2001). (Alcune copie disponibili in biblioteca)
-
[HMU]
J.E. Hopcroft, R. Motwani, J.D. Ullman. Automi, linguaggi e calcolabilita', 3a Ed, Addison Wesley, Pearson Education Italia (2009). (Alcune copie disponibili in biblioteca)
-
[GL]
G. Lolli. Logica Matematica (pdf file)
Simulatori
(per gli interessati) Curiosita', Applicazioni e Varie
- Il codice Haskell corrispondente alla
parte (<=) del teorema di deduzione di Herbrand.
- Grammatica di JAVA in BNF (alcune notazioni, come quella per l'iterazione sono differenti da quelle che conosciamo, ma la sostanza e' la stessa).
- Grammatica di C++ in EBNF (EBNF e' una versione di BNF. Notare che C++ non e' pero' completamente un linguaggio context-free. Questo significa che con grammatiche context-free possiamo solamente descrivere un sovrainsieme di C++).
-
Una delle tante ditte che lavorano con linguaggi funzionali, in particolare con OCaml https://ahrefs.com/it
-
Una bibliografia regionata su alcune applicazioni della teoria dei linguaggi formali alla Bioinformatica
(pdf file)
- Il sistema Key (un tool per dimostrazioni interattive di correttezza per programmi Java)
- Una MT dal vivo!! :-)
-
Functional Programming in the real world (per convincersi che la programmazione funzionale si utilizza nel mondo reale)
- How functional programming mattered. [Ntl. Sci. Rev. 2(3), 349-370 (2015)](Una introduzione di Hu, Hughes e Wang alle caratteristiche ed all'utilita' dei linguaggi funzionali)
- Cos'e' la Logica
(Audio conferenza molto divulgativa di Piergiorgio Odifreddi, sulla logica nel senso piu' ampio del termine, non solo logica matematica).
- Odifreddi: Video-corso di Logica Matematica
(Estremamente interessante per chi volesse ampliare i propri orizzonti logici).
-
[DH] Douglas R. Hofstadter. Goedel, Escher, Bach: un'Eterna Ghirlanda Brillante (testo di natura divulgativa, suggerito anche dal vostro collega G.Buzzanca).
-
[PO] Piergiorgio Odifreddi. Il Dio Della Logica: vita geniale di Kurt Goedel, matematico della filosofia. Longanesi. (bellissimo testo di natura divulgativa).
-
[SW] Stephen Worfram.
Combinators, a centennial view
-
[SW] Stephen Worfram.
Combinators: a 100-year celebration (video conference)
-
[SW] Stephen Worfram.
Combinators and the Story of Computation