Aniello Murano » 14.Valutazione Lazy

Prefazione alla lezione

• Nella lezione precedente abbiamo introdotto i linguaggi (funzionali) con tipi di ordine superiore.
• Si tratta di linguaggi più articolati di IMP in cui sono ammesse anche funzioni come valori (è possibile scrivere una procedura che prende in input e restituisce in output una funzione).
• La progettazione di tali linguaggi si basa su funzioni matematiche.
• Per ogni termine del linguaggio è possibile calcolarne il “tipo” tramite l’uso di regole.
• La valutazione (operazionale) di un termine è data tramite l’uso di “forme canoniche“.
• Esistono due tipi di valutazione per i linguaggi funzionali:
  • Valutazione Eager o Call by value (lezione precedente), in cui gli oggetti sono valutati il prima possibile.
  • Valutazone Lazy o Call by name (questa lezione), in cui la valutazione degli oggetti è rinviata al momento in cui tali valori sono di fatto usati.

Esercitazione su termini tipabili

Mostrare che il termine seguente è tipabile utilizzando le regole (di tipo) per la determinazione del relativo tipo :

if ((λx. λy. x+y z) k) then (z , k) else (k , z)

Alcuni suggerimenti per la soluzione:

1. x e y devono essere interi; z e k dello stesso tipo;
2. La guardia dell’if deve essere intera, dunque λx. λy. x+y è di tipo int → int → int e z di tipo intero
3. Dunque il termine è tipabile e il tipo del termine è int*int

Esercitazione su valutazione eager

• Il termine (λx. λy. x+y 5) non è in forma canonica, mentre lo è il termine (_y. 5+y). “Esercizio per gli studenti“.
• Valutare se il termine (λx. λy. λz. ((x,z), (y,z)) rec f. λx. x+1) è in forma canonica.
• Suggerimenti per la soluzione:
  • Il termine dato è una applicazione (t₁ t₂). Applichiamo dunque la rego-la relativa, iniziando col trovare la forma canonica dei sottotermini;
  • Il termine t₁ ´ λx. λy. λz. ((x,z), (y,z)) è già in forma canonica;
  • Il termine t₂ è una “finta ricorsione” e la forma canonica è λx. x+1;
  • Visto che t₁ è di tipo λx.t, possiamo applicare la regola di valutazione. Dunque la forma canonica del termine dato è ottenuta sostit. x in t con la forma canonica di t2 (cioè λy. λz. ((x,z), (y,z)) [x → λx. x+1]);
  • Risposta: la forma canonica del termine è λy. λz. ((λx. x+1,z), (y,z))

Valutazione Lazy

• La valutazione Lazy (conosciuta anche come valutazione pigra) consiste nel posticipare la valutazione di una computazione fino a quando (e ogni volta) il risultato della computazione è realmente usato.
• Tra i vantaggi della valutazione Lazy ricordiamo:
  • Aumento delle performance di un programma in seguito alla non valutazione di componenti non necessari alla computazione;
  • Riduzione della possibilità di incontrare errori nella valutazione condizionale di computazioni (l’errore potrebbe essere nella diramazione di un comando “if” che non verrà mai preso);

Linguaggio Lazy

Come nel caso eager, esistono termini la cui valutazione può produrre valori di base (numeri), coppie di valori o funzioni.

Per tener conto della diversa natura dei valori prodotti dalla valutazione dei termini, consideriamo anche in questo caso il concetto di “tipi” per le espressioni, indicati con τ, e definiti come segue:

τ ::= int| τ₁ * τ₂ | τ₁ → τ₂

dove

• int -> termine valutato con numero
• τ₁ * τ₂ -> termine valutato coppia
• τ₁ → τ₂ -> termine valutato funzione

Semantica operazionale lazy

• Nella semantica operazionale lazy (come nel caso eager) si utilizzano forme canoniche dei termini.
• t 2 C^l_τ indica che t è una forma canonica lazy di tipo τ, ed è definita per induzione strutturale su τ nel modo seguente:
  • n 2 C^l_int (i numeri sono forme canoniche)
  • (t₁,t₂) 2 C^l_τ1*τ2 se t₁:τ₁ & t₂:τ₂ con t₁ e t₂ chiusi;
  • λx.t 2 C^l_τ1→τ2 se λx.t : τ₁ → τ₂ e λx.t è chiuso.
• Dunque le forme canoniche sono particolari termini chiusi.
• Definiamo ora le regole di inferenza in grado di ridurre un termine chiuso tipabile t in una forma canonica c, cioè t →^lc.
• Nella lazy, la coppia è già considerate in forma canonica. Nella eager, invece, la coppia deve essere trasformata in forma canonica.

Valutazione di operatori e condizioni (come in eager)

Attenzione, il simbolo “e” sulle derivazioni va cambiata con il simbolo “l”

Valutazione del prodotto

Si noti che viene valutato un solo elemento della coppia e non entrambi come invece avveniva nella eager

Esercizio 1

Verificare se esiste la forma canonica lazy del seguente termine:

(rec f. λx. (f x) 5)

Soluzione: Nella lezione precedente, abbiamo mostrato che non esiste una forma canonica eager del termine. Con una valutazione analoga è possibile dimostrare che non ne esiste una lazy.

Esercizio 2

Verificare se esiste la forma canonica (e se si quale) eager e lazy del seguente termine:

fst(5+5, (rec f. λx. (f x) 5))

Soluzione:

1. Non esiste una forma canonica eager perché il secondo termine della coppia non è in forma canonica.
2. Esiste la forma canonica lazy che è 10. Questo perché, a differenza della eager, nella valutazione lazy del first di una coppia, non occorre che il secondo termine sia in forma canonica.

La valutazione lazy è deterministica

• Per dimostrare che la valutazione è deterministica occorre provare che per ogni termine se t →^lc e t →^lc’ allora c ´ c’.
• La precedente proprietà è facilmente dimostrabile per induzione sulle regole di derivazione date (esercizio per gli studenti).