Aniello Murano » 13.Linguaggi con Tipi di Ordine Superiori

Prefazione

• In questa seconda parte del corso parleremo di linguaggi di ordine superiore.
• Si tratta di linguaggi più articolati di IMP in cui sono ammesse anche funzioni come valori possibili.
• In questa lezione considereremo un linguaggio Eager. Di questo linguaggio vedremo:
  • La sintassi dei termini del linguaggio (cioè gli oggetti che possiamo costruire a partire da una grammatica data).
  • Il calcolo del “tipo” associato ad ogni termine, cioè stabilire il termine di che tipo è (per esempio il termine 3+5 è di tipo intero).
  • La semantica operazionale Eager per il calcolo del significato di un termine del linguaggio considerato.

I tipi nei linguaggi di programmazione

• Un sistema dei tipi per un linguaggio di programmazione è un insieme di regole che consentono di dare un tipo ad espressioni, comandi ed altri costrutti del linguaggio.
• Un linguaggio si dice tipato se per esso è definito un tale sistema; altrimenti si dice non tipato.
• Il processo che porta alla determinazione di un tipo per i termini di un linguaggio si chiama controllo dei tipi (type checking).
• Lo scopo di un sistema dei tipi è quello di evitare che durante l’esecuzione di un programma occorrano errori quali, ad esempio, l’applicazione di funzioni ad argomenti inappropriati o il riferimento illegale della memoria.
• La definizione di una teoria dei tipi, ovvero un sistema dei tipi dato sotto forma di regole formali di deduzione, permette, tramite una semantica formale, di dimostrare matematicamente proprietà del linguaggio.

Il λ-calcolo

• Il λ-calcolo è un formalismo generale per rappresentare funzioni.
• Il λ-calcolo definisce la stessa classe di funzioni che è definita dalle Macchine di Turing.
• Da questa uguaglianza la tesi di Church che congettura che questa sia la classe di tutte le funzioni calcolabili.
• λx.t è una λ-astrazione definisce una funzione con un parametro “formale” x. Ad esempio λx.x+1 denota la funzione successore.
• In λx.t, λ lega x nel termine t (scope del legame) ed x è legata (bound) in λx.t
• Importante: λx.t è solo un segna-posto e possiamo rinominarla a piacimento, rinominando anche le occorrenze di x in t.
  • Ad esempio, la funzione identità può essere scritta λx.x oppure λy.y

Tecniche di Valutazione

Esistono due tecniche fondamentali di valutazione per i linguaggi funzionali:

• Eager/Call by value: Gli argomenti sono valutati prima della chiamata a funzione
• Lazy/Call by name: Gli argomenti sono valutati quando essi vengono utilizzati dalle funzioni
• La scelta Eager/Lazy porta a linguaggi il cui comportamento è riconducibile:
  • nel caso Eager, a quello dei linguaggi ML, LISP e Schema (un dialetto di LISP);
  • nel caso Lazy, a quello di Miranda, Orwell e Haskell.

Valutazione Eager

• La valutazione Eager è la strategia di valutazione maggiormente utilizzata nei linguaggi di programmazione.
• Nella valutazione Eager, una espressione è valutata non appena viene assegnata ad una variabile.
• I vantaggi della valutazione Eager risiedono in un minor consumo di memoria e una maggiore velocità di esecuzione dei programmi.
• Per esempio, si considerino le seguenti istruzioni:
  • x = 5 + 3 * (1 + 5^2);
  • print x;
  • print x + 2;
• In questo caso non solo la valutazione Eager permette di salvare spazio (in quanto conserviamo il valore 83 dell’espressione, invece dell’espressione stessa), ma permette di valutare l’espressione una sola volta e non ogni volta che viene usata.

Valutazione Lazy (prossima lezione)

• La valutazione Lazy (conosciuta anche come valutazione ritardata) 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 Eager

• Esistono termini la cui valutazione (Eager) può produrre valori di base, come per esempio i numeri, oppure coppie di valori o funzioni.
• Per tener conto della diversa natura dei valori prodotti dalla valutazione dei termini, si introducono i tipi per le espressioni, indicati con τ, e definiti come segue:

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

dove:

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

Esempi

Calcolo del Fattoriale di n (per n>0):

• rec fact.(λn. (if n-1 then n else n * fact(n-1)))

Calcolo dell’n-esimo numero di Fibonacci:

• rec fib.(λn. (if n then n else if n-1 then n else fib(n-1) + fib(n-2)))

Uno sguardo a O’Caml per il numero di Fibonacci:

• let rec fib = fun n -> if n < 2 then n else fib(n-1) + fib(n-2)

Esercizio: Scrivere il termine per la funzione ricorsiva f(n)=2ⁿ

Variabili libere di un termine

• In x+3 la variabile x è libera
• Ricordiamo che λ è un operatore che lega (binds) una variabile (binding operator). Un’occorrenza di una variabile x legata da un operatore λ (cioè che compare nello scope di un λx.) non è libera.
• L’insieme delle variabili libere di un termine t è definito per induzione strutturale su t (vedi Winskel pagina 205 per le regole).
• Un termine è chiuso quando non contiene variabili libere.

Sostituzione

La sostituzione consiste nel rimpiazzo di tutte le occorrenze di un sotto-termine con un altro, all’interno di un terzo termine.

Indichiamo con:

[x →T₂]T₁ oppure T₁[T₂ / x]

la sostituzione del termine T₂ al posto di ogni occorrenza di variabile libera x all’interno del termine T₁, il quale funge da contesto.

Un esempio di sostituzione è il seguente:

[x → t²] λy. log(y + x) =λy. log(y + t²)

Regole di sostituzione (I tentativo)

Di seguito una definizione ricorsiva dell’algoritmo di sostituzione

• [x → t₁] x = t₁;
• [x → t₁] y = y; se x ≠ y
• [x → t₁] λy.t = λy.([x → t₁] t)

Cosa succede allora se applico la seguente sostituzione:

[x → y](λx.x)

Ottengo λx.y cioè la variabile legata è diventata libera!!

Regole di sostituzione (II tentativo)

Di seguito una definizione ricorsiva dell’algoritmo di sostituzione

• [x → t₁] x = t₁;
• [x → t₁] y = y; se x ≠ y
• Distinguiamo allora i seguenti casi:
  • [x → t₁] λx.t = λx.t
  • [x → t₁] λy.t = λy.([x → t₁] t) se x ≠ y

Cosa succede allora se applico la seguente sostituzione:

[x → y](λy.x)

Otteniamo λy.y cioè una variabile libera è divenuta legata dopo la sostituzione!! (fenomeno di cattura di variabili). Ciò è dovuto al fatto che la variabile y legata al λ è anche presente tra le variabili libere del termine che t₁ che subentra (cioè y 2 FV(t₁)= FV(y) ={y}.

Regole di sostituzione (definiz. finale)

Di seguito una definizione ricorsiva dell’algoritmo di sostituzione

• [x → t₁] x = t₁;
• [x → t₁] y = y; se x ≠ y
• Distinguiamo allora i seguenti casi:
  • [x → t₁] λx.t = λx.t
  • [x → t₁] λy.t = λy.([x → t₁] t) se x ≠ y e y ∉ FV(t₁)
  • [x → t₁] λy.t = λz.([x → t₁] [y → z]t) se x ≠ y e y 2 FV(t₁)

Dove z è una nuova variabile non presente né in t, né in t₁

Semantica operazionale eager

Nella semantica operazionale si utilizzano forme canoniche dei termini mentre nella semantica denotazionale si usano i loro valori.

In generale, un insieme di regole che esprimono un dato concetto sono in forma canonica se esse sono nella forma più semplice possibile, senza però perdere di generalità.

• t 2 C^e_τ indica che t è una forma canonica di tipo τ, ed è definita per induzione strutturale su τ nel modo seguente:
• n 2 C^e_int (i numeri sono forme canoniche)
• (c₁,c₂) 2 C^e_τ1*τ2 se c₁ 2 C^e_τ1 e c₂ 2 C^e_τ2;
• λx.t 2 C^e_τ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 → ^ec.

Valutazione di operatori e condizioni

Valutazione delle coppie

Valutazione di funzioni, let e rec

Esempi ed esercizi

Il termine (λx. λy. x+y     5) non è in forma canonica, mentre lo è il termine (λy. 5+y)

Esercizio

Si derivi la valutazione del termine

rec f. (λz. if z then 1 else z * f(z-1))

La valutazione è deterministica

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

Forme Canoniche

In mathematics, a canonical form is a function that is written in the most standard, conventional, and logical way. For example, polynomials are usually written with the terms in descending powers: it is more usual to write x² + x + 30 than x + 30 + x², although the two forms are essentially equivalent.

A canonical form is required to have two essential properties:

• Every object under consideration must have exactly one canonical form
• Two objects that have the same canonical form must be essentially the same