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

    Trovare il principal pair dei numerali di Church.
    Esiste un tipo piu' generale per TUTTI i numerali di Church?
    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

    Perche' l'operatore di punto fisso Y=\f(\x.f(xx))(\x.f(xx)) non puo' essere utilizzato per definite funzioni per ricorsione nel lambda-calcolo se utilizziamo una strategia call-by-value?
    Perche' H=\g.( (\f.ff)(\f.(g\x.ffx)) ) invece va bene?
    Se volessimo introdurre H come costante nel PCF lazy per definire funzioni per ricorsione, quale comportamento funzionale dovrebbe avere? cioe', quali altre costanti e/o regole di riduzione dovremmo aggiungere?


    Esercizio 17.5
    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 Church ogni termine e' fortemente normalizzabile. Come e' possibile allora in PCF definire funzioni ricorsive che non terminano?
    Esercizio 19

    Fornire l'assioma e le regole che definiscono la strategia Leftmost-Outermost per il PCF.


    Esercizio 20

    Una proprieta' molto importante dei termini del lambda calcolo tipato a' la Church e' che sono tutti fortemente normalizzabili. Questo vale anche per i termini di PCF? Se si, perche'? Se no, perche'?
  • Aiutino.

    Esercizio 21

    Aggiungere in PCF le costanti e le regole di riduzione che descrivano il tipo di dato lista-di-interi.

    Esercizio 22
    Fornire un termine PCF, esteso come nell'esercizio precedente, che rappresenti la lista infinita di tutti i numeri naturali.
    Scrivere una funzione PCF che restituisca il primo numero pari di una lista (assumere di avere qualche predicato primitivo). Applicare la funzione alla lista infinita e simulare la valutazione lazy.

  • Soluzione.
    Esercizio 23

    Fornire una semantica operazionale big-step del PCF lazy.
    Esercizio 24

    Cosa si intende per Polimorfismo? Cosa si intende per polimorfismo implicito?