Programmazione dichiarativa
A.A. 2020/2021
Learning objectives
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.
Expected learning outcomes
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.
Course syllabus and organization
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
Professor(s)