Conoscenza e capacità di comprensione (knowledge and understanding): L'obiettivo del corso e' quello di offrire allo studente studente una introduzione ad alcune delle principali teorie formali che costituiscono le basi teoriche dell'informatica. Lo studente imparera' a comprendere come tutti gli aspetti dell'Informatica applicata siano basati o fortemente influenzati da conoscenze sviluppate a livello teorico.
Capacità di applicare conoscenza e comprensione (applying knowledge and understanding): Per ogni teoria fondamentale affrontata, allo studente verranno mostrati brevi esempi del suo concreto utilizzo, come l'uso di espressioni regolari in tool di editing e ricerca; l'uso delle grammatiche per lo sviluppo di compilatori; l'uso degli automi per la descrizione del comportamento di circuiti sequenziali; l'uso della logica matematica per la descrizione di specifiche di programmi e l'uso di sistemi formali per la descrizione della semantica dei linguaggi e per le dimostrazioni di correttezza dei programmi. Inoltre, utilizzando elementi di lambda-calcolo e di logica proposizionale, verra' indirizzato alla comprensione della perfetta sovrapposizione esistente tra processi computazionali e processi logico-deduttivi. Questo allo scopo anche di stimolarlo allo studio di materie come analisi e matematica discreta, che potrebbero apparire ad uno studente del primo anno troppo distanti dall'informatica e dalla programmazione.
Autonomia di giudizio (making judgements): Lo studente verra' stimolato a cercare autonomamente quali aspetti dell'informatica teorica vengono utilizzati negli argomenti trattati in corsi piu' apllicativi da lui seguiti nello stesso anno, come Programmazione e Architettura degli elaboratori. Verra' inoltre stimolato a comprendere come gli argomenti di corsi come Elementi di analisi matematica e Matematica discreta potrebbero venire formalizzati nella logica matematica.
Abilità comunicative (communication skills): lo studente acquisira' la capacita' di esprimere in maniera formale e non ambigua argomentazioni di tipo scientifico.
Capacità di apprendimento (learning skills): Lo studente sara' messo in condizione di poter affrontare autonomamente lo studio di argomenti teorici descritti formalmente.
Il sito del corso contiene un notevole insieme di esercizi, e gli studenti sono invitati ad affrontarli durante lo studio individuale. Quelli in cui gli studenti avessero riscontrato difficolta' vengono affrontati nella prima parte della lezione, su richiesta degli studenti. Sempre nella prima parte il docente invita gli studenti a comunicare eventuali difficolta' incontrate nell'affrontare lo studio degli argomenti delle lezioni precedenti, in modo di poterne cosi' discutere insieme.
Nella seconda parte della lezione si affrontano nuovi argomenti e vengono spesso indicati esercizi relativi agli stessi, tra quelli presenti nella pagina degli esercizi del corso o nuovi (che eventualmente andranno ad incrementare l'insieme degli esercizi disponibili).
Come l'anno precedente, si cerchera' di organizzare numerose prove in itinere, la cui valutazione permettera' di venire esonerati dallo svolgere parte dell'esame finale.
Qualora l'insegnamento venisse impartito in modalità mista o a distanza potranno essere introdotte le necessarie variazioni rispetto a quanto dichiarato in precedenza, al fine di rispettare il programma previsto e riportato nel syllabus
Nessuno.
Non obbligatoria, ma fortemente consigliata.
Elementi di Teoria dei linguaggi formali:
Modelli computazionali e teoria della calcolabilita':
Codici e rappresentazione informazione numerica:
Macchine astratte
Logica:
Semantica dei linguaggi di programmazione:
Fondamenti generali
La grande maggioranza dei testi sono in formato elettronico e scaricabili dalla seguente pagina web
Argomenti | Riferimenti testi | |
---|---|---|
1 | Introduzione alla teoria dei linguaggi formali. Definizioni di alfabeto, stringa, linguaggio. Espressioni regolari | Link ai testi |
2 | Enumerazione di Sigma*. Non numerabilita' dei linguaggi su un alfabeto Sigma. Numerabilita' dei programmi di riconoscimento dei linguaggi. Introduzione alle Grammatiche di Chomsky: Definizione, Classi di grammatiche. | Link ai testi |
3 | BNF. Cosa significa computare. Automi. Automi a stati finiti e corrispondenza con linguaggi regolari. | Link ai testi |
4 | Linguaggio decidibili e semidecidibili. Introduzione al Pumping Lemma | Link ai testi |
5 | Automi a stati finiti non deterministici. Pumping Lemma: enunciato e dimostrazione. Induzione e suo utilizzoper dimostrare proprieta' di programmi. | Link ai testi |
6 | Uso del Pumping Lemma. Alcune caratteristiche dei linguaggi context-free. Alberi di derivazione sintattica. Esistenza di linguaggi non generabili da grammatiche: metodo di diagonalizzazione. | Link ai testi |
7 | Introduzione alle macchine di Turing. Definizione formale di Macchina di Turing. Esempio di macchina di Turing. | Link ai testi |
8 | Induzione completa ed esempio di uso per dimostrare proprieta' di programmi. Trasduttori. Esempi di trasduttori. Macchina di Turing Universale. | Link ai testi |
9 | Codici. Rappresentazione informzione numerica. Rappresentazione posizionale e algoritmi di conversione di base. Codici a lunghezza fissa e variabile. | Link ai testi |
10 | Definizione di rappresentazione degli interi in complemento alla base. Proprieta' della rappresentazione in complemento a due e loro dimostrazioni. Introduzione alla programmazione funzionale. | Link ai testi |
11 | Intro alla programmazione funzionale ed al lambda-calcolo Lambda-termini; beta-riduzione (informale); | Link ai testi |
12 | Variabili libere e legate; Alfa-conversione; Sostituzione; Forme normali e loro unicita'; strategie di riduzione; Introduzione alle funzioni lambda-definibili; | Link ai testi |
13 | Lambda-definibilita' di algoritmi che calcolano funzioni. Teorema del punto fisso (enunciato). Lambda-definibilita' di algoritmi ricorsivi. Introduzione ai sistemi formali. Esempio di sistema formale: alfa-conversione. | Link ai testi |
14 | Sistemi formali. Principali definizioni correlate ai sistemi formali. Esempio di sistema formale: Combinatory Logic | Link ai testi |
15 | Logica Proposizionale alla Hilbert. Teorema di deduzione. Semantica della Logica Proposizionale. Teorema di correttezza e completezza (enunciato), | Link ai testi |
16 | Logica Proposizionale in deduzione naturale. Corrispondenza deduzioni-programmi. | Link ai testi |
17 | Logica del primo ordine: segnatura, fbf, strutture, semantica. | Link ai testi |
18 | Regole ammissibili e derivabili. Deduzione naturale per logica primo ordine. | Link ai testi |
19 | Correttezza e completezza; Assiomi non logici dell'aritmetica (PA) e dei gruppi. | Link ai testi |
20 | Alcuni risultati fondamentali di Teoria della Ricorsivita'. Problema della fermata. Isomorfismo di Cantor. Codifica di stringhe con numeri naturali. Definizione di macchina astratta. Corrispondenza Macchine astratte e linguaggi. | Link ai testi |
21 | Realizzazione di Macchine Astratte. Gerarchie di Macchine Astratte. Enunciati teoremi di Incompletezza di Goedel. | Link ai testi |
22 | Teorema di Church. Semidecisione per relazione di derivabilita'; Cenni di Prolog. Induzione ben-fondata. | Link ai testi |
23 | Introduzione alla semantica formale dei linguaggi di programmazione. Semantica Operazionale Strutturata dei linguaggi imperativi: il linguaggio WHILE | Link ai testi |
24 | Il lavoro dell'informatico nel mondo globalizzato. | Link ai testi |
L'esame si articola in uno scritto ed un orale (quest'ultimo facoltativo).
Nello scritto vengono proposte domande sia di natura teorica che esercizi.
Lo scritto e' composto in genere da tre sottoparti: la prima, suddivisa in tre quesiti (il primo solitamente di natura teorica), si basa sulla prima parte del programma.
Compatibilmente con la natura relativamente soggettiva del concetto di "difficolta'", i tre quesiti vengono proposti in ordine di difficolta'.
Similmente per la seconda.parte dello scritto.
La terza parte consta invece di un unico esercizio o quesito che puo' vertere sulla prima o sulla seconda parte del programma, ma comunque su argomenti non presi in considerazione dalle due parti precedenti.
La valutazione sufficiente dello scritto permette di accettare il voto come conclusivo o di accedere, su richiesta, all'orale facoltativo che concorrera' alla valutazione conclusiva .
La verifica dell’apprendimento potrà essere effettuata anche per via telematica, qualora le condizioni lo dovessero richiedere.
E' stata preparato un portale web contenente tutti i testi degli scritti degli anni precedenti:
Le soluzioni degli esercizi proposti agli esami, insieme a molti altri, con relative soluzioni, si possono trovare in un altro portale
appositamente sviluppato: