Programmazione dichiarativa
A.A. 2020/2021
Obiettivi formativi
Lo scopo dell'insegnamento è fornire agli studenti una solida conoscenza della programmazione dichiarativa, nella sue declinazioni di programmazione funzionale e programmazione logica. L'insegnamento è organizzato intorno all'idea della programmazione relazionale come una estensione del paradigma funzionale. Le applicazioni che studieremo sono legate alla dimostrazione automatica e la semantica dei linguaggi di programmazione.
Risultati apprendimento attesi
Lo studente sarà in grado di scrivere programmi di media complessità in ambo i paradigmi e di apprezzarne la complementarietà.
Periodo: Secondo semestre
Modalità di valutazione: Esame
Giudizio di valutazione: voto verbalizzato in trentesimi
Corso singolo
Questo insegnamento non può essere seguito come corso singolo. Puoi trovare gli insegnamenti disponibili consultando il catalogo corsi singoli.
Programma e organizzazione didattica
Edizione unica
Responsabile
Periodo
Secondo semestre
Metodi didattici:
Lezioni a distanza in modalità sincrona con Microsoft Teams, basate su slides, scrivendo su tavoletta quello che non c'è nelle slides per rispondere a domande; saranno assegnati esercizi da svolgere in simultanea col PC. Gli studenti dovranno essere pronti a partecipare attivamente alle lezioni negli orari stabiliti, con un PC su cui sia installato il software del corso. Le lezioni verranno registrate e rese disponibili per la durata del semestre.
Materiali di riferimento:
Il programma e il materiale di riferimento non subiranno variazioni
Modalità di verifica dell'apprendimento: esame scritto parziale e finale in presenza (se possibile)
Metodi didattici:
le lezioni verranno effettuate in modalità sincrona con la piattaforma Teams durante l'orario previsto. Verranno registrate e rese disponibili per la durata del semestre.
Materiali di riferimento:
Il programma e il materiale di riferimento non subiranno variazioni
.
Modalità di verifica dell'apprendimento:
ogni 3/4 lezioni verrà effettuata una prova in itinere via Teams/Zoom. Come prova finale è prevista (se possibile) un breve esame scritto in presenza e un semplice progetto/presentazione in gruppi di due. Queste modalità sono soggette a cambiamento a seconda del numero di studenti e della situazione contingente.
Lezioni a distanza in modalità sincrona con Microsoft Teams, basate su slides, scrivendo su tavoletta quello che non c'è nelle slides per rispondere a domande; saranno assegnati esercizi da svolgere in simultanea col PC. Gli studenti dovranno essere pronti a partecipare attivamente alle lezioni negli orari stabiliti, con un PC su cui sia installato il software del corso. Le lezioni verranno registrate e rese disponibili per la durata del semestre.
Materiali di riferimento:
Il programma e il materiale di riferimento non subiranno variazioni
Modalità di verifica dell'apprendimento: esame scritto parziale e finale in presenza (se possibile)
Metodi didattici:
le lezioni verranno effettuate in modalità sincrona con la piattaforma Teams durante l'orario previsto. Verranno registrate e rese disponibili per la durata del semestre.
Materiali di riferimento:
Il programma e il materiale di riferimento non subiranno variazioni
.
Modalità di verifica dell'apprendimento:
ogni 3/4 lezioni verrà effettuata una prova in itinere via Teams/Zoom. Come prova finale è prevista (se possibile) un breve esame scritto in presenza e un semplice progetto/presentazione in gruppi di due. Queste modalità sono soggette a cambiamento a seconda del numero di studenti e della situazione contingente.
Programma
Parte 1: il paradigma funzionale
Linguaggio usato: F#
1.1 Intro
- il paradigma, basi di F#
- ricorsione e iterazione
- tipi e poliformisfmo
- tipi di dati algebrici
- property based testing
- funzioni higher horder
- lazy evaluation
- tipi di dati astratti
1.2 Case studies
1.2.1 Type checking and type inference - si parte da soliti type checkers per
espressioni aritmetiche per arrivare a type inference del lambda calcolo
1.2.3 Logica: soddisficibilità, tautology checking, forme normali
--------------------------------------------
Parte 2: il paradigma relazionale:
Linguaggio usato: Twelf
- fatti, regole e queries
- unificazione e proof search
- esempi:
+ rappresenzazione conoscenza ...
+ esempi combinatoriali come 8 regine
+ automi non deterministici
- analisi statica di programmi logici: mode, coverage e termination checking
- esempi legati alla teoria dei linguaggi di programmazione:
+ interpreti e type checkers da lambda calcolo base
fino a un modello di MiniML
+ uso di tipi dipendenti per scrivere interpreti e macchine astratte
type preserving
Linguaggio usato: F#
1.1 Intro
- il paradigma, basi di F#
- ricorsione e iterazione
- tipi e poliformisfmo
- tipi di dati algebrici
- property based testing
- funzioni higher horder
- lazy evaluation
- tipi di dati astratti
1.2 Case studies
1.2.1 Type checking and type inference - si parte da soliti type checkers per
espressioni aritmetiche per arrivare a type inference del lambda calcolo
1.2.3 Logica: soddisficibilità, tautology checking, forme normali
--------------------------------------------
Parte 2: il paradigma relazionale:
Linguaggio usato: Twelf
- fatti, regole e queries
- unificazione e proof search
- esempi:
+ rappresenzazione conoscenza ...
+ esempi combinatoriali come 8 regine
+ automi non deterministici
- analisi statica di programmi logici: mode, coverage e termination checking
- esempi legati alla teoria dei linguaggi di programmazione:
+ interpreti e type checkers da lambda calcolo base
fino a un modello di MiniML
+ uso di tipi dipendenti per scrivere interpreti e macchine astratte
type preserving
Prerequisiti
Nessuno. E' fortemente consigliato il superamento degli esami di Logica, Programmazione e Algoritmi.
Metodi didattici
(video)Lezioni frontali e laboratorio
Materiale di riferimento
Pagina web
https://amomiglianopd.ariel.ctu.unimi.it/v5/home/Default.aspx
Bibiografia:
Parte 1: Functional Programming using F# , Michael R. Hansen and Hans Rischel.
Parte 2: Dispense di Frank Pfenning:
Logic programming https://www.cs.cmu.edu/~fp/courses/lp/
Computation and Deduction https://www.cs.cmu.edu/~fp/courses/comp-ded/
https://amomiglianopd.ariel.ctu.unimi.it/v5/home/Default.aspx
Bibiografia:
Parte 1: Functional Programming using F# , Michael R. Hansen and Hans Rischel.
Parte 2: Dispense di Frank Pfenning:
Logic programming https://www.cs.cmu.edu/~fp/courses/lp/
Computation and Deduction https://www.cs.cmu.edu/~fp/courses/comp-ded/
Modalità di verifica dell’apprendimento e criteri di valutazione
L'esame consiste di una prova in laboratorio su PC, e richiede la scrittura di programmi relativi agli argomenti trattati nell'insegnamento. La valutazione è espressa in trentesimi e dipende dalla correttezza ed eleganza delle soluzioni offerte.
INF/01 - INFORMATICA - CFU: 6
Lezioni: 48 ore
Docente/i