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
 
I corsi di Scienze Matematiche Fisiche e Naturali
 
Il Corso Le lezioni del Corso La Cattedra
 
Materiali di approfondimento Risorse Web Il Podcast di questa lezione

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.

Linguaggi con tipi di Ordine Superiore

  • Si tratta di linguaggi che ammettono anche funzioni come valori: dunque, è possibile scrivere una procedura che prende in input una funzione e restituisce una funzione!
  • La progettazione dei linguaggi funzionali è basata su funzioni matematiche (a differenza di quelli imperativi, basata sulla architettura di von Neumann degli elaboratori).
  • La base teorica dei linguaggi funzionali è rappresentata dal lambda-calcolo.
  • Il λ-calcolo è stato definito da Alonso Church nel 1933.

Alonzo Church (14 giugno, 1903 – 11 agosto, 1995), matematico e logico americano, co-fondatore dell’informatica. In un suo famoso articolo del 1936 mostra l’esistenza di un “problema indecidibile”. Questo risultato precedette il famoso lavoro di Alan Turing sul problema della fermata.

Alonzo Church

Alonzo Church


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| τ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 è mostrata in figura.


Termini tipabili

Un termine t è tipabile, cioè t : τ, se corrisponde a un tipo:

int τ12 oppure τ1→τ2

secondo le seguenti regole (di tipo):

  • Variabili
    • x : τ se type(x) = τ
  • Operazioni
    • n : int
    • se t1 : int & t2 : int allora t1 op t2 : int (dove op è una operazione aritmet.)
  • Per i prodotti e le funzioni si veda Winskel a pagina 203
  • Let e REC
  • Un termine è univocamente tipato se esiste un solo tipo possibile corrispondente (si provi per esercizio che questo vale per i termini considerati).
Let e REC

Let e REC


Esercizio 1

Verificare se il termine seguente è tipabile. In tale caso, mostrarne il tipo, descrivendo tutte le regole di tipo utilizzate.

if fst(x) then (snd(x), fst(x)) else x

Soluzione [Sketch]:

  • Dalla regola di tipo dell ‘if, segue la figura 1.
  • Per la regola di fst(x), segue che x è di tipo coppia con il primo termine intero, dunque x: τ ´ int*τ1 per un opportuno τ1
  • Siccome (snd(x), fst(x)) : τ ´ int*τ1 segue che snd(x): int
  • Dunque il termine è di tipo τ ´ int*int
Figura 1

Figura 1


Esercizio 2

Provare che λx. λy. λz. if z then (x y) else (y x) non è tipabile

Soluzione[Sketch]:

  • Tralasciando la valutazione per λ e per l’if (da completare per esercizio), per le funzioni si ha la figura 2.
  • Dalle regole precedenti segue che τ1 ´ τ3 ! τ4
  • Siccome τ3 ´ τ1 ! τ2, segue che τ1 ´ τ1 ! τ2 ! τ4 che è ricorsivo.
  • Dunque il termine non è tipabile.
Figura 2

Figura 2


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)=2n

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 →T2]T1 oppure T1[T2 / x]

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

Un esempio di sostituzione è il seguente:

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

Regole di sostituzione (I tentativo)

Di seguito una definizione ricorsiva dell’algoritmo di sostituzione

  • [x → t1] x = t1;
  • [x → t1] y = y; se x ≠ y
  • [x → t1] λy.t = λy.([x → t1] 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 → t1] x = t1;
  • [x t1] y = y; se x ≠ y
  • Distinguiamo allora i seguenti casi:
    • [x → t1] λx.t = λx.t
    • [x t1] λy.t = λy.([x t1] 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 t1 che subentra (cioè y 2 FV(t1)= FV(y) ={y}.

Regole di sostituzione (definiz. finale)

Di seguito una definizione ricorsiva dell’algoritmo di sostituzione

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

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

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

Attenzione

  • Non sempre è possibile scrivere un termine in forma canonica. Quando questo non è possibile, abbiamo una situazione analoga a quella di computazioni non terminanti viste per IMP.
  • Per esempio, il termine t ´ (rec f. (λx. (f x) 5)) non ha forma canonica.
  • Il termine t è una applicazione (t1 t2).
  • Per applicare la regola corrispondente, siccome t2 è già in forma canonica, occorre lavorare solo su t1
    t1 è un rec e per la regola corrispondente abbiamo:
  • rec f. (λx. (f x) →e λx.[f →t1 ] (f x) ´ λx. (rec f. (λx. (f x) x)
  • Ritornando alla regola delle applicazioni, la forma canonica di t è data da [x → 5] (rec f. (λx. (f x) x) ´ t.
  • Si noti come, per le regole di sostituzione, la x nello scope del lambda non viene sostituita (la seconda è invece libera).

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 x2 + x + 30 than x + 30 + x2, 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
  • 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