FONDAMENTI DI INFORMATICA M - Z

Anno accademico 2017/2018 - 1° anno
Docente: Maria Serafina MADONIA
Crediti: 9
SSD: INF/01 - Informatica
Organizzazione didattica: 225 ore d'impegno totale, 153 di studio individuale, 36 di lezione frontale, 36 di esercitazione
Semestre:

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

 ArgomentiRiferimenti testi
1Introduzione alla teoria dei linguaggi formali. Definizioni di alfabeto, stringa, linguaggio. Espressioni regolarihttp://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html  
2Enumerazione 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  
3BNF. Cosa significa computare. Automi. Automi a stati finiti e corrispondenza con linguaggi regolari.http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html  
4Linguaggio decidibili e semidecidibili. Introduzione al Pumping Lemmahttp://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html  
5Automi 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  
6Uso 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  
7Introduzione 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  
8Induzione 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  
9Codici. 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  
10Definizione 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  
11Intro alla programmazione funzionale ed al lambda-calcolo Lambda-termini; beta-riduzione (informale);http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html  
12Variabili 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  
13Lambda-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  
14Sistemi formali. Principali definizioni correlate ai sistemi formali. Esempio di sistema formale: Combinatory Logichttp://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html  
15Logica 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  
16Logica Proposizionale in deduzione naturale. Corrispondenza deduzioni-programmi.http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html  
17Logica del primo ordine: segnatura, fbf, strutture, semantica.http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html  
18Regole 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  
19Formalismo 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  
20Alcuni 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  
21Realizzazione 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  
22Teorema 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  
23Uso 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  
24Semantica Operazionale Strutturata dei linguaggi imperativi: il linguaggio WHILEhttp://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html  
25Alcuni 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