Programma Fondamenti

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)
[AF] A.Farrugia. Combinatory Logic: From Philosophy and Mathematics to Computer Science (pdf file)
[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

Un simulatore di Turing Machines(ce ne sono molti sul web, potete provare a farne uno voi in java come esercizio di programmazione)
Un simulatore di Turing Machines (sviluppato dai vostri colleghi Daniele Distefano e Marco Apa)
Un simulatore di URM (segnalazione di Danilo SkyWolf)
Un simulatore per il lambda-calcolo (con link a simulatori per grammatiche e automi a stati finiti) (segnalazione di Ocelot92)
Un altro simulatore per il lambda-calcolo (quando visualizza un redex sottolinea solo la parte argomento) (la documentazione).
Un evidenziatore di parentesi per λ-termini (sviluppato da S.Veneziano) (permette di evidenziare gli annidamenti di parentesi nei λ-termini; utilissimo per fare gli esercizi su termini complessi; per usarlo in locale basta scaricarsi la pagina).
Animazione su uso codici ad espansione per codifica codici operativi istruzioni macchina

(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). Questo tool e' stato utilizzato per la verifica dell'algoritmo di ordinamento TimSort della libreria standard Java. Tale verifica ha permesso di rilevare un bug nell'algoritmo.
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
Uwe Nestman et al. Alcuni video ben fatti sul lambda calcolo (quelli da 2 a 5 riguardano quel che abbiamo noi nel programma)

SYLLABUS and READING MATERIAL

Syllabus

Reading Material