Programmazione dichiarativa

A.A. 2019/2020
Insegnamento per
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.
Lo studente sarà in grado di scrivere programmi di media complessità in ambo i paradigmi e di apprezzarne la complementarietà.

Struttura insegnamento e programma

Edizione attiva
Responsabile
INF/01 - INFORMATICA - CFU: 6
Lezioni: 48 ore
STUDENTI FREQUENTANTI
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 HO
- 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 http://twelf.org/wiki/Main_Page

- 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
Informazioni sul programma
Propedeuticità
programmazione, algoritmi
Prerequisiti e modalità di esame
nessuno

esame scritto
Metodi didattici
lezioni frontali e laboratorio
Materiale didattico e bibliografia
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/cd
STUDENTI NON FREQUENTANTI
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 HO
- 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 http://twelf.org/wiki/Main_Page

- 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 e modalità di esame
nessuno

esame scritto
Materiale didattico e bibliografia
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/cd
Periodo
Secondo semestre
Periodo
Secondo semestre
Modalità di valutazione
Esame
Giudizio di valutazione
voto verbalizzato in trentesimi
Docente/i
Ricevimento:
Su appuntamento
Via Celoria, 18 - stanza 4012
Ricevimento:
venerdì 14.30--16
4009