ESERCIZI LAMBDA CALCULUS


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

    Esercizio 42

    Esercizio 43
    Fornire un lambda termine che sia normalizzabile, ma a partire dal quale esiste anche una sequenza infinita di beta-riduzioni.
    Esercizio 44
    Cos'e' una strategia di riduzione?
    Esercizio 45
    Cosa si intende per strategia di riduzione Call-by-value?
    Esercizio 46
    Dimostrare che le strategie di riduzione leftmost-outermost e lazy formalizzate negli appunti del corso sono deterministiche.

  • Soluzione.
    Esercizio 47
    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 48
    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 49
    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)
    Esercizio 50-67

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

  • Soluzione.
    Esercizio 69

    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

    Esercizio 73

    Dimostrare che il lambda-termine

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

    non e' normalizzabile.

  • Soluzione.


    Esercizio 74

    Cosa si intende per Principal Pair nel lambda calcolo? Descrivere l'algoritmo di principal pair.


    Esercizio 75

    Enunciare il Teorema di Confluenza del λ-calcolo ed utilizzarlo per dimostrare la proprieta' di unicita' della forma normale.



    Esercizio 76

    Fornire la definizione formale di sostituzione per il lambda-calcolo.
    Trovare poi tre termini M,P e Q, tali che M contenga x e y tra le sue variabili libere e tali che M[P/x,Q/y] sia diverso da M[P/x][Q/y]
  • Soluzione.


    Esercizio 77

    Definire formalmente la nozione di sostituzione nel λ-calcolo.
    Effettuare la seguente sostituzione e ridurre il termine ottenuto, se possibile, in forma normale.
    ((λw.(xw))(λy.(yx)))[λx.(w(xy))/x]

  • Soluzione.


    Esercizio 78

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


    Esercizio XX


  • Soluzione.


    Esercizio XX


  • Soluzione.