Conoscenza e capacità di comprensione (knowledge and understanding): L'obiettivo del corso e' quello di far entrare in contatto lo studente con le principali teorie formali che costituiscono i fondamenti dell'informatica. Lo studente imparera' a comprendere come tutti gli aspetti dell'Informatica applicata siano stati realizzati o 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 esempi di 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.
Nessuno.
No.
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:
http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html
http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html
Argomenti | Riferimenti testi | |
1 | Introduzione alla teoria dei linguaggi formali. Definizioni di alfabeto, stringa, linguaggio. Espressioni regolari | http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html |
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. | http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html |
3 | BNF. Cosa significa computare. Automi. Automi a stati finiti e corrispondenza con linguaggi regolari. | http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html |
4 | Linguaggio decidibili e semidecidibili. Introduzione al Pumping Lemma | http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html |
5 | Automi a stati finiti non deterministici. Punping Lemma: enunciato e dimostrazione. Induzione e suo utilizzoper dimostrare proprieta' di programmi. | http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html |
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. | http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html |
7 | Introduzione alle macchine di Turing. Definizione formale di Macchina di Turing. Esempio di macchina di Turing. | http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html |
8 | Induzione completa ed esempio di uso per dimostrare proprieta' di programmi. Trasduttori. Esempi di trasduttori. Macchina di Turing Universale. | http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html |
9 | Codici. Rappresentazione informzione numerica. Rappresentazione posizionale e algoritmi di conversione di base. Codici a lunghezza fissa e variabile. Codici ad espansione. | http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html |
10 | Definizione di rappresentazione degli interi in complemento alla base. Proprieta' della rappresentazione in complemento a due e loro dimostrazioni. Introduzione alla programmazione funzionale. | http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html |
11 | Intro alla programmazione funzionale ed al lambda-calcolo Lambda-termini; beta-riduzione (informale); | http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html |
12 | Variabili libere e legate; Alfa-conversione; Sostituzione; Forme normali e loro unicita'; strategie di riduzione; Introduzione alle funzioni lambda-definibili; | http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html |
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. | http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html |
14 | Sistemi formali. Principali definizioni correlate ai sistemi formali. Esempio di sistema formale: Combinatory Logic | http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html |
15 | Logica Proposizionale alla Hilbert. Teorema di deduzione. Semantica della Logica Proposizionale. Teorema di correttezza e completezza (enunciato), | http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html |
16 | Logica Proposizionale in deduzione naturale. Corrispondenza deduzioni-programmi. | http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html |
17 | Logica del primo ordine: segnatura, fbf, strutture, semantica. | http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html |
18 | Regole ammissibili e derivabili. Deduzione naturale per logica primo ordine. Correttezza e completezza; Assiomi non logici dell'aritmetica (PA) e dei gruppi. | http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html |
19 | Formalismo delle funzioni primitive ricorsive e parziali ricorsive. Non esistenza di formalismi per tutte e sole le funzioni totali. | http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html |
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. | http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html |
21 | Realizzazione di Macchine Astratte. Gerarchie di Macchine Astratte. Primo teorema di Incompletezza di Goedel e schema di dimostrazione. Enunciato secondo teorema di Incompletezza di Goedel. | http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html |
22 | Teorema di Church. Semidecisione per relazione di derivabilita'; Clausole di Horn. Cenni di Prolog. Induzione ben-fondata. | http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html |
23 | Uso dell'Induzione ben-fondata per dimostrare la correttezza di programmi. Introduzione alla semantica formale dei linguaggi di programmazione. | http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html |
24 | Semantica Operazionale Strutturata dei linguaggi imperativi: il linguaggio WHILE | http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html |
25 | Alcuni risultati di teoria dei modelli. | http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html |
Scritto e orale
No.
http://www.dmi.unict.it/~barba/FONDAMENTI/ESAMI/modalita.html
http://www.dmi.unict.it/~barba/FONDAMENTI/ESERCIZI/index.html