A.A. 2001-02

Linguaggi di Programmazione I: Paradigmi Prova scritta del 9 gennaio 2002

Esercizio 1. Sia ϕ : F 1 → Fun la traduzione dal sistema di tipi F 1 nel linguaggio funzionale Fun così definita: ϕ(M) è il programma ottenuto cancellando da M tutte le annotazioni sui tipi. Assumendo che ∅ ⊢ M : int sia derivabile in F 1, può il programma ϕ(M) andare in loop se valutato con semantica lazy statica? Motivare.

Esercizio 2. Scrivere nel linguaggio Fun un programma M, se esiste, tale che la valutazione con semantica lazy statica di

(fn x ⇒ (M (x x))) (fn x ⇒ (M (x x)))

termini. Scrivere nel linguaggio Fun un programma M′, se esiste, tale che la valutazione con semantica lazy statica di

(fn x ⇒ (M′ (x x))) (fn x ⇒ (M′ (x x)))

non termini.

Esercizio 3. Definire in ML il tipo di dato astratto LAMBDA che rappresenti i termini del lambda calcolo (non tipato) e che fornisca l’operazione subst di sostituzione, dove subst(N, x, M) è il termine ottenuto sostituendo con N tutte le occorrenze libere della variabile x in M. Non è richiesto che subst eviti la cattura.

Esercizio 4. Usando al più 60 parole, definire la nozione di modulo di programma.