Programmazione dichiarativa

A.A. 2021/2022
6
Crediti massimi
48
Ore totali
SSD
INF/01
Lingua
Italiano
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à.
Programma e organizzazione didattica

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
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/
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
Docente/i
Ricevimento:
Su appuntamento
Via Comelico, 39 - Ufficio S.202
Ricevimento:
Venerdì, 16:30 --18
4009, Celoria 18