ESERCIZI LAMBDA CALCULUS
N.B. Gli esercizi sulle strategie di riduzione sono alla fine del file.


Esercizio 0
  • Cosa si intende per "programma" nel contesto dei linguaggi di programmazione funzionale?
  • In cosa consiste l'"esecuzione" di un programma in un linguaggio funzionale?
  • Elencare alcuni concetti tipici della programmazione imperativa che perdono completamente di significato in quella funzionale.
  • Cos'e' un Modello Computazionale?
  • Cosa si intende per "astrazione funzionale" e come questa viene formalizzata nel lambda-calcolo?
  • Cosa si intende per "currificazione" e quali sono i possibili vantaggi del suo utilizzo.
  • Cos'e' la relazione di alfa-convertibilita' tra termini?
    Esercizio 1
    Dato il seguente termine, cerchiare le sue variabili libere e collegare, utilizzando delle frecce, le sue variabili legate con i lambda relativi.

    λz.( ((λx.λx.yx)x)(vλz.λw.v) )

  • Soluzione.
    Esercizio 2


    Descrivere sinteticamente alcuni svantaggi dei linguaggi di programmazione funzionali.


  • Soluzione.
    Esercizio 3


    Ridenominare alcune variabili legate nel seguente termine, in modo che non ci siano due lambda che leghino variabili con lo stesso nome.

    (λxxx.(zλz.x))(xλy.(y(λy.z)yy))

  • Soluzione.
    Esercizio 4


    Ricopiare il seguente termine sottolineando le variabili libere e mettendo un cerchietto intorno a quelle legate:

    (λx.(z(λz.((xyz)x))zx))x(λx.((λy.yy)(λz.zz)))

  • Soluzione.
    Esercizio 5


    Rinominare le variabili legate nel seguente termine in modo che non ci siano due variabili legate con lo stesso nome

    x(λx.((λx.x)x))

    Esercizio 6


    Fornire un lambda-termine che contenga variabili con nome x, y e z ed in cui ci siano occorrenze sia legate che libere di variabili con tali nomi.

  • Soluzione.
    Esercizio 7


    Riscrivere il seguente termine utilizzando il minimo numero di parentesi secondo le convenzioni sintattiche

    ((xy)(λy.(λz.(z(xy)))))

  • Soluzione.
    Esercizio 8

    Supponendo di non utilizzare le convenzioni sintattiche sulle parentesi, riscrivere il seguente termine inserendo tutte le possibili parentesi.

    (λxyz.xy(xz))λxy.x

  • Soluzione.
    Esercizio 9

    Definire la nozione di "Currificazione". E' una nozione applicabile al lambda-calcolo? perche'?


  • Soluzione.
    Esercizio 10

    Fornire la definizione formale di sostituzione.
    Esercizio 11

    Qual e' la condizione che deve essere soddisfatta affinche' sia possibile applicare una sostituzione senza produrre "effetti indesiderati"?
    Esercizio 12

    Eseguire le seguenti sostituzioni
    Esercizio 13

    Eseguire le seguenti sostituzioni:
    Esercizio 14

    Eseguire la seguente sostituzione:

    z(λy.wy)λz.((λx.yx)xz) [yz/x,yz/w]

    Esercizio 15

    Dire qual e' il risultato della seguente sostituzione:

    ((λy.xy)(λz.y(λy.x)))[xyz/x]

    Esercizio 16

    Dire qual e' il risultato della seguente sostituzione:

    ((λy.yy)y(λy.y(λy.y)))[λy.zy/y]

    Esercizio 17

    Qual e' il risultato delle seguenti sostituzioni?
    Esercizio 18

    Qual e' il risultato della seguente sostituzione?

    ((λw.(xw))(λy.(yx)))[λx.(w(xy))/x]

    Esercizio 19

    Eseguire le seguenti sostituzioni:
    Esercizio 20

    Qual e' il risultato delle seguenti sostituzioni? Quali sono gli insiemi delle variabili legate e libere dei termini ottenuti?
    Esercizio 21

    Qual e' la condizione che deve essere necessariamente soddisfatta per poter correttamente effettuare una sostituzione M[N/x] ? Perche' tale condizione e' necessaria?

    Esercizio 22

    Eseguire le seguenti sostituzioni:
    Esercizio 23
    Fornire la definizione esplicita dell'insieme di tutti i lambda-termini in forma normale (descrivere, in modo ricorsivo, la forma che deve avere un termine in forma normale).

  • Soluzione.
    Esercizio 23.5
    Qual e', se esiste, la forma normale del seguente termine? (\x.yy)((\z.z)x))
    Esercizio 24
    Trovare la forma normale di

    (λxxxx.xx)(λx.xx)(λx.x)y((λx.x)x)

  • Soluzione.
    Esercizio 25
    Trovare la forma normale di

    (λx.((λy.z)x))((λx.xx)(λx.xx))

    Esercizio 26
    Trovare la forma normale di

    (λx.((λy.z)x))((λx.xx)(λx.xx))

    Dire inoltre se questo termine e' fortemente normalizzabile.

    Esercizio 27
    Qual e' la formal normale del seguente termine?

    ((λw.(xw))(λy.(yx)))[λx.(w(xy))/x]

    Qual e' l'insieme delle sue variabili libere? e quale quello delle sue variabili legate?
    Esercizio 28
    Fornire un lambda-termine normalizzabile il cui insieme di variabili libere sia {x, y}, e tale che l'insieme delle variabili libere della sua forma normale sia {x, y, z}.
  • Soluzione.
    Esercizio 29
    Fornire un lambda termine che si riduca a forma normale in due passi di riduzione. Inoltre tale termine deve avere {x, y, z} come insieme di variabili libere, mentre le variabili libere della sua forma normale dovranno essere {x, y}.
  • Soluzione.
    Esercizio 30
    Portare in forma normale, se esiste, il seguente lambda-termine:

    (λx.((λz.zwz)(((λxyx.y)(λx.y)(λy.x))((λx.xx)(λy.yyy)))))t



  • Soluzione.
    Esercizio 31
    Qual e' la forma normale, se esiste, del seguente lambda-termine?

    (λx.xxy)(λxy.xyy)

  • Soluzione.
    Esercizio 32
    Dire in quale caso e' possibile avere un lambda-termine con piu' di una forma normale.
  • Soluzione.
    Esercizio 33
    Qual e' la forma normale, se esiste, del seguente lambda-termine?

    (λxy.yx)(λxy.x(yy))(λx.xz(λy.yy))

  • Soluzione.
    Esercizio 34
    Qual e' la forma normale del seguente termine?

    ((λw.(xw))(λy.(yx)))[λx.(w(xy))/x]

    Qual e' l'insieme delle sue variabili libere? e quale quello delle sue variabili legate?

    Esercizio 35
    Dire se il seguente termine possiede forma normale ed eventualmente fornirla insieme ai vari passi di riduzione:

    (λxxx.((λxx.x)(xx)(λx.x)))x(xx)


  • Soluzione.
    Esercizio 36
    Dire in quale caso e' possibile avere un lambda-termine con una sola forma normale.
  • Soluzione.
    Esercizio 37
    Fornire un algoritmo di semidecisione per la proprieta' di avere forma normale.
    Perche' non puo' esistere un algoritmo di decisione?
  • Soluzione.
    Esercizio 38
    Dimostrare che se un termine M contiene Omega ( (λx.xx)(λx.xx) ) come sottotermine proprio, allora non e' normalizzabile (non possiede forma normale).
  • Soluzione.
    Esercizio 39
    Enunciare e dimostrare il Corollario di Unicita' della forma normale.
    Esercizio 40
    Fornire la definizione di alfa-conversione. Qual e' il motivo per introdurre tale nozione nel lambda-calcolo?
    Esercizio 41
    Cosa si intende per "consistenza" di una teoria? La teoria della beta-conversione e' consistente? Perche'? E la teoria della alfa-conversione?
    Esercizio 42
    Dimostrare la consistenza (consistency) della teoria della beta-conversione come corollario del teorema di Church-Rosser.
    Esercizio 43
    Fornire un lambda termine che sia normalizzabile, ma a partire dal quale esiste anche una sequenza infinita di beta-riduzioni.
    Esercizio 44
    Perche' il termine

    (λx.xx)((λy.y)z);

    e' un controesempio al fatto che la proprieta' del diamante non vale per la relazione di beta-riduzione ad un passo?
    Esercizio 45
    Fornire dei lambda termini M1 e M2 tali che M1 si puo' ridurre in piu' passi a M2, ma non si puo' ridurre ad M2 con un passo di beta riduzione parellela (=>).
    Esercizio 46
    Dimostrare con un esempio che per la relazione di beta riduzione ad un passo non vale la proprieta' del diamante (diamond property).
    Esercizio 47
    Dimostrare che la relazione di beta-riduzione parallela (=>) non e' transitiva.


  • Soluzione.
    Esercizio 48
    Dimostrare che (λx.xx)(λx.xx) non e' beta-convertibile a (λx.xx)(λx.xxx).

  • Soluzione.
    Esercizio 49
    Dare la definizione di beta-convertibilita' e dire se i termini   (IΩ)((Iy)I)     e     Ω(y(II))    sono beta-convertibili,  dove I e' λx.x  e   Ω  e' (λx.xx)(λx.xx)

    Esercizio 50
    Il termine  λx.((yy)((λz.z)x))  e' beta-eta-convertibile a (yy)? Perche'?
    Esercizio 51
    I termini   (λx.λy.(xλz.z))λa.a    e    (λy.y)λb.λz.z   sono beta-convertibili?  Perche'?
    Esercizio 52
    I seguenti termini sono beta-convertibili? Giustificare la risposta.
    • ( λy.y((λx.xx)(λx.xx)) )(λz.z)                   (λx.xx)(λx.xx)

    Esercizio 53
    Ricordiamo che se M=N allora e' possibile derivarlo a partire dall'assioma beta e dalle regole di inferenza che dicono che la beta-conversione e' una congruenza.
    Esercizio 54
    L'assioma eta non e' derivabile nella teoria della beta conversione. Comunque, per ogni termine M beta-convertibile ad una lambda-astrazione, abbiamo che λx.Mx = M, se x non appartiene alle variabili libere di M.
    Perche'?


  • Questa soluzione e' sbagliata, perche?.
    Esercizio 55
    Se si vuole evitare di utilizzare l'alfa-conversione oppure dover considerare i lambda-termini uguali modulo alfa-conversione, si puo' utilizzare la notazione di De Bruijn per i lambda-termini:
    le variabili sono rappresentate da numeri, i lambda non indicano esplicitamente quale variabile legano, ed un numero k indica che la relativa variabile e' legata dal k-esimo lambda che si incontra a partire dal numero e procedendo verso l'esterno del termine.
    Per esempio il termine (λx.λy.λz.z(xx))w(λx.zx) e' rappresentato nella notazione di De Bruijn con (λ.λ.λ.1(3 3))8(λ.(6 1)).
    Quale problema si incontra con questa notazione quando eseguiamo una beta riduzione? come si puo' risolvere?
    Esercizio 55
    I seguenti termini sono o no beta-riducibili ad una hnf?
  • Y
  • Y not
  • K == λxy.x (Quindi K non è altro che true!)
  • Y I
  • x omega
  • Y(K x)
  • n


  • Soluzione.
    Esercizio 56
    Discutere brevemente in che modo la proprieta' del diamante per la relazione di beta-riduzione parallela ( => ) e' utilizzata nella dimostrazione del teorema di Church-Rosser.
    Esercizio 57
    Enunciare il teorema di Church-Rosser.
    Cos'e' la proprieta' del diamante per una relazione?
    Fornire un esempio che mostri che per la relazione di beta-riduzione ad un passo non vale la prorpieta' del diamante.
    Esercizio 58
    Quali delle seguenti equazioni sono vere nella teoria della beta-conversione? Perche'?
    Esercizio 59
    Sia => la relazione di beta-riduzione parallela e I il lambda termine λx.x
    Quali delle seguenti relazioni sono vere? Perche'?
  • Soluzione.
    Esercizio 60
    Considerate i seguenti termini Se applicati a numerali di Church calcolano la stessa funzione sui naturali?
    Esercizio 61
    Dire se i due seguenti termini sono beta-convertibili.

    (DDD)((λx.xxx)D)

    ((λy.yyy)D)(DDD)

    dove D e' il termine λy.yy
  • Soluzione.
    Esercizio 62
    Supponiamo di voler definire nel lambda-calcolo un termine J che servisse a confrontare nomi di variabili. J dovrebbe avere il seguente comportamento: per ogni coppia di variabili distinte y e z, Jyz -->> false, mentre, per ogni variabile x Jxx -->> true, dove true e false sono i lambda termini che rappresentano i valori di verita'.
    Perche' un termine con queste caratteristiche non e' definibile nel lambda-calcolo?

    (Aiutone: all'interno di un termine, un sottotermine della forma Jxy potrebbe diventare Jxx dopo una qualche beta riduzione).

  • Soluzione.

    Esercizio 63
    Dire se, e perche', i due seguenti lambda-termini sono beta-convertibili.

    (DDDx)((λx.xxxy)D)

    ((λx.xxxy)D)(DDDx)

    dove D e' il termine λy.yy
  • Soluzione.
    Esercizio 64
    Supponete che, nella definizione della beta-riduzione parallela "=>", la clausola
    (λx.M)N => M'[N'/x] if M => M' and N => N'
    venga sostituita semplicemente con
    (λx.M)N => M[N/x]
    Questo dovrebbe causare la perdita' della proprieta' del diamante per la relazione "=>", e questo fatto sarebbe mostrato dal termine (λy.((λx.xx)(Ia)))I
    E' vero? motivare la risposta.

  • Soluzione.
    Esercizio 65
    Dato un lambda-termine M, l'insieme { N | esiste P. M => P e P => N } e' ricorsivo?
    la relazione => e' la beta-riduzione parallela usata nella dimostrazione del teorema di Confluenza.

  • Soluzione.
    Esercizio 66
    Sia (-)* la funzione utilizzata nella dimostrazione della proprieta' del diamante della beta-riduzione parallela in 0 o piu' passi (=>).
    Si consideri l'insieme { M | (M)* non contiene beta-redessi}.
    Tale insieme e' ricorsivo? Perche'?
  • Soluzione.
    Esercizio 67
    Considerate i due seguenti termini: λnfx.f(nfx) e λnfx.nf(fx)
    Se applicati a numerali di Church calcolano la stessa funzione sui naturali?
  • Se si, quale? Dimostrarlo formalmente. Sono termini beta-convertibili? Perche', intuitivamente, pur calcolando la stessa funzione non e' da ritenersi "sconveniente" che non siano beta-convertibili?
  • Se no, quali funzioni distinte calcolano? Dimostrarlo formalmente. Sono termini beta-convertibili? Perche', intuitivamente, pur calcolando funzioni distinte non e' da ritenersi "sconveniente" che siano beta-convertibili?

  • Soluzione.
    Esercizio 68
    Dimostrare che se P -->beta Q allora FV(Q) e' un sottoinsieme di FV(P).

  • Soluzione.
    Esercizio 69
    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.

  • Soluzione.
    Esercizio 70
    Spiegare perche' talvolta, prima di eseguire una beta-riduzione, occorra rinominare le variabili legate (della lambda astrazione). In tali casi, si riuscirebbero ad evitare problemi se si operasse invece sulle variabili dell'argomento della beta riduzione? Motivare.
    Esercizio 71
    Trovare tre termini M,P e Q, tali che M contiene x e y tra le sue variabili libere e tali che M[P/x,Q/y] sia diverso da M[P/x][Q/y]
    Esercizio 72

    Fornire la definizione formale (o al limite quella informale) della funzione (-)* da lambda-termini a lambda-termini.
    Descrivere in quale punto si utilizza nella dimostrazione del Teorema di Confluenza per il lambda-calcolo.
    Esercizio 73

    Dimostrare che il lambda-termine

    (λx.xxx)(λx.xxx)

    non e' normalizzabile.

  • Soluzione.


    Esercizio 74

    Dimostrare che

    (λx.xy)(λy.y) = (λyz.(λx.x)z)xy


  • Soluzione.

    Esercizio 75

    Dimostrare che

    Y(Y(YY)) = (YY)((YY)(Y(YY))).


  • Soluzione.

    Esercizio 76

    Quali sono i punti fissi del seguente lambda termine?

    λx.x

    Qual'e' quello che si ottiene attraverso l'operatore di punto fisso Y?

    Esercizio 77


    Dimostrare che (λx.xx)(λx.xx) non e' beta-convertibile a (λx.xx)(λx.xxx).

  • Soluzione.

    Esercizio 78

    Dimostrare che non puo' esistere alcun lambda termine F tale che, per qualsiasi M ed N, F(MN) = M.



  • Soluzione.

    Esercizio 79

    Dare un controesempio che mostri che, se vale che per ogni P MP = NP, questo non implica che M = N.

    Aiutone: C'entra la nozione di estensionalita' e quindi l'assioma di eta-conversione.
    Esercizio 80


    Dare la definizione di lambda-definibilita' di funzioni sui numeri naturali.
    Dimostrare che la funzione successore appartiene alla classe di funzioni lambda-definibili e che tale classe e' chiusa per composizione.

    Esercizio 81


    Scrivere esplicitamente il lambda-termine che rappresenta la funzione prodotto quando questa e' definita ricorsivamente a partire dalla funzione somma : x*y = if (x=0) then 0 else (y + (x-1)*y).

  • Soluzione.

    Esercizio 81.5
    Qual e' la principale differenza tra il comportamento dell'operatore di punto fisso di Church Y e quello di Turing Θ  ?
    Esercizio 82


    Qual'e' la funzione rappresentata dal seguente lambda-termine?

    Y(λf.λx.if x=0 then 1 else if x=1 then 1 else f(x-2) )

  • Soluzione.
    Esercizio 83


    Scrivere esplicitamente il lambda-termine che rappresenta la funzione prodotto quando questa e' definita ricorsivamente a partire dalla funzione somma : x*y = if (x=0) then 0 else (y + (x-1)*y).
    Si supponga di avere gia' i lambda-termini if, add, iszero, pre e, crepi l'avarizia, Y.
    Esercizio 84


    Fornire la definizione di funzione lambda-definibile.
    Dimostrare che la funzione successore sui numeri naturali e' lambda-definibile.
    Esercizio 85
    Qual e' la funzione su numeri naturali lambda-definita dal seguente lambda-termine?

    Y(λf.λnm.if(iszero n) m (if (iszero m) n (succ (f (pre n) (pre m)))) )

    dove i lambda termini if, add, iszero, succ, pre sono la lambda-rappresentazione dell'if-then-else, la somma, il predicato vero su 0 e falso sugli altri numeri, il successore ed il predecessore.

  • Soluzione.

    Esercizio 86
    Supponendo di avere gia' definito nel lambda calcolo le funzioni succ (successore) e mult (moltiplicazione), definire la funzione sqr (quadrato).
    Supponendo poi di avere anche definito la funzione cons, il numerale di Church zero e l'operatore di punto fisso Y, definire i lambda-termini corrispondenti
  • alla lista infinita formata da tutte x,
  • alla lista infinita formata dai quadrati di tutti i naturali.
    possibile aiutino: definire, tramite Y, la funzione che, preso un naturale n restituisca la lista infinita dei quadrati dei naturali da n in poi.
    Mostrare qualche passo di riduzione dei termini cosi' definiti.

  • Soluzione.

    Esercizio 86.5
    Cosa rappresenta il seguente termine?
                                 (Y(λf.λn.cons (mult 2 n) (f (succ n))) ) 0
    Esercizio 87
  • Il seguente lambda-termine e' in head-normal form? Se si, possiede altre head-normal forms? Quali? Se no, possiede una head-normal form?

    λxy.((λyx.x(yy))z(λz.zz))

  • Un lambda-termine puo' avere piu' di una head-normal form? Se no, quale teorema ce lo garantisce? Se si, fornire un lambda-termine con piu' di una head-normal form.
  • Come si puo' interpretare il fatto che un termine possieda una head-normal form?

  • Soluzione.


    Esercizio 88
    Mostrare come e a cosa si riduce il numerale di Church c3 applicato a c2.
    Scrivere esplicitamente un termine la cui forma normale sia il numerale di Church c10000000000

    Esercizio 89
    Quali sono i lambda-termini che NON ammettono punto fisso? Giustificare la risposta.



    ESERCIZI REDUCTION STRATEGIES
    Esercizio 1


    Cos'e' una strategia di riduzione?

    Esercizio 2


    Cosa si intende per strategia di riduzione Call-by-value?

    Esercizio 3


    Dimostrare che le strategie di riduzione leftmost-outermost e lazy formalizzate negli appunti del corso sono deterministiche.

  • Soluzione.
    Esercizio 4


    Dare la definizione di strategia di riduzione, strategia di riduzione call-by-value, strategia di riduzione call-by-name, strategia leftmost-outermost.
    La strategia leftmost-outermost e' call-by-value o call-by-name ?

    Esercizio 5


    Fornire degli assiomi e delle regole che definiscano nel lambda-calcolo la strategia di riduzione rightmost-innermost (quella che in un termine seleziona il redex piu' interno e piu' a destra).

  • Soluzione.

    Esercizio 6


    Fornire un controesempio che mostri che la strategia leftmost-outermost non e' in genere ottimale (non permette cio' di raggiungere la forma normale, se esiste, con il minimo numero di passi)