FONDAMENTI DI INFORMATICA M - Z
Anno accademico 2017/2018 - 1° annoCrediti: 9
Organizzazione didattica: 225 ore d'impegno totale, 153 di studio individuale, 36 di lezione frontale, 36 di esercitazione
Semestre: 1°
Obiettivi formativi
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.
Prerequisiti richiesti
Nessuno
Frequenza lezioni
La frequenza non è obbligatoria ma consigliata.
Contenuti del corso
Elementi di Teoria dei linguaggi formali:
- Alfabeto, stringa, linguaggio. Operazioni tra linguaggi. Espressioni regolari. Cardinalita' dei linguaggi.
- Grammatiche di Chomsky. Grammatiche ti tipo 0, 1, 2 e 3. Gerarchia di Chomsky. Forma normale di Bakus.
- Cosa vuol dire computare
- Accettazione e riconoscimento di linguaggi. Automi.
- Automi a stati finiti deterministici e non deterministici.
- Nota sugli Automi a Stati Finiti
- Pumping Lemma per Automi a stati finiti.
- Cenni di linguaggi non contestuali.
Modelli computazionali e teoria della calcolabilita':
- Macchine di Turing. Maccchina di Turing Universale.
- Introduzione alla programmazione funzionale ed al Lambda-calcolo
- variabili libere e legate,alfa-equivalenza, sostituzione, beta-riduzione. Definizione di sistema formale. Numerali di Church, funzioni lambda-definibili.
- Lambda-definibilita' di funzioni ricorsive. Il teorema di Church-Rosser; unicita' della forma normale, consistenza della teoria della beta-equivalenza.
- Il formalismo delle funzioni primitive ricorsive e parziali ricorsive
- Introduzione informale alla teoria della ricorsivita' e ad alcuni risultati fondamentali.
- Un modello computazionale basato sulla logica: un cenno alla programmazione logica.
Codici e rappresentazione informazione numerica:
- Codici e rappresentazione in complemento a due.
- Strings vs Numbers
Macchine astratte
- Macchine astratte
- Realizzazione di macchine astratte; organizzazione a livelli dei sistemi di calcolo.
Logica:
- Sistemi formali. Regole derivabili ed amissibili. Alcune proprieta' dei sistemi formali. Consistenza.
- La Logica Proposizionale. Principali definizioni e proprieta'. Teorema di deduzione.
- Semantica della Logica Proposizionale. Correttezza e completezza.
- La Deduzione Naturale per la logica proposizionale.
- La corrispondenza dimostrazioni-programmi
- La logica dei predicati: linguaggio e semantica.
- La logica dei predicati: sostituzioni, deduzione naturale, sistema assiomatico.
- Enunciati di alcuni teoremi fondamentali.
- Formalizzazione dell'aritmetica e della teoria dei gruppi.
- Enunciati di alcuni teoremi fondamentali della teoria dei modelli.
- Introduzione formale ai risultati limitativi della logica: Goedel, Tarski, Church.
- Induzione, induzione completa, induzione ben fondata e suo utilizzo nelle dimostrazioni di correttezza
- Corrispondenza tra Induzione e Ricorsione: un cenno
- Un frammento decidibile della logica del primo ordine: clausole di Horn e cenni di Prolog
Semantica dei linguaggi di programmazione:
- Semantica Operazionale Strutturata
Testi di riferimento
http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html
Programmazione del corso
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 utilizzo per 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 |
Verifica dell'apprendimento
Modalità di verifica dell'apprendimento
Scritto e orale
Esempi di domande e/o esercizi frequenti
http://www.dmi.unict.it/~barba/FONDAMENTI/ESERCIZI/index.html