Vai alla Home Page About me Courseware Federica Living Library Federica Federica Podstudio Virtual Campus 3D Le Miniguide all'orientamento Gli eBook di Federica La Corte in Rete
 
 
Il Corso Le lezioni del Corso La Cattedra
 
Materiali di approfondimento Risorse Web Il Podcast di questa lezione

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 (t1 t2). Applichiamo dunque la rego-la relativa, iniziando col trovare la forma canonica dei sottotermini;
    • Il termine t1 ´ λx. λy. λz. ((x,z), (y,z)) è già in forma canonica;
    • Il termine t2 è una “finta ricorsione” e la forma canonica è λx. x+1;
    • Visto che t1 è 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);

Un esempio “performante”

Nella valutazione lazy di un’espressione della forma:

let x = N

consiste nel rimandare la valutazione di N fino a quando non è richiesto il valore di x.

Esempio: Si consideri il termine

let x= N in 1

con N espresso in figura.

Perchè calcolare N se il risultato sarà comunque 1?

Va notato che, adottando la valutazione lazy, non sempre si risparmia “tempo di calcolo”. Lo si risparmia nel caso dell’esempio precedente, ma lo si triplica per let x = N in (x + x + x).


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| τ1 * τ2 | τ1 → τ2

dove

  • int -> termine valutato con numero
  • τ1 * τ2 -> termine valutato coppia
  • τ1 → τ2 -> termine valutato funzione

Sintassi dei termini

Assumendo che a ciascuna variabile x di Var sia associato un unico tipo, dato da type(x), la sintassi dei termini è resa in figura.


Termini tipabili

Nella valutazione lazy (come nel caso della valutazione eager) un termine t è tipabile, cioè

t : τ

se corrisponde a un tipo (int, τ12, τ1→τ2), secondo le seguenti regole (di tipo):

  • Variabili, operazioni, let, prodotti e funzioni hanno le stesse regole di tipo del caso eager
  • Il rec, invece, ha la regola di tipo in figura (a destra quella eager)

Le variabili libere dei termini si calcolano con le regole introdotte per eager, ad eccezione del termine rec che ha la regola:

  • FV(rec x.t)=FV(t)n{x}
  • Nel caso eager si ha invece FV(rec y.(λx. t))=FV(λ x.t)n{x}

Semantica operazionale lazy

  • Nella semantica operazionale lazy (come nel caso eager) si utilizzano forme canoniche dei termini.
  • t 2 Clτ indica che t è una forma canonica lazy di tipo τ, ed è definita per induzione strutturale su τ nel modo seguente:
    • n 2 Clint (i numeri sono forme canoniche)
    • (t1,t2) 2 Clτ1*τ2 se t11 & t22 con t1 e t2 chiusi;
    • λx.t 2 Clτ1→τ2 se λx.t : τ1 → τ2 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”

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

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


Valutazione di funzioni, let e rec

Si noti come la sostituzione nel Let e nelle funzioni viene fatta senza richiedere la valutazione del termine da sostituire, dunque l’idea è quella di passare oggetti non ancora valutati.


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).
  • Contenuti protetti da Creative Commons
  • Feed RSS
  • Condividi su FriendFeed
  • Condividi su Facebook
  • Segnala su Twitter
  • Condividi su LinkedIn
Progetto "Campus Virtuale" dell'Università degli Studi di Napoli Federico II, realizzato con il cofinanziamento dell'Unione europea. Asse V - Società dell'informazione - Obiettivo Operativo 5.1 e-Government ed e-Inclusion