FONDAMENTI DI INFORMATICA A - L

INF/01 - 9 CFU - 1° semestre

Docente titolare dell'insegnamento

FRANCO BARBANERA


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

No.



Contenuti del corso

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:



Testi di riferimento

http://www.dmi.unict.it/~barba/FONDAMENTI/PROGRAMMI-TESTI/programmaAAcorrente.html


Altro materiale didattico

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 utilizzoper 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


PROVE IN ITINERE

No.


PROVE DI FINE CORSO

http://www.dmi.unict.it/~barba/FONDAMENTI/ESAMI/modalita.html


ESEMPI DI DOMANDE E/O ESERCIZI FREQUENTI

http://www.dmi.unict.it/~barba/FONDAMENTI/ESERCIZI/index.html




Apri in formato Pdf English version