Programma del Corso

• Introduzione e preliminari
• Breve panoramica dei vari "stili" di programmazione
• Richiamo di alcune nozioni di base:
• Sintassi BNF
• Grammatiche
• Linguaggi
• Ambiguita'
• Semantica operazionale tramite regole induttive
• Esempio: sintatti e semantica di un linguaggio per espressioni
• Ricorsione
• Breve accenno a questioni implementative
• Esempio: Tail recursion
• Esempio: Rappresentazione delle espressioni in forma postfissa e valutazione tramite pila
• Correttezza statica e Tipi
• Caratterizzazione dei type-systems statici/dinamici, strong/soft/weak, polimorfi/monomorfi
• Type inference
• Tipi di Ordine Superiore (Higher Order)
 
• Linguaggi Funzionali (Higher Order)
• Valori denotabili e valori esprimibili
• Cenni di Lambda-calcolo
• Restrizioni alla beta-riduzione: strategie di valutazione nei linguaggi "reali"
• Valutazione "Eager" (ML)
• Valutazione "Lazy" (Miranda e Askell)
• Semantica operazionale: dalla riscrittura (con sostituzioni) alle associazioni esplicite (con ambiente)
• Il problema dello scoping statico: il concetto di chiusura
• Altri problemi sullo scoping statico per la valutazione lazy
• Stile di programmazione lazy
• Funzioni come processi comunicanti tramite streams
• Tipi di dato lazy
• Esempi di programmazione lazy: Lista dei numeri naturali, lista dei fattoriali, lista dei numeri primi (Crivello di Eratostene)
• Costruttori
• Pattern matching
• Tipi di dato concreti (in ML)
• Uguaglianza in ML
• Type inference
• Type inference in Lambda-calcolo
• Corrispondenza con la logica intuizionista
• Isomorfismo di Curry-Howard
• Correttezza del Type System (subject reduction)
• Type inference in ML
• Problema del polimorfismo nelle espressioni con dichiarazioni locali
• Schemi di tipo.
• Generalizzazione e istanziazione
• Breve introduzione alla sintassi di Standard ML e all'uso del suo interprete (del New Jersey)
• Esempio di programmazione in ML: Realizzazione di un interprete per un sottolinguaggio del Pascal
• Tipi di dato Astratti (in ML)
• Esempio: Liste ordinate di interi
• Polimorfismo
• Esempio: Insiemi
• Moduli in ML
• Segnature, strutture e funtori
• Matching fra strutture e segnature.
• Aspetti relativi al polimorfismo
• Esempio: Dizionario (entry=(chiave,descrizione))
• Aspetti implementativi
• Un meta-interprete basato sulla semantica operazionale "naif".
• Un meta-interprete basato sull'ambiente.
• Il problema delle definizioni ricorsive.
• Implementazione delle funzioni ricorsive tramite puntatori
• Limiti della programmazione funzionale
• Valutazione simbolica, unificazione, nondeterminismo
 
• Linguaggi Logici
• Logic Programming classico (basato sulla HCL -- Horn Clause Logic)
• Introduzione. Esempio di somma e prodotto definiti come relazioni
• Sintassi della HCL
• Termini, atomi, clausole, programmi
• Esempio dell'albero genealogico
• Semantica dichiarativa
• Cenni di Teoria dei Modelli per la Logica del Primo Ordine (nozioni di interpretazione, modello, conseguenza logica)
• Forma a clausole e skolemizzazione (cenni)
• Base, interpretazioni e modelli di Herbrand
• Clausole di Horn ed esistenza del modello minimo
• Programmi come teorie logiche (insiemi di clausole Horn definite)
• Programmi come sistemi induttivi
• Modelli = interpretazioni chiuse rispetto al sistema induttivo
• Modello di Herbrand minimo = insieme definito dal sistema induttivo
• Semantica operazionale
• Sostituzioni
• Unificazione di un insieme di equazioni
• Most General Unifier
• Derivazione, refutazione, computed answer substitution
• Corrispondenza fra semantica operazionale e semantica dichiarativa (soundness e completeness)
• Indipendenza dalla regola di selezione
• SLD-resolution e SLD-tree
• Strategia del Prolog: regola di selezione leftmost e visita dell'albero in deep-first
• Cenni alla risoluzione per clausole generali
• Algoritmo di Unificazione
• Prolog
• Breve introduzione all'SWI Prolog
• Liste
• Negazione per fallimento
• Aritmetica
• Altre primitive non logiche: cut, assert e retract
• Primitive meta. Metaprogrammazione in Prolog
• Esempio: metainterprete relativo a teorie organizzate secondo una gerarchia isa
 
• Lambda Prolog
• Il sistema dei tipi in Lambda Prolog
• Dichiarazioni "kind"
• Dichiarazioni "type"
• Ordine di un tipo
• Clausole di Horn del Primo Ordine (FOHC). Semantica operazionale nello stile della deduzione naturale.
• Formule ereditarie di Harrop del Primo Ordine (FOHH)
• Goal con implicazione
• Goal con quantificazione universale
• Moduli in Lambda Prolog
• Accumulate
• Import
• Local
• Caratteristiche Higher-Order in Lambda Prolog
• Unificazione modulo lambda-conversione
• Decidibilita` dell'unificazione modulo lambda_0 conversione e esistenza del most general unifier
• Esempi di programmazione in Lambda Prolog
 
• Linguaggi Object Oriented
• Classi e oggetti
• Metodi e variabili di stato
• Incapsulamento (protezione delle informazioni)
• Creazione e distruzione di oggetti
• Applicazione di metodi (messaggi)
• Il concetto di self
• Sottoclassi e inheritance
• Definizione di sottoclassi (/estensioni/specializzazioni) di altre classi
• Inheritance
• Regole di hiding nella definizione di una sottoclasse
• Possibilita' di ridefinire metodi e regole di dispatching
• Esempio: definizione di stack e queue come specializzazioni delle liste circolari
• Caratteristiche Object Oriented del C++
• Costruttori
• Oggetti dinamici e statici
• Protezione delle informazioni in C++
• Esempio: il crivello di Eratostene