SYLLABUS and READING MATERIAL

• 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)
• Cosa vuol dire computare  in [AAVV].(here)
• 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.  [AAG].(3.4)
• 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)

• 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]
• Il formalismo delle funzioni primitive ricorsive e parziali ricorsive  [SMb]pag.1
• Introduzione informale alla teoria della ricorsivita' e ad alcuni risultati fondamentali.  [AAG] 1.1.7, [PO]fino a 4.4 escluso
• Un modello computazionale basato sulla logica: un cenno alla programmazione logica.  [FBj], [AC].

• Codici e rappresentazione in complemento a due.  [CB]
• Strings vs Numbers  [FBa].

• 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, sistema assiomatico.   [SM](4.2, fino a Prop 4.3 esclusa; Definizione 4.18), [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]
• Enunciati di alcuni teoremi fondamentali della teoria dei modelli.  [SM] Sezione 5.1 (senza dim. di teorema 5.1).
• Introduzione formale ai risultati limitativi della logica: Goedel, Tarski, Church.   [SMb](dalla Definizione 1 in poi, escludendo: Def.3, Teor.2, Def.4, Prop.1, Oss.1, Fatto-3, Dim.Teor.3, Dim.Cor.3, Teor.5, Oss.2, Lem.1, Dim.Teor.6, Cor.4, Dim.Teor.9, Lem.2, Teor.10.).
• Induzione, induzione completa, induzione ben fondata e suo utilizzo nelle dimostrazioni di correttezza  [VS] (Sez.1, Sez.2, Sez.3), [FBh]
• Corrispondenza tra Induzione e Ricorsione: un cenno  [FBi]
• Clausole di Horn e cenni di Prolog [FBj],[AC].

• Semantica Operazionale Strutturata  [RR] (tutto fino al Teorema escluso).

• [AA] A.Asperti 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 (html file)


• [AAVVb] Nota sugli automi a stati finiti (html file)


• [AC] Alison Cawsey The Basics of Prolog (html file, excerpt from AI Programming in Prolog, by Alison www.macs.hw.ac.uk)
  


• [AU] A.Ursini La deduzione naturale (pdf file)


• [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 19 Giu 2017) (LaTeX source)


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


• [FBd] F.Barbanera Piccole note sul lambda-calcolo. (html file)


• [FBe] F.Barbanera Due parole introduttive alla deduzione naturale (html file)


• [FBf] F.Barbanera Introduzione all'aritmetica di Peano (html file)


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


• [FBh] F.Barbanera Notes on Well-founded sets. (html file)


• [FBi] F.Barbanera Corrispondenza Induzione-Ricorsione: un cenno (html file)


• [FBj] F.Barbanera Prolog: un cenno (html file)


• [PO] P.Odifreddi Teoria della ricorsivita' (pdf file) (voce enciclopedica, e quindi a carattere divulgativo)


• [PS] P.Selinger Lecture Notes on the Lambda Calculus (pdf file)


• [RR] S.Ronchi della Rocca Semantica del linguaggio WHILE (pdf file)


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


• [SMb] S.Martini et al. Alcuni risultati limitativi della logica (pdf file)


• [VS] V.Sassone Induzione (pdf file)

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

• 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

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