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 in [AAVV].(here)
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] .(here)
Introduzione alla programmazione funzionale ed al Lambda-calcolo [FBb],[PS].(1, 2.1)
variabili libere e legate,alfa-equivalenza, sostituzione, beta-riduzione. Definizione di sistema formale. Numerali di Church, funzioni lambda-definibili. [FBc],[PS].(2.2, 2.3, 2.4, 2.5, 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]

Codici e rappresentazione informazione numerica:

Macchine astratte

Macchine astratte in [AAVV].(here)
Realizzazione di macchine astratte; organizzazione a livelli dei sistemi di calcolo. in [AAVV].(tutto il resto)

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; no proposizioni da 3.2 a 3.12)
Semantica della Logica Proposizionale. Correttezza e completezza. [SM](Sez. 3.3. Enunciati dei Teoremi 3.5,3.6 e del Corollario 3.4. Corollario 3.3 con dimostrazione.)
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: sostituzioni, deduzione naturale. [SM](4.2, fino a Prop 4.3 esclusa), [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]

Semantica dei linguaggi di programmazione:

Reading Material

[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)

[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)

[FBb] F.Barbanera Computazioni, Programmazione funzionale e Preludio al lambda-calcolo (file .pdf, updated 1 Dic 2017) (LaTeX source)

[FBc] F.Barbanera Cos'e' un Sistema Formale ed un esempio: il sistema formale per l'alfa-equivalenza (html file)

[FBe] F.Barbanera Due parole introduttive alla deduzione naturale (html file; updated 20 Nov 2017)

[FBg] F.Barbanera Corrispondenza tra Deduzioni e Programmi: un cenno (html file)

[SM] S.Martini et al. Appunti di Logica Matematica (pdf file) (with some typos corrected by Giuseppe Pulvirenti)

Testi facoltativi
(per approfondire o avere punti di vista differenti)

[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)
[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)(il lambda simulatore ha qualche baco, per esempio non valuta correttamente (\x.x x y)(\x.\y.x y y) ).
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

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 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).