Programmazione Funzionale
06 Ottobre 2006

Neiente appunti o calcolatrici. Massima SINTETICITA' nelle risposte.
Esercizio 1
(a) Dimostrare che se P -->beta Q allora FV(Q) e' un sottoinsieme di FV(P).
(b) Qual e' il risultato della seguente sostituzione? ((\w.(xw))(\y.(yx)))[\x.(w(xy))/x]
(c) Dire se, qualsiasi sia k, l'insieme
{M | M e' normalizzabile e ogni sequenza di riduzione che arriva alla forma normale e' lunga almeno k}
e' chiuso per beta-conversione. Giustificare la risposta.
Esercizio 2
(a)
  • Definire in SCHEME il dato astratto "Tipo" (gli oggetti di questo tipo di dato astratto rapresentano i tipi dei sistemi a' la Church e a' la Curry per il lambda-calcolo).
  • Scrivere una funzione SCHEME "substitute" che, preso un tipo T1, una variabile di tipo V ed un altro tipo T2, restituisca T1 in cui al posto di ogni occorrenza di V e' stato sostituito T2.
  • Dimostrare formalmente che substitute e' totale.

    (b) Svolgere in HASKELL i pri due punti dell'esercizio precedente.
    Esercizio 3

    (a) Supponiamo di introdurre un nuovo tipo di espressione in SCHEME, della forma
    (clarabella var1 var2 exp1 exp2 exp3)
    Se valutiamo una clarabella espressione partendo da un frame puntato da n, il suo valore e' quello dell'espressione exp3 valutata in n2, dove n2 e' come indicato nel diagramma seguente e dove i frame puntati da n1 e n2 vengono creati dalla valutazione della clarabella espressione. Inoltre v1 e' il valore di exp1 valutato in n, mentre v2 e' il valore di exp2 valutato in n1. 
              |   n  ______________   n1 ______________   n2       
          | <--- | var1 -> v1 | <--- | var2 -> v2 | <---- 
-----------      --------------      --------------
    Fornire una espressione SCHEME il cui effetto sia esattamente quello della valutazione di una clarabella espressione.

    (b)
    Scrivere una espressione SCHEME il cui valore sia la chiusura < p1, (lambda (x) (x x)) >, dove p1 punta al frame empty[a,3] il cui padre (il frame immediatamente superiore) sia il frame al top-level.