Programmazione dichiarativa
A.A. 2021/2022
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
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
Lezioni in presenza (a meno di circostanze eccezionali) 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 Fiorentini e slides
Riferimenti addizionali: 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 Fiorentini e slides
Riferimenti addizionali: 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 di durata di circa 3 ore (tre), e richiede la scrittura di programmi relativi agli argomenti trattati nell'insegnamento. La valutazione, che verrà comunicata anonimizzata sul sito del corso, è espressa in trentesimi e dipende dalla correttezza ed eleganza delle soluzioni offerte.
INF/01 - INFORMATICA - CFU: 6
Lezioni: 48 ore
Professor(s)