ESERCIZI TYPED LAMBDA CALCULUS
Esercizio 1



Fornire le definizioni di lambda-calcolo tipato a' la Church e a' la Curry. Fornire inoltre una proprieta' che li distingue.

  • Soluzione.

    Esercizio 2

    Descrivere la differenza tra lambda calcolo tipato 'a la Church e 'a la Curry. Nel lambda calcolo tipato semplice 'a la Curry qual e' il senso di avere variabili di tipo e del lemma di sostituzione?
    Esercizio 3
    Dare una derivazione formale nel sistema di assegnamento di tipi alla Curry per il seguente giudizio:

    |--  \xy.yx :  a --> (a-->b) --> b

    Esercizio 3.5
    Dimostrare formalmente che il seguente giudizio e' valido

    z: b-->a |- \xy.x(zy) : (a-->c) --> (b-->c)

    Esercizio 4

    Dato un termine M, qual e' la relazione che sussiste tra tutti i giudizi    B |-- M : T   ?
    Esercizio 5


    Quale teorema del lambda calcolo tipato puo' essere parafrasato ne seguente modo?
    "Le informazioni fornite dai tipi nei programmi possono essere ignorate a tempo di esecuzione."

  • Soluzione.

    Esercizio 6

    Dimostrare che se un lambda-termine tipato e' derivabile, allora lo e' ogni sua istanza.
    Ricordiamo che una istanza di Gamma |- M : sigma e' S(Gamma) |- S(M) : S(sigma), dove S sostituisce tipi a variabili di tipo.
    Esercizio 7

    Nel contesto del lambda-calcolo tipato fornire la definizione di Controllo del tipo (Type Checking) e di Ricostruzione del tipo (Type Inference).

    Esercizio 8


    Eseguire il "principal typing algorithm" sul termine \x.\y.x
    Qual'e' invece il tipo principale dell'operatore di punto fisso \f.((\x.f(xx))(\x.f(xx))) ?

  • Soluzione.

    Esercizio 9

    Volendo estendere il lambda-calcolo a' la Curry con i record ed i record types, descrivere come estendere la sintassi dei termini, dei tipi e le typing rules.
    Come si introduce in questo contesto la nozione di sottotipo?
    Esercizio 10

    Dire se c'e' un errore nella seguente proposizione e qual e'.
    Dato un lambda termine M tipabile, sia < P,pi > la principal pair di M. Allora se nel sistema di inferenza di tipi a' la Curry riusciamo a derivare B |- M : tau abbiamo che esiste una sostituzione di tipi S tale che B = S(P) e tau = S(pi).

  • Aiutone.

    Esercizio 11

    Fornire una derivazione nel sistema di tipi a' la Curry per il termine

    \bc.((\y.c)(bc))


  • Soluzione.
    Esercizio 12

    Fornire una derivazione nel sistema di tipi a' la Curry per il termine

    \b.((\y.c)(bc))


  • Soluzione.

    Esercizio 13

    Perche' il termine (\x.x)((\y.yy)(\y.yy)) non e' tipabile nel sistema dei tipi semplici a' la Curry?
    Esercizio 14

    Fornire la coppia principale (Principal Pair) nel sistema di tipi a' la Curry per il lambda termine y(\x.x) . Motivare la risposta.
    Esercizio 14.5
    Perche' possiamo affermare con sicurezza che
    (a-->(b-->b)) --> (a-->(b-->b))
    e' un tipo per \xy.(xy), senza dover andare a trovare una derivazione per
    empty |- \xy.(xy) : (a-->(b-->b)) --> (a-->(b-->b))
    nel sistema di tipi di Curry?
    Esercizio 15
    Dimostrare che se Gamma |-Church M : alpha allora Gamma |-Curry Erase(M) : alpha.

  • Soluzione.

    Esercizio 16

    Qual e' il Principal Pair della funzione che presa una funzione ed un suo argomento applica il secondo alla prima? (cioe' il Principal Pair del lambda termine \fx.fx)

  • Soluzione.

    Esercizio 17
    Se intendiamo introdurre nel lambda-calcolo anche delle costanti esplicite per numeri ed operatori numerici, cosa occorre estendere oltre la definizione di lambda-termine?
    Esercizio 18

    Nel lambda-calcolo tipato a' la Curry ogni termine e' fortemente normalizzabile. Come e' possibile allora estendere il calcolo in modo da poter definire funzioni ricorsive che non terminano?
    Esercizio 19

    Fornire l'assioma e le regole che definiscono la strategia Leftmost-Outermost per l'estensione data nei test del lambda calcolo tipato a' la Curry.


    Esercizio 20

    Esercizio 21

    Aggiungere al lambda calcolo tipato a' la Curry le costanti e le regole di riduzione che descrivano il tipo di dato lista-di-interi.

    Esercizio 22

    Cosa si intende per Polimorfismo? Cosa si intende per polimorfismo implicito? E per Subtyping Polymorphism?

    Esercizio 23
    Definire il lambda-calcolo tipato a' la Church e l'algoritmo di Type Checking.

    Esercizio 24
    Supponiamo di voler estendere il lambda-calcolo tipato a' la Curry LC+ anche con termini che rappresentino liste (in modo esplicito, non tramite una codifica).
    Fornire i tipi, gli assiomi e le regole di inferenza da aggiungere al type system.

  • Soluzione.

    Esercizio 25
    In che modo possiamo affermare con sicurezza che
    (c→c)→((c→c)→(b→b)) → (b→b)
    e' un tipo per \xy.(yx), senza dover andare a trovare una derivazione per
    ∅ |- \xy.(yx) : (c→c)→((c→c)→(b→b)) → (b→b)
    nel sistema di tipi di Curry?

  • Soluzione.

    Esercizio 26
    Descrivere il Principal Pair Algorithm fornendone una succinta giustificazione.

    Esercizio 27

    Dimostrare intuitivamente (ma non troppo...) che 
    (b→c) → ((b→c)→ b) → c
    e' il tipo principale di λxy.x(yx)
  • Soluzione.