(Laboratorio di)Linguaggi di Programmazione

Corso di Laurea in Matematica – A.A. 2010/2011

Giulio Caravagnacaravagn@di.unipi.it

7 giugno 2011

Sommario

Appunti (informali, colloquiali e non revisionati) per il laboratorio del corso di Linguaggi di Pro-grammazione tenuto nell’ a.a. 2010/11 dal Prof. Degano. Queste note, costruite partendo dalladispensa realizzata negli anni precedenti da Paolo Milazzo, non pretendono di sostituire alcunodei libri di testo consigliati durante il corso. Tuttavia, possono servire allo studente per una breveconsultazione prima/durante/dopo il corso.

Giulio Caravagna,

7 giugno 2011.

“We believe that ML contain[s] features worthy ofserious consideration; these are the escape mechanism,and the polymorphic type discipline ..., and also theattempt to make programming with functions -includingthose of higher type- as easy and natural as possible.”

Robin Milner,Edinburgh LCF 1979

1

Indice

1 Introduzione 31.1 Preambolo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31.2 Linguaggi di programmazione . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31.3 Breve storia di “ML” (e “Caml”) . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71.4 Esecuzione di programmi Ocaml . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8

2 SimpleCAML 92.1 Sintassi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92.2 Semantica . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

3 Da SimpleCAML a Ocaml 153.1 Pattern matching di base . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 153.2 Tipi di dato strutturati . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18

3.2.1 Tuple . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 183.2.2 Liste . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 193.2.3 Unions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20

3.3 Funzioni . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 213.3.1 Polimorfismo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 243.3.2 Curry, uncurry e valutazione parziale . . . . . . . . . . . . . . . . . . . . . . 253.3.3 Higher-order . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26

3.4 Eccezioni . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28

4 Scrivere interpreti in Ocaml 334.1 Interpretazione vs compilazione . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 334.2 Express: il linguaggio delle sole espressioni . . . . . . . . . . . . . . . . . . . . . . 344.3 σ-Express : il linguaggio delle espressioni con variabili . . . . . . . . . . . . . . . 374.4 While: un linguaggio imperativo . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39

5 Cenni di analisi statica 445.1 Type-checking del linguaggio While . . . . . . . . . . . . . . . . . . . . . . . . . . 445.2 Analisi dataflow del linguaggio While . . . . . . . . . . . . . . . . . . . . . . . . . 50

2

Capitolo 1

Introduzione

1.1 PreamboloObiettivi di questo ciclo di lezioni ed esercitazioni sono:

• fornire nozioni di base di programmazione funzionale;

• illustrare alcune differenze tra i vari paradigmi di programmazione;

• illustrare come costruire un interprete di un linguaggio di programmazione per un linguaggiodi cui sia data la semantica operazionale;

• illustrare nozioni di base e aspetti implementativi sul controllo dei tipi nei programmi;

• illustrare nozioni di base e aspetti implementativi sull’analisi dei programmi.

Materiale utile per il corso sono i seguenti testi:

- G.Cousineau and M.Mauny, The Functional Approach to Programming, Cambridge Univer-sity Press.

- Jason Hickey, Introduction to Objective Caml (draft)

http://www.cs.caltech.edu/courses/cs134/cs134b/book.pdf

- The Objective Caml system release 3.11, reference manual

http://caml.inria.fr/pub/docs/manual-ocaml/index.html

Gli argomenti trattati in alcune di queste lezioni si possono trovare su siti web di corsi di introdu-zione alla programmazione funzionale. Ad esempio si veda il corso tenuto da Massimo Bartolettipresso l’Univesità di Cagliari

http://unicaml.sc.unica.it/doku.php

1.2 Linguaggi di programmazioneI linguaggi di programmazione si dividono in (almeno) tre classi principali:

• linguaggi imperativi (e.g. C, Pascal, Basic, . . . );

• linguaggi a oggetti (e.g. C++, Java, . . . );

• linguaggi dichiarativi (e.g. ML, Haskell, Prolog, Lisp . . . ).

Nei linguaggi imperativi un programma è costituito da una sequenza di comandi i quali:

3

• leggono lo stato del calcolatore (e.g. i valori in memoria);

• modificano lo stato del calcolatore (e.g. i valori in memoria);

• controllano il flusso di esecuzione del programma stesso.

Implementare una funzione in un linguaggio imperativo significa specificare la sequenza di passiche servono per calcolarne il risultato a seconda dell’input (vedi il paragrafo successivo “Iterazionev.s. Ricorsione per un esempio di definizione di funzioni in C).

I linguaggi a oggetti, che non considerati in questo ciclo di lezioni, sono sostanzialmente un’e-stensione dei linguaggi imperativi con construtti che semplificano la suddivisione dei programmi inmoduli indipendenti. Nei linguaggi ad oggetti esiste il concetto di classe la quale definisce un tipoe le possibili operazioni effettuabili su quel tipo, e di oggetto inteso come istanza di una classe. Lanozione di classe permette di stabilire gerarchie non banali tra i tipi mediante relazioni d’ordine, inpratica si introducono nozioni come sottoclasse e superclasse al fine di ottenere ereditarietà e certeforme di polimorfismo.

Example 1 Il seguente è un esempio Java di definizione di una classe Foo la quale offre unmetodo principale main che stampa un messaggio all’utente.

// Una definizione di classepublic class Foo{

// varibile (statica)private static String fie = "Ciao ciao ";

// un metodopublic static void main(String [] arg){

System.out.println(fie + " Pippo!");}

}

I linguaggi dichiarativi si dividono in due classi principali:

• i linguaggi logici, i cui programmi sono insiemi di clausole; logiche.

• i linguaggi funzionali, i quali traggono ispirazione dal modo in cui le funzioni vengono definitein ambito matematico.

In un linguaggio logico è possibile, ad esempio, definire una base di conoscenza in termini di unaserie di predicati ed effettuare delle interrogazioni per stabilire la soddisfacibilità di un predicato.Come per i linguaggi a oggetti, i linguaggi logici non vengono considerati in questo ciclo di lezioni.

Example 2 Il seguente è un esempio Prolog che, data una base di conoscenza espressa coni primi 4 predicati, si chiede se esiste una valore assegnabile ad X tale per cui piace(S, X) ∧piace(R, X) sia soddisfatta.

% Una serie di predicatipiace(S, soldi ).piace(S, bunga bunga).piace(S, R).piace(R, soldi ).% Cosa piace sia a S che a R?piace(S, X), piace(R, X)

I linguaggi funzionali, la cui base formale è il λ-calcolo di Church, sono appunto caratterizzatidal concetto di funzione la cui valutazione (in serie) ne definisce la nozione di flusso di esecuzione.Questa particolarità dei linguaggi funzionali li rende differenti dai linguaggi imperativi per una seriedi motivi noti e dibattuti. Ad esempio, nel paradigma funzionale non esistono side effects, ovvero

4

non si possono effettuare assegnamenti a variabili modificando lo stato del programma perchè unprogramma funzionale è, di base, immutabile, ovvero i valori non vengono trovati cambiando lostato del programma, ma costruendo nuovi stati a partire dai precedenti. Questo tipo di nozionepermette, in alcuni casi, una più facile verifica della correttezza e della mancanza di bug delprogramma e la possibilità di una maggiore ottimizzazione dello stesso.

Nel seguito si discutono alcune differenze tra il paradigma funzionale e quello imperativo, altrecosiderazioni verrano fatte nei prossimi capitoli.

Iterazione v.s. Ricorsione Prendiamo C come esempio di linguaggio imperativo e Ocaml(nella sua parte puramente funzionale) come esempio di linguaggio funzionale e confrontiamoli conun esempio: il calcolo del fattoriale. La nostra funzione di riferimento è fact : IN+ → IN+ dove

fact(n) =

{1 se n = 0,

n · fact(n− 1) altrimenti,

o analogamente

fact(n) =

{1 se n = 0,∏n

i=1 i altrimenti.

L’approccio più diffuso della programmazione imperativa è l’approccio iterativo basato sull’utilizzo di costrutti iterativi di due tipi: for e while. In linea di principio1 il costrutto fordovrebbe essere utilizzato quando si desidera ripetere un numero fissato di volte una porzionedi codice; formalmente i for-programmi dovrebbero corrispondere a funzioni primitive ricorsive.Differentemente, il costrutto while dovrebbe essere utilizzato quando non è possibile sapere aprioriquante volte debba essere ripetuta una porzione di codice. In particolare, la condizione di iterazionedi un while dovrebbe corrispondere ad un predicato che viene valutato ad ogni passo di iterazione;formalmente i while-programmi corrispondono a funzioni µ-ricorsive.

L’algoritmo (in C) che calcola la funzione fact può essere definito con un ciclo for come segue.

int fact(int n){

int ret = 1;

// eseguo il corpo n volte incrementando ifor(int i = 1; i <= n; i++){ ret = ret * i; }

return ret;}

Il significato di questi tipi di ciclo è intuitivo: se denotiamo con reti il valore della variabile retalla fine dell’iterazione i-esima del ciclo abbiamo la sequente catena di equazioni:

ret0 = ret1 = 1

ret2 = 2

ret3 = 6

. . .

reti = reti−1 · i

da cui n! = n · retn−1. In maniera simile, ma metodologicamente meno corretta/apprezzata, èpossibile implementare lo stesso algoritmo usando un costrutto while

int fact(int n){

int r=1;while (n>1) // predicato o ’guardia ’

1Questo linea di principio deriva dal fatto che i moderni linguaggi di programmazione non hanno una nettadistinzione for/while.

5

r=r*n;n=n-1;

}return r;

}

Potete riflettere sulle varie implementazioni e convincervi della loro equivalenza. Come abbiamogià detto, implementare l’algoritmo che calcola fact(n) in C è possibile sia in maniera iterativa chein maniera ricorsiva. In generale, le procedure ricorsive si possono definire su insiemi ben fondati(e.g. i naturali) e si possono usare per fare dimostrazioni di properietà per induzione.

int fact(int n){

if( n==0) return 1;else return n * fact(n-1);

}

Questa rappresenta la definizione tail-recursive2 di fact in C. Potete quindi notare che le dueimplementazioni iterative e la singola implementazione ricorsiva sono equivalenti. Molto spes-so, nell’utilizzare linguaggi che permettono sia ricorsione che iterazione si sceglie la struttura diprogrammazione che più si adatta alle esigenze del programma o dell’ambiente in cui il program-ma viene eseguito. Infatti, in generale, le funzioni ricorsive richiedono una maggiore quantità dimemoria per essere eseguite (provate a immaginare perché) e, ad esempio, in dispositivi con li-mitata capacità di memoria (e.g. cellulari, elettrodomestici) si preferisce talvolta programmare lafunzioni/procedure in maniera iterativa.

Tornando ai linguaggi funzionali abbiamo che in tali linguaggi non esistono costrutti iterativi,gli oggetti di base sono funzioni le quali, se necessario, sono definite per ricorsione. Ad esempio,la tipica implementazione in Ocaml del fattoriale è la seguente:

let rec fact n =if n=0 then

1else

n * fact (n-1)

Si noti che, indipendentemente dal paradigma di programmazione scelto (C v.s. Ocaml), loscheletro della definizione dell’algoritmo è simile, in ambedue i casi, alla definizione matematicadella funzione: si dichiara il valore della funzione per un input di base (e.g. per 0) e si definisce ilvalore per un input superiore (e.g. il caso induttivo per n) in base al valore della funzione stessaper un valore inferiore (e.g. per n− 1 in questo caso).

Un altro semplice esempio è l’Algoritmo di Euclide per calcolare il MCD di due naturali. Unapossibile implementazione iterativa (in C) di tale algoritmo dove a, b ∈ IN e a > b è la seguente

int gcd(int a, int b){

int r;while (r=a%b) != 0) {

a=b;b=r;

}return b;

}

Si noti che questa implementazione usa un while (perché?), mentre la tipica implementazionericorsiva in Ocaml è la seguente:

let rec gcd a b =let r = a mod b in

2Un tipo particolare di ricorsione in cui il valore restituito dalla chiamata ricorsiva viene restituito a sua voltadal chiamante. Questo tipo speciale di ricorsione si può compilare in modo molto efficente (i.e. senza far crescere lostack delle chiamate, perché?).

6

if r=0 thenb

elsegcd b r

Questa implementazione corrisponde alla seguente definizione matematica:

gcd(a, b) =

{b se a mod b = 0

gcd(b, a mod b) altrimenti.

Osservando le varie implementazioni di questi algoritmi nei due lingauggi di programmazionepossiamo notare delle particolarti che determinano le caratteristiche di uno o dell’altro paradigmadi programmazione, ad esempio:

• in C le variabili possono cambiare valore tramite assegnamenti (side-effects) della forma

int i = 1; (* id_variabile = valore *)

mentre in Ocaml no, più precisamente in Ocaml non ci sono assegnamenti perchè non c’èil concetto di stato/store;

• in C dobbiamo dichiarare il tipo delle variabili, ad esempio scriviamo

int i = 1; (* tipo: int id:i val:1 *)float x = 3.0 (* tipo: float id:x val :3.0 *)

mentre in Ocaml non è necessario, comunque sia la struttura dei tipi di Ocaml è più fortedi quella del C 3;

• in C dobbiamo usare una keyword (ovvero return) per esprimere la restituzione del risultatodella funzione al chiamante, mentre in Ocaml ciò è implicito.

Alcune di queste differenze verranno analizzate o almeno esplicitate nell’arco di queste lezioni,.

1.3 Breve storia di “ML” (e “Caml”)Riporto un breve estratto da scholarpedia.

“ML” stands for meta language. ML, the predecessor of Standard ML, was devised by RobinMilner and his co-workers at Edinburgh University in the 1970s, as part of their theorem proverLCF (Milner, Gordon and Wadsworth, 1979). Other early influences were the applicative languagesalready in use in Artificial Intelligence, principally LISP, ISWIM, POP2 and HOPE. During the1980s and first half of the 1990s, ML inspired much programming language research internationally.MacQueen, extending ideas from HOPE and CLEAR, proposed the Standard ML modules system(MacQueen, 1984). Other major advances were mature compilers (Appel and MacQueen, 1991),a library (Gansner and Reppy, 2004), type-theoretic insight (Harper and Lillibridge, 1994) and aformal definition of the language (Milner, Tofte, Harper and MacQueen, 1997). Further informationon the history of Standard ML may be found in the language definition (Milner et al., 1997).

Informazioni dettagliate su Caml si trovano qui

http://www.pps.jussieu.fr/∼cousinea/Caml/caml_history.html .3Al dato pratico il (quasi totale) controllo del sistema che si può avere in C utilizzando determinati tipi di

puntatori lo rende quasi un linguaggio non-tipato.

7

1.4 Esecuzione di programmi Ocaml

Gli esempi che verranno discussi in questa dispensa sono descritti in Ocaml, un linguaggio fun-zionale della famiglia di ml del quale useremo un sottoinsieme minimo. Siete invitati a provare adeseguire parte degli esempi che troverete in questa dispensa e, soprattutto, siete invitati a variarlia vostro piacimento. L’ambiente interattivo al quale ci riferiamo lo si trova in alcune distribuzioniLinux o lo si può scaricare all’indirizzo caml.inria.fr.

Per avviare l’ambiente interattivo è sufficiente digitare ocaml da una shell; l’ambiente vi mo-strerà un nuovo prompt con il simbolo #. In generale, ogni comando sarà terminato dai doppi duepunti (;;) l’ambiente risponderà con un messaggio che contiene informazioni sul comando digitato.Ad esempio:

(* questo e’ un commento , non e’ codice *)# let sumc x y = x+y;;val sumc : int -> int -> int = <fun >

Il significato è abbastanza evidente, sumc è una funzione che lavora su interi (int); il significatoesatto di int -> int -> int verrà discusso più avanti nella dispensa.

Ogni programma può essere interpretato (dall’interprete ocamlrun che interpreta byte-codeottenuto con ocamlc) o compilato (dal compilatore ocamlopt). In generale l’interprete producebytecode da eseguirsi usando il comando ocamlrun, in alternativa il compilatore produce codicenativo che dipende dalla piattaforma di compilazione. In pratica, il compilato dovrebbe esserecodice più “performante” dell’analogo interpretato, tuttavia la compilazione richiede maggior tempoe generea eseguibili di dimensioni maggiori.

Supponendo che il nostro codice sia contenuto nel file es.ml, per produrre un eseguibiledenominato es si usa il compilatore come segue

ocamlopt -o es es.ml

Il file compilato (eseguibile) si esegue (interpreta) con il comando

./es (oppure ocamlrun es).

Nel caso in cui il programma non venga compilato correttamente il compilatore fornirà il maggiornumero di informazioni utili sugli errori che hanno impedito la compilazione.

Example 3 Per considerare un esempio particolarmente semplice si consideri un programma chechiede in input una stringa e stampa un messaggio di benvenuto all’utente. Una sequenza (∗..... ∗) denota un commento, l’operatore apice concatena due stringhe ed il significato deglialtri costrutti sarà spiegato in seguito.

(* My first Ocaml program *)

print_string "Please enter your name: ";;let name = read_line ();;print_string ("Hello , " ^ name ^ "\n");;

Compilare ed eseguire questo programma è molto semplice.

dhcp130:examples caravagn$ ocamlc -o es es.mldhcp130:examples caravagn$ ocamlrun esPlease enter your name: BourbakiHello , Bourbakidhcp130:examples caravagn$

8

Capitolo 2

SimpleCAML

SimpleCAML è il frammento di linguaggio funzionale che utilizziamo per i nostri scopi. Tut-to quello che dobbiamo riuscire a fare può essere fatto usando solo questa porzione di linguag-gio; al dato pratico, SimpleCAML è il più piccolo nucleo della maggior parte dei linguaggidi programmazione funzionali. Come ogni linguaggio formale ne daremo sia la sintassi che lasemantica.

2.1 SintassiLa sintassi di SimpleCAML è definita in accordo alla seguente grammatica context-free.

Definition 4 (SimpleCAML) I programmi sintatticamente corretti di SimpleCAML sonodescritti da questa grammatica

EXP ::= n∣∣ fl

∣∣ true∣∣ false

∣∣ id∣∣ (EXP )∣∣ EXP op EXP∣∣ if EXP then EXP else EXP∣∣ fun id→ EXP∣∣ EXP EXP∣∣ let id = EXP in EXP∣∣ let rec id id = EXP in EXP

dove:n è un intero (0 1 2 -1 -2 . . . )fl è un reale (float) (0. 1.4 5e-6 . . . )id è un identificativo di variabile o funzione (x y f g sum fact . . . )op è un operatore (+, -, *, /, mod , +., -., *., /. &, or , not , >, <, =, >=, <=, . . . )

Nel seguito al posto di scrivere id useremo spesso x e f per rappresentare identificari di variabilie funzioni, rispettivamente. Inoltre assumeremo che → associ a destra, mentre l’applicazionefunzionale (EXP EXP ) associ a sinistra. Ad esempio,

(i) fun x→ fun y → x+ y

(ii) f x y

corrisponderanno a

(i) fun x→ ( fun y → x+ y)

(ii) (f x) y .

Un’occorrenza libera di una variabile è un’occorrenza non legata. Un’occorrenza legata di unavariabile x è un’occorrenza che si trova nel corpo di una funzione di cui x è un argomento, o nel

9

corpo di una definizione per x stessa. Ad esempio, se consideriamo

(iii) x+ ( fun y → 3 + y)

(iv) let x = 5 in x+ y

(v) x+ let x = 5 in x+ 2

in (iii) la variabile x è libera, mentre y è legata, mentre in (iv) la variabile x è legata e la y èlibera, infine in (v) la prima occorrenza di x è libera, mentre la seconda (quella dopo in ) è legata.Nel caso di definizioni ricorsive tipo

(vi) let rec f x = e1 in e2

le occorrenze di entrambi gli identificatori f ed x sia in e1 che in e2 sono considerate legate. D’orain poi considereremo come espressioni di SimpleCAML ben formate solo le espressioni che noncontengono variabili libere.

Example 5 Proviamo ad inserire alcuni degli esempi (i)− (vi) nell’interprete Ocaml.

# fun x -> fun y -> x + y;;- : int -> int -> int = <fun ># f x y;;Unbound value f# x + (fun y -> 3 + y);;Unbound value x# let x = 5 in x+1;;- : int = 6# x + let x =5 in x+1;;Unbound value x

Come atteso l’interprete non sa valutare la semantica di espressioni con variabili libere (unbound).

2.2 SemanticaNel definire la semantica di SimpleCAML useremo una nozione di sostituzione definita comesegue: data due espressioni e1, e2 e un identificatore x si definisce e1[x ← e2] come l’espressioneottenuta rimpiazzando sintaticamente in e1 ogni occorrenza libera di x con e2.

Definition 6 (Sostituzione) L’operazione di sostituzione si definisce formalmente come segue.

x[x← e] ≡ ey[x← e] ≡ y

n[x← e] ≡ n (analogo per fl, true, false)(e1 op e2)[x← e] ≡ e1[x← e] op e2[x← e]

( if e1 then e2 else e3)[x← e] ≡ if e1[x← e] then e2[x← e] else e3[x← e]

( fun x→ e1)[x← e] ≡ fun x→ e1

( fun y → e1)[x← e] ≡ fun y → e1[x← e]

( let x = e1 in e2)[x← e] ≡ let x = e1[x← e] in e2

( let y = e1 in e2)[x← e] ≡ let y = e1[x← e] in e2[x← e]

( let rec f x = e1 in e2)[x← e] ≡ let rec f x = e1 in e2

( let rec f x = e1 in e2)[f ← e] ≡ let rec f x = e1 in e2

( let rec f x = e1 in e2)[y ← e] ≡ let rec f x = e1[y ← e] in e2[y ← e] .

10

Scrivere ogni volta espressioni fun laddove sia chiaro che intendiamo una funzione è notevol-mente noioso, quindi in pratica vorremo poter abbreviare

let f = fun x→ e1 in e2

con la scritturalet f x = e1 in e2 .

A tal proposito introduciamo delle equivalenze (tipicamente chiamate zucchero sintattico proprioper denotarne la semplicità) che useremo nel seguito.

Definition 7 (Zucchero sintattico)

let f x = e1 in e2

≡let f = fun x→ e1 in e2

let f x1 x2 . . . xn = e1 in e2

≡let f = fun x1 → fun x2 → . . . fun xn → e1 in e2

let rec f x1 x2 . . . xn = e1 in e2

≡let rec f x1 = fun x2 → fun x3 → . . . fun xn → e1 in e2

Possiamo verificare le equivalenze usando l’interprete.

# let f = fun x-> x in f 3;;- : int = 3# let f x = x in f 3;;- : int = 3

Sino ad ora abbiamo usato l’interprete per valutare programmi SimpleCAML pur non conoscen-done la semantica. Adesso definiamo una semantica operazionale (big step - semantica naturale) diSimpleCAML. Nella definizione faremo uso di una nuova costante Rec che consentirà di descrivereil comportamento delle funzioni ricorsive. Inoltre, denoteremo con op l’operazione corrispondenteall’operatore descritto da op.

Definition 8 (Semantica di SimpleCAML) Le regole (Axm1) − (Axm5) rappresentano gliassiomi che definiscono la relazione di transizione ⇒.

(Axm1)n⇒ n

(Axm2)fl⇒ fl

(Axm3)true⇒ true

(Axm4)false⇒ false

(Axm5)fun x→ e⇒ fun x→ e

11

Le restanti regole ricorsive sono le seguenti.

(Par)e⇒ v

(e)⇒ v

(Op)e1 ⇒ v1 e2 ⇒ v2 v1 op v2 = v

e1 op e2 ⇒ v

(Not1)e⇒ true

not e⇒ false

(Not2)e⇒ false

not e⇒ true

(Cond1)e1 ⇒ true e2 ⇒ v

if e1 then e2 else e3 ⇒ v

(Cond2)e1 ⇒ false e3 ⇒ v

if e1 then e2 else e3 ⇒ v

(App)e1 ⇒ fun x→ e3 e2 ⇒ v2 e3[x← v2]⇒ v

e1e2 ⇒ v

(Let)e1 ⇒ v1 e2[x← v1]⇒ v

let x = e1 in e2 ⇒ v

(Rec)e1[f ← Rec ( fun f → e1)]⇒ v

Rec ( fun f → e1)⇒ v

(LetRec)e2[f ← Rec ( fun f → fun x→ e1)]⇒ v

let rec f x = e1 in e2 ⇒ v

Si noti che ( fun x→ e1)e2 è semanticamente equivalente a let x = e2 in e1 e possiamo dimostrarloesibendo le derivazione della semantica che abbiamo appena definito, infatti

fun x→ e1 ⇒ fun x→ e1 e2 ⇒ v2 e1[x← v2]⇒ v

( fun x→ e1)e2 ⇒ v

corrisponde ae2 ⇒ v2 e1[x← v2]⇒ v

let x = e2 in e1 ⇒ v

come richeisto. In pratica abbiamo quindi che# (fun x -> x * x) 5;;- : int = 25# let x = 5 in x * x;;- : int = 25

Si noti che, in questo caso, alla funzione non è nemmeno associato un nome, come è possibile peresempio nel λ-calcolo.

Alcuni esempi di derivazioni e uso dell’interprete

Example 9 Consideriamo(3 + 5) ∗ (2 + 8)

abbiamo la seguente derivazione

3⇒ 3 5⇒ 5

3 + 5⇒ 8

2⇒ 2 8⇒ 8

2 + 8⇒ 10(3 + 5) ∗ (2 + 8)⇒ 80

12

# (3+5)*(2+8);;- : int = 80

Example 10 Consideriamoif 3 < 5 then 3 else 5

abbiamo la seguente derivazione

3⇒ 3 5⇒ 5

3 < 5⇒ false5⇒ 5

if 3 < 5 then 3 else 5⇒ 5

# if 3 < 5 then 3 else 5;;- : int = 3

Example 11 Consideriamo( fun x→ x ∗ x)(5 + 2)

abbiamo la seguente derivazione

( fun x→ x ∗ x)⇒ ( fun x→ x ∗ x)5⇒ 5 2⇒ 2

5 + 2⇒ 7

7⇒ 7 7⇒ 7

7 ∗ 7⇒ 49(x ∗ x)[x← 7]⇒ 49

( fun x→ x ∗ x)(5 + 2)⇒ 49

# (fun x -> x * x) (5 + 2);;- : int = 49

Example 12 Consideriamo( fun x→ fun y → x+ y) 5 3

abbiamo la seguente derivazione

( fun x→ fun y → x+ y)⇒ ( fun x→ fun y → x+ y) 5⇒ 5

( fun x→ fun y → x+ y) 5⇒ ( fun y → x+ y)[x← 5]3⇒ 3

5⇒ 4 3⇒ 3

(5 + y)[y ← 3]⇒ 8

( fun x→ fun y → x+ y) 5 3⇒ 8

# (fun x -> fun y -> x + y) 5;;- : int -> int = <fun ># (fun x -> fun y -> x + y) 5 3;;- : int = 8

Example 13 Consideriamo

( fun f → fun x→ f(f(x)))( fun x→ x+ 1) 5

abbiamo la seguente derivazione (saltando qualche passaggio)

( fun f→ fun x→f(f(x)))⇒( fun f→ fun x→f(f(x))) ( fun x→x+1)⇒( fun x→x+1)( fun f→ fun x→f(f(x))) ( fun x→x+1)⇒( fun x→f(f(x)))[f←( fun x→x+1)]

( fun x→x+1)5⇒6( fun x→x+1)(( fun x→x+1)5)⇒7

( fun f → fun x→ f(f(x))) ( fun x→ x+ 1) 5⇒ 7

# (fun f -> fun x -> f(f(x))) (fun x -> x +1) 5;;- : int = 7

13

Example 14 Consideriamo

let rec fact x = if x = 0 then 1 else x ∗ fact(x− 1) in fact 2

ed introduciamo le seguenti abbreviazioni

e ≡ if x = 0 then 1 else x ∗ fact(x− 1)

R ≡ Rec( fun fact→ fun x→ e)

abbiamo la seguente derivazione

( fun x→e)[fact←R]⇒( fun x→e)[fact←R]Rec( fun fact→ fun x→e)⇒( fun x→e)[fact←R] 2⇒ 2 e[x← 2][fact← R]⇒ 2

(fact 2)[fact← R]⇒ 2

let rec fact x = e in fact 2⇒ 2

avendo che2⇒2 0→02=0⇒false

2⇒2( fun x→e)[fact←R]⇒( fun x→e)[fact←R] 2−1⇒1

R (2−1)⇒e[fact←R][x←1]

2∗fact(2−1)⇒2

e[x← 2][fact← R]⇒ 2

ovvero e[fact← R][x← 1]⇒ 1.

# let rec fact x = if x = 0 then 1 else x * fact (x-1) in fact 2;;- : int = 2

Example 15 Consideriamo

let rec foo x = foo(x− 1) + 6 in foo 2

ed introduciamo le seguenti abbreviazioni

e ≡ foo(x− 1) + 6

R ≡ Rec( fun foo→ fun x→ e)

abbiamo la seguente derivazione

( fun x→e)[foo←R]⇒( fun x→e)[foo←R]Rec( fun foo→ fun x→e)⇒( fun x→e)[foo←R] 2⇒ 2 ...

e[x←2][foo←R]⇒...

(foo 2)[foo← R]⇒ ...

let rec foo x = foo(x− 1) + 6 in foo 2⇒ ...

# let rec foo x = foo (x-1) + 6;;val foo : int -> int = <fun ># foo 9;;Stack overflow during evaluation (looping recursion ?).

Example 16 (Eager/Lazy evaluation) Si consideri queste due nuove regole operazionali per ilcondizionale

(Cond1)e1 ⇒ true e2 ⇒ v1 e3 ⇒ v2

if e1 then e2 else e3 ⇒ v1

(Cond2)e1 ⇒ false e3 ⇒ v1 e3 ⇒ v2

if e1 then e2 else e3 ⇒ v2

Riflettere sugli effetti di queste regole nel valutare la semantica di espressioni tipo la seguente

let rec foo x = foo(x− 1) + 6 in ( if x = x then x else foo x)

14

Capitolo 3

Da SimpleCAML a Ocaml

Per il momento abbiamo considerato un linguaggio funzionale denominato SimpleCAML i cuiunici tipi di dato sono interi, float, booleani e funzioni. Ovviamente il linguaggio ci serviva soloper poterne studiare la semantica e capire come sia fatta un linguaggio funzionale, nella sua piùsemplice accezione. In generale, i linguaggi moderni sono molto più complessi e offrono molte piùfeatures di quelle che abbiamo visto in SimpleCAML.

In questo capitolo si “introduce” un frammento del noto Ocaml che contiene, al suo interno, ilnostro SimpleCAML. Per lo scopo del nostro corso di questo linguaggio non studiamo la semantica,ma vediamo solamente alcune delle sue principali caratteristiche.

Tra le caratteristiche più potenti dei linguaggi ML-like come ad esempio Ocaml si contano lapossibilità di utilizzare un costrutto di pattern matching, la presenza dei costruttori di tipo, e lefunzioni di ordine superiore. Alcune di queste caratteristiche sono presenti anche in lingauggi diprogrammazione basati su altri paradigmi, (i.e. particolarmente in quello logico). Inoltre, alcuni diquesti costrutti sono “similmente” presenti in altri paradigmi quindi, ad esempio, considerando soloi tipi di dato di base il pattern matching è molto simile al costrutto switch-case del C. Vedremo,definendo tipi di dato strutturati, come questo costrutto diventi particolarmente comodo nelladefinizione di funzioni.

3.1 Pattern matching di baseIl pattern matching è utilizzato nel costrutto match, definito come segue:

match EXP withPAT → EXP

| PAT → EXP

...| PAT → EXP

dove PAT rappresenta un pattern ovvero un’espressione che può contenere costanti e variabili.L’intuizione è che il valore ottenuto dall’espressione dopo il match viene confrontato con i varipattern in sequenza. Quando uno dei pattern fa match con il valore, ovvero il valore è uguale alpattern a meno di sostituzioni di variabili con costanti, allora si valuta l’espressione associata alpattern e il risultato ottenuto diventerà il valore restituito dall’intero costrutto match.

Alla fine di questa sezione daremo una definizione più formale di un algoritmo di unficazionesu cui si basa il pattern matching. Per adesso consideriamo qualche esempio Ocaml di codice cheutilizza pattern matching; si consideri la successione di Fibonacci {Fn}IN+

F0 = 0 F1 = 1 Fn = Fn−1 + Fn−2 se n > 1.

descritta in SimpleCAML come segue:

15

# let rec fib i =match i with

0 -> 0| 1 -> 1| j -> fib (j-2) + fib (j-1);;

val fib : int -> int = <fun >

Si noti che le variabili usate nel pattern (e.g. nell’esempio, j) legano le occorrenze presenti nelleespressioni associate. Più pattern possono anche essere composti con l’operatore | e associati allastessa espressione:

# let rec fib i =match i with

( 0 | 1 ) -> i| j -> fib (j-2) + fib (j-1);;

val fib : int -> int = <fun >

Dal momento che è molto comune applicare il costrutto match all’argomento di una funzionesi considera il seguente zucchero sintattico, che utilizza la nuova keyword function:

let f x = match xwith p1 → e1 | . . . | pn → en

≡let f = function p1 → e1 | . . . | pn → en

let rec f x = match xwith p1 → e1 | . . . | pn → en

≡let rec f = function p1 → e1 | . . . | pn → en

da cui si ottiene una nuova definizione per Fibonacci:

# let rec fib = function0 -> 0

| 1 -> 1| i -> fib (i-2) + fib (i-1);;

val fib : int -> int = <fun >

Si noti che con questo nuovo costrutto non si utilizza più un nome per l’argomento della funzione,e ciò costringe a ri-suddividere i due casi di base della definizione di fib. Possibili rimedi a questo“problema” sono i seguenti:

# let rec fib = function( 0 | 1 ) as i -> i

| i -> fib (i-2) + fib (i-1);;val fib : int -> int = <fun >

oppure

# let rec fib = functioni when (i < 2) -> i

| i -> fib (i-2) + fib (i-1);;val fib : int -> int = <fun >

Capita spesso di voler definire un caso “di default” in un costruttomatch da considerare quandotutti gli altri casi definiti non sono soddisfatti. Tale caso può essere descritto dal pattern _, adesempio, la seguente funzione verifica se l’argomento è uguale a zero:

# let iszero = function0 -> true

| _ -> false ;;val iszero : int -> bool = <fun >

In realtà il pattern _ è solo una notazione usata comunemente ma che potrebbe essere rimpiazzatada una variabile:

16

# let iszero = function0 -> true

| x -> false ;;val iszero : int -> bool = <fun >

Negli esempi che abbiamo visto il pattern matching è sempre stato esaustivo, ovvero non c’eranopossibili valori per l’espressione a cui il pattern matching era applicato che non fossero compresiin uno dei pattern considerati. Il pattern matching può non essere esaustivo, ad esempio:# let is_odd i =

match (i mod 2) with0 -> false

| 1 -> true;;

Questa funzione funziona perfettamente in quanto sappiamo che i mod 2 valuterà sempre a 1 o a2. Il compilatore non è però in grado di fare questo ragionamento, per cui segnalerà un warningdi questo tipo:Warning: this pattern -matching is not exhaustive.Here is an example of a value that is not matched:2

In modo simile il compilatore controlla se ci siano dei casi ridondanti e quindi inutilizzati, comenel seguente esempio:# let f i =

match i withtrue -> 1

| false -> 2| _ -> 3;;

Anche in questo caso il compilatore segnalerà un warning di questo tipo:Warning: this match case is unused.

| _ -> 3;;

Per concludere, si noti che in realtà il pattern matching in ocaml è ovunque vi sia la possibilitàdi legare variabili. Anche i costrutti let e fun sono in realtà definiti come segue:

let PAT = EXP

let f PAT . . . PAT = EXP

fun PAT → EXP

L’ unificazione. Il patter matching, così come l’inferenza di tipi si basano sull’unificazione,ovvero il processo di trovare una sostituzione che rende due termini equivalenti (si noti che poichési parla di sostituzione si intende equivalenza sintattica).

Vediamo un semplice esempio; siano dati due termini

t1 = f x (g y) t2 = f (g z) w

una sostituzione [x← g z, w ← g y] sarebbe una unificazione poiché

t1 =f x (g y) [x← g z, w ← g y]

= f (g z) w [x← g z, w ← g y]

= f (g z) (g y) = t2 .

In generale, dati due termini una unificazione potrebbe non esistere; ad esempio a questi duetermini

t1 = f x t2 = x

non si può associare alcuna sostituzione che li renda equivalenti. Inoltre non è detto che, seesiste, esista una sola possibile unificazione per un insieme di termini. Comunque sia, se esiste ununificatore, allora esiste un unificatore più generale unico rispetto alla ridenominazione, ovvero chesi riduce agli altri usando ulteriori sostituzioni.

17

3.2 Tipi di dato strutturatiQuasi tutti i linguaggi di programmazione definiscono dei tipi primitvi e dei costruttori di tipo. Aseconda dal paradigma su cui si basa il linguaggio i costruttori di tipo sono differenti e, a secondadel contesto d’uso del linguaggio, i tipi primitiv cambiano. Tuttavia, la maggior parte dei lingauggidi programmazione forniscono come tipi primitivi i numeri naturali, i numeri reali ed i caratteri.Le stringhe, ad esempio in C, si ottengono in modo implicito o esplicito dai caratteri. Nel seguitovediamo alcuni tipi di dato strutturati molto utilizzati in Ocaml.

3.2.1 TupleUna tupla è una collezione di valori di tipo arbitrario. La sintassi di una tupla è una sequenza divalori separati da virgole. Ad esempio:

let p = (1, “Ciao”)

definisce una tupla p composta dall’intero 1 e dalla stringa “Ciao”.

# let p = (1, "Ciao");;val p : int * string = (1, "Ciao")

In questo esempio le parentesi non sono necessarie e si otterrebbe lo stesso risultato con

# let p = 1, "Ciao";;val p : int * string = (1, "Ciao")

Ovviamente una tupla può essere composta da più di due elementi:

let q = 1, 1.5, “Ciao”, 18

Quindi abbiamo, ad esempio

# let p =(1,2,3,4,5);;val p : int * int * int * int * int = (1, 2, 3, 4, 5)

Le tuple possono essere decomposte usando il pattern matching. Ad esempio, la funzione

let fst(x,_) = x

restituisce il primo elemento di una tupla di due elementi (i.e. una coppia), mentre

let snd(_, x) = x

restituisce il secondo.

# fst (1 ,2);;- : int = 1# snd (1 ,2);;- : int = 2

In realtà fst e snd sono funzioni built-in del linguaggio, quindi sono sempre utilizzabili anchesenza averle definite precedentemente.

# fst;;- : ’a * ’b -> ’a = <fun ># snd;;- : ’a * ’b -> ’b = <fun >

Il tipo di una tupla è il prodotto cartesiano dei tipi degli elementi che la costituiscono. Adesempio, la tupla 1, 1.3 ha tipo int * float. Le tuple giocano un ruolo importante nella defi-nizione delle funzioni, più precisamente nella definizione dell’applicazione parziale delle funzioni,come vedremo più avanti in questo capitolo.

18

3.2.2 ListeUna lista è una sequenza di valori x1, x2, . . . , xn con n ≥ 0 e denotata

[x1; x2; . . .; xn]

tali che ∀i ∈ {1, . . . , n}. xi ` τ , ovvero tutti gli elementi hanno lo stesso tipo. L’espressione [ ]rappresenta una lista vuota;

# [];;- : ’a list = []

ed esistono funzioni predefinite per manipolare liste. Ad esempio l’espressione x::xs, dove :: èchiamato cons, rappresenta l’aggiunta in testa alla lista rappresentata da xs del valore rappresen-tato da x. Si noti che :: associa a destra;

# 3::[2;3;4];;- : int list = [3; 2; 3; 4]

Differentemente, l’espressione x@y rappresenta la concatenazione delle liste rappresentate da x edy. Si noti che non ci sono ipotesi sulle due liste se non che la lista ottenuta come unione sia bentipata, dunque le due liste abbiano elementi dello stesso tipo

# [1;2;3;4;]@[5;6;7];;- : int list = [1; 2; 3; 4; 5; 6; 7]# [1;2;3;4;]@[true ];;This expression has type bool but is here used with type int

Le liste posso essere decomposte usando il pattern matching, vediamo adesso due sempliciesempi di funzioni definite su liste.

Example 17 Definiamo, data una lista l, una funzione len tale che

len(l) = n⇔ l = [x1; x2; . . .; xn] .

L’implementazione, che non può esser altro che lineare, è la seguente

# let rec len = function[] -> 0

| x::xs -> 1 + len xs;;val len : ’a list -> int = <fun ># len ([1;2;3;4;]@[5;6;7]);;- : int = 7

e corrisponde alla seguente visione matematica della funzione stessa

len(l) =

{0, se l = []1 + len(xs), se l = x::xs .

Si noti che il costrutto x::xs è usato in un pattern la cui interpretazione è la seguente: x rappre-senta il primo elemento della lista, mentre xs rappresenta il resto della lista. Inoltre, si noti chel’uso delle parentesi nell’esempio è dovuto all’associatività a sinistra dell’applicazione funzionale.

Example 18 Definiamo, data una lista l =[x1; x2; . . .; xn], una funzione sum tale che

sum(l) =

n∑i=1

xi .

Anche in questo caso la soluzione possibile è ovvia dato che la sommatoria si spezza in un modoche rende immediatamente riconoscibile la “ricorsione”

sum(l) =

n∑i=1

xi = x1 +

n∑i=2

xi .

Da cui abbiamo la seguente definizione

19

# let rec sum = function[] -> 0

| n::l -> n + sum l;;val sum : int list -> int = <fun >

# sum ([1;2;3;4;]@[5;6;7]);;- : int = 28

3.2.3 UnionsUna union rappresenta l’unione disgiunta di diversi tipi di dato, ottenuta associando un’etichettaad ogni tipo di dato considerato. Una union è definita con il seguente costrutto di definizione ditipi:

type typename =

Id of tipo| Id of tipo...| Id of tipo

Dove Id è un identificatore detto costruttore di tipo che rappresenta un’etichetta e che deveiniziare con una lettera maiuscola, mentre tipo è un qualunque tipo di dato di ocaml, ad esempio:int, float, int*float (i.e. il prodotto cartesiano IN×R, ovvero le coppie costituite da un interoe un float), int->float (una funzione), int list (una lista di interi), ecc. . . . Si noti che è anchepossibile unire tipi vuoti omettendo la parte of tipo associata ad un costruttore.

Un esempio di union in cui si definisce un nuovo tipo number che accomuna int e float e unvalore canonico che rappresenta lo zero è il seguente

# type number =Zero

| Integer of int| Real of float;;

type number = Zero | Integer of int | Real of float

I valori di una unione si ottengono applicando il costruttore ad un valore del tipo ad essoassociato, se non omesso. Ad esempio:

# let zero = Zero;;val zero : number = Zero# let i = Integer 1;;val i : number = Integer 1# let x = Real 3.2;;val x : number = Real 3.2

I costruttori possono essere usati anche nel pattern matching.

Example 19 La funzione seguente, ad esempio, somma due valori di tipo number.

# let add n1 n2 =match n1,n2 with(Zero ,n | n,Zero) -> n

| Integer i1 , Integer i2 -> Integer (i1 +i2)| (Integer i,Real x | Real x,Integer i) -> Real (x +. (float_of_int i))| Real x1,Real x2 -> Real (x1 +. x2);;val add : number -> number -> number = <fun >

Si noti che per fare pattern matching contemporaneamente di n1 ed n2 si è costruita la coppian1, n2. Inoltre, si noti che per effettuare la somma tra un naturale ed un reale si usano gli operatoripiù generali, ovvero quelli dei reali (perchè?); quindi ad esempio si usa la somma tra float, denotatadall’operatore +., e per poterla applicare correttamente dal punto di vista dei tipi si converte ilparametro intero nell’equivalente valore float mediante una funzione predefinita float_of_int.

20

# add i i;;- : number = Integer 2# add x x;;- : number = Real 6.4# add x i;;- : number = Real 4.2# add i x;;- : number = Real 4.2

Le definizioni di tipo possono essere ricorsive, ovvero all’interno della definizione di un tipo τè possibile menzionare il tipo τ stesso. Tra le strutture dati maggiormente utilizzate ne esistonomolte definibili per ricorsione: alberi, liste, dizionari solo per citarne alcune.

Example 20 La seguente definizione consente di descrivere alberi binari con informazioni nume-riche nelle foglie, e fa uso della ricorsione.

# type int_tree =Leaf of int

| Node of int_tree*int_tree ;;type int_tree = Leaf of int | Node of int_tree * int_tree

Un esempio di albero di questo tipo è il seguente:

# let t = Node ( Leaf 3 , Node (Leaf 4, Leaf 5));;val t : int_tree = Node (Leaf 3, Node (Leaf 4, Leaf 5))

Una funzione che calcola la somma dei valori in un albero di questo tipo è la seguente:

# let rec sumtree = functionLeaf n -> n

| Node (t1,t2)-> sumtree t1 + sumtree t2;;val sumtree : int_tree -> int = <fun ># sumtree t;;- : int = 12

Si noti la naturalezza con la quale si possono definire funzioni ricorsive su tipi ricorsivi.

Si noti infine, che tramite il costrutto type è anche possibile definire sinonimi. Ad esempio:

# type ide = string ;;type ide = string ;;

definisce un tipo ide sinonimo del tipo string.

3.3 FunzioniIn Ocaml si possono costrutire funzioni complesse partendo da funzioni semplici. Si consideri unafunzione square(x) = x2

# let square = fun x -> x * x;;val square : int -> int = <fun >

Il suo tipo int -> int è inferito automaticamente dal compilatore usando il sistema di tipidi Ocaml; il sistema non necessita di altre informazioni ed il simbolo <fun> denota che, in unsistema a tempo/memoria finita, non vi è rappresentazione migliore di questa per una funzioneche ha dominio infinito. In teoria, l’insieme {(x, x2) | x ∈ IN} sarebbe una denotazione estensio-nale migliore per questa funzione, tuttavia il compilatore non la sa inferire automaticamente. Inparticolare, consideriamo una nuova definizione della stessa funzione

# let square ’ x = (x+1) * (x-1) + 1;;val square ’ : int -> int = <fun >

21

Pur valendo l’equivalenza

∀x ∈ IN. square(x) = square’(x)

tale uguaglianza tra funzioni non si può testare essendo l’equivalenza estenzionale tra funzioni noncalcolabile, infatti l’interprete risponde come segue.

# square = square ’;;Exception: Invalid_argument "equal: functional value".

In Ocaml si possono definire funzioni infisse come segue.

# let ( -! ) n m = if n<m then 0 else n-m;;val ( -! ) : int -> int -> int = <fun ># 5 -! 3;;

- : int = 2# 3 -! 5;;

- : int = 0

Qui abbiamo definito un semplice operatore binario −! che sottrae un intero m da un intero n erestituisce 0 se n < m.

Consideriamo ora le procedure ricorsive che possiamo definire in Ocaml, analizziamo la fun-zione definita come segue

# let rec f x = if x=0 then 1 else f x;;val f : int -> int = <fun ># f 2;;^C Interrupted. (* provate ad aspettare ... *)

La funzione non termina se valutata su certi argomenti, ed ovviamente non fornisce nemmenoun errore a runtime. Definiamo adesso la funzione

# (fun x -> 1) (f 2);;^C Interrupted.

Teoricamente la funzione fun x -> 1 valuta sempre ad 1, quindi termina sempre. Oltretuttola funzione non dipende dal valore del suo parametro, eppure se il parametro non ha valutazioneche termina, tutto non termina. Questo deriva dal fatto che SimpleCAML, o Ocaml in generale,dipendono da ML il quale implementa una strategia di valutazione nell’applicazione funzionaledenominata call-by-value (o eager). Tale strategia dice che l’argomento di una funzione sarà semprevalutato, anche se non utilizzato nel corpo della funzione. A tal proposito, guardate la regola disemantica operazionale (App) usata in SimpleCAML.

La tail-recursion. Esistono molti modi di fare ricorsione su un dominio ben fondato. Ad esempiofacendo mutua ricorsione tra più variabili

f(n) = φf (g(n− 1)) g(n) = φg(f(n− 1))

oppure, ad esempio, facendo una doppia ricorsione

f(n) = φf (g(n− 1)) + φf (g(n− 2)) .

Nella maggior parte dei casi le funzioni ricorsive sono costose da essere eseguite perché, per laloro valutazione, lo stack cresce ad ogni chiamata ricorsiva. A seconda del numero di chiamatericorsive lo stack può crescere esponenzialmente, portando la memoria dell’interprete ad esaurisi1.Esistono tuttavia alcuni tipi di ricorsione che non presentano questo tipo di problema, si consideriad esempio

f(n) = φf (f(n− 1)) .

1Si assume che abbiate idea di cosa significhi, operazionalmente parlando, eseguire una funzione in un runtimebasato su stack. Intuitivamente, ad ogni chiamata di funzione si crea un frame nuovo per la valutazione del corpodelal funzione.

22

Questo tipo di ricorsione, denominata tail-recursion, è tale per cui la crescita dello stack può esserelimitata ad un singolo frame. Questo perchè la chiamata ricorsiva alla funzione restituisce un valoreche il chiamante restituisce a sua volta e, din conseguenza, la valutazione della chiamata ricorsivasi può fare opportunamente nello stack usato per il chiamante.

Example 21 Consideriamo la seguente definizione della successione di Fibonacci {Fn}IN+

F0 = 0 F1 = 1 Fn = Fn−1 + Fn−2 se n > 1.

Una sua possibile implementazione naive sarebbe

# let rec fib_rec n =if n < 2 then nelse

fib_rec (n - 1) + fib_rec (n - 2);;val fib_rec : int -> int = <fun >

Pur non essendo la performance il centro delle nostre discussioni è facile notare che questa imple-mentazione non è particolarmente soddisfacente dato che la funzione si richiama ricorsivamentedue volte sommando i risultati quindi, in generale, non è tail-recursive. Infatti abbiamo che

# fib_rec 3;;- : int = 2# fib_rec 10;;- : int = 55# fib 45;;..... (* interrotto dopo circa 10 secondi *)

Una possibile definizione più astuta è la seguente

# let fib n =let rec fib_aux n a b =

match n with| 0 -> a| _ -> fib_aux (n-1) (a+b) a

in fib_aux n 0 1;;val fib : int -> int = <fun >

Notate che questa definizione si ottiene con una funzione definita nel let interno la quale usa non1 ma 2 parametri ed è tail-recursive.

# fib 3;;- : int = 2# fib 10;;- : int = 55# fib 45;;- : int = -1012580478 (* overflow! *)

In questo caso abbiamo un overflow perché la memoria del calcolatore è finita. In particolare, suuna macchina a 32 bit dove la rappresentazione del numero in binario mantiene il segno del numeroesplicito, gli interi variano nell’intervallo

[−230, 230 − 1] = [−1073741824; 1073741823].

Compilando e monitorando le performance delle due definizioni abbiamo

dhcp130:examples caravagn$ time ocamlrun fib_rec 3614930352real 0m2.611s, user 0m2.596s, sys 0m0.011sdhcp130:examples caravagn$ time ocamlrun fib 3614930352real 0m0.032s, user 0m0.023s, sys 0m0.009s

23

Example 22 In maniera simile all’esempio precedente si possono fare le stesse considerazionisulle due seguenti implementazioni del fattoriale?

# let rec factorial n =if n <= 0 then 1else n * factorial (n-1);;

val factorial : int -> int = <fun ># let factorial n =

let rec loop i accum =if i > n then accumelse loop (i + 1) (accum * i)

in loop 1 1;;val factorial : int -> int = <fun >

Example 23 Si consideri la Funzione di Ackermann A(m,n) tale che

A(m,n) =

n+ 1 se m = 0

A(m− 1, 1) se m > 0 e n = 0

A(m− 1, A(m,n− 1)) se m > 0 e n > 0.

Questa funzione è molto importante in calcolabilità poiché rappresenta un esempio di funzionericorsiva che non è primitiva ricorsiva. Notate che questa funzione cresce in maniera estremamenteveloce quindi, ad esempio, calcolare A(4, 3) su computer tradizionali potrebbe essere arduo.

A(m,n) n = 0 n = 1 n = 2 n = 3 n = 4 n = 5m = 0 1 2 3 4 5 6m = 1 2 3 4 5 6 7m = 2 3 5 7 9 11 13m = 3 5 13 29 61 125 253

m = 4 13 65533 265536 − 3 2265536 − 3 A(3, 22

65536 − 3) A(3, A(4, 4))m = 5 65533 A(4, 65533) A(4, A(4, 65533)) A(4, A(5, 2)) A(4, A(5, 3)) A(4, A(5, 4)). . . . . . . . . . . . . . . . . . . . .

Una sua possibile definizione, estendendola a A(m,n) = 0 se m < 0 o n < 0, è

# let rec ackermann = function| m,n when m < 0 || n < 0 -> 0| 0,n -> n+1| m,0 -> ackermann (m-1,1)| m,n -> ackermann (m-1,ackermann (m,n -1));;

val ackermann : int * int -> int = <fun ># ackermann (0 ,0);;- : int = 1# ackermann (1 ,1);;- : int = 3# ackermann (2 ,13);;- : int = 29# ackermann (3 ,1);;- : int = 13# ackermann (3 ,7);;- : int = 1021# ackermann (3 ,9);;- : int = 4093

3.3.1 PolimorfismoConsideriamo la funzione identià

f(x) = x

24

# let f = fun x -> x;;val f : ’a -> ’a = <fun >

Questa funzione viene tipata ’a -> ’a, ovvero viene usato un quantificatore del tipo

∀τ. f ` τ → τ

per denotare che la funzione è polimorfa e che quindi può essere applicata ad argomenti di unqualunque tipo.

# id 3;;- : int = 3# id "pippo";;- : string = "pippo"# id (fun x -> x+1);;- : int -> int = <fun >

Il polimorfismo è una delle caratteristiche principali dei linguaggi funzionali e permette, in generale,di definire facilmente funzioni e la loro composizione.

Example 24 Definiamo una funzione comp che prende in input due funzioni f e g e ne costruiscela funzione composta. Per poterle comporre deve valere che il codominio di g deve coincidere conil dominio di f

# let comp f g = fun x -> f (g x);;val comp : (’a -> ’b) -> (’c -> ’a) -> ’c -> ’b = <fun >

Infatti quello che ci dice l’interprete è proprio questo, il tipo di g è ’c -> ’a, quello di f è ’a ->’b, da cui il tipo delle composizione f ◦ g è ’c -> ’b.

3.3.2 Curry, uncurry e valutazione parzialeIl currying funzionale, dal logico Haskell Curry (e da Frege inizialmente), permette di studiarefunzioni di molte variabili in linguaggi formali che prevedono solamente funzioni di una variabile(e.g. il λ-calcolo). In generale il currying significa stabilire una opportuna equivalenza tra i dominidelle funzioni

A×B → C ≈ A→ B → C

così che una funzione f : A×B → C possa essere scritta come una funzione

g : A→ B → C .

Ovviamente le due funzioni devon essere equivalenti, ovvero

∀x ∈ A, y ∈ B. f(x, y) = g x y .

Le procedure che permette di ottenere g da f e viceversa si chiama appunto currying/uncurryinge, in λ-calcolo, queste due funzioni sono definibili come segue:

curry = λf.λx.f(x, y)

uncurry = λf.λx.f fst(x) snd(y) .

Example 25 Le funzioni curry/uncurry si possono definire in Ocaml come segue

# let curry f = fun x y -> f (x,y);;val curry : (’a * ’b -> ’c) -> ’a -> ’b -> ’c = <fun ># let uncurry f = fun (x,y) -> f x y;;val uncurry : (’a -> ’b -> ’c) -> ’a * ’b -> ’c = <fun >

Da cui otteniamo

25

# let addpair (x,y) = x+y;;val addpair : int * int -> int = <fun ># let add = curry addpair ;;val add : int -> int -> int = <fun ># add 3 5;;- : int = 8# let addpair = uncurry (+);;val addpair : int * int -> int = <fun ># addpair (3 ,5);;

- : int = 8

L’ applicazione parziale consiste nel definire una funzione di n argomenti come una funzionedella sua applicazione ad n − 1 argomenti piu un argomento fissato. Questo in pratica permettedi trasformare una funzione che prende un tupla di argomenti in una catena di di funzioni cheprendono un singolo argomento. L’applicazione parziale è un concetto legato al currying.

Example 26 Consideriamo ad esempio due funzioni sum ed incr tali che

sum : IN× IN→ IN incr : IN→ IN

con l’ovvio significato

sum(x, y) = x+ y incr(x) = x+ 1 .

Supponiamo di fissare il primo dei due argomenti della funzione sum al valore 1, allora abbiamoche

sum(1, y) ≈ sum 1 y = 1 + y = incr(y) .

Questo vale perchèIN× IN→ IN ≈ IN→ IN→ IN

In Ocaml possiamo osservare il suguente output del typechecker:

# let sum x y = x + y;;val sum : int -> int -> int = <fun ># let sum x y = x + y in sum 1;;- : int -> int = <fun >

3.3.3 Higher-orderRiprendiamo l’esempio sul currying, la relazione che avevamo richiesto alle due funzioni f e g era

∀x ∈ A, y ∈ B. f(x, y) = g x y .

Se guardiamo il lato sinistro dell’equazione abbiamo g x y, se consideriamo solo la prima delle dueapplicazioni funzioni abbiamo

g x : B → C

ovvero una funzione g che, una volta fissato un suo argomento x, è ancora una funzione. In pratica,questo comportamento denota una funzione di ordine superiore, ovvero una funzione che, dettorozzamente, nel suo tipo contiene un tipo funzione. Queste tipi di funzioni sono estremamentecomode perché permettono, ed esempio, di passare le funzioni direttamente come parametro adaltre funzioni. Inoltre, l’ordine superiore non è limitato superiormente, quindi si possono definirefunzioni completamente arbitrarie. Nella maggior parte dei linguaggi di programmazione nonfunzionali l’ordine superiore non è presente, a meno di utilizzare trucchi poco eleganti come, adesempio i puntatori a funzioni in C. Di seguito vengono definiti alcuni esempi di note funzioni diordine superiore.

26

Example 27 Supponiamo di avere a disposizione una funzione f ed una lista l tali che

f : A→ B l = [x1;x2;x3; . . . ;xn] .

Condizione sui tipi dell’applicabilità di questa funzione è che

∀i ∈ {1, . . . , n}. xi : A .

Quello che vogliamo automatizzare è l’applicazione della funzione f agli elementi della lista lottenendo il seguente risultato

l′ = [f(x1); f(x2); f(x3); . . . ; f(xn)]

con l′ lista di elementi di tipo B (i.e. ∀i ∈ {1, . . . , n}. f(xi) : B). Tale funzione è di base presentein SimpleCAML ma la si puo definire cosi:

# let rec map f l =match l with| [] -> [];| x::xs -> f x :: map f xs;;

- : map : (’a -> ’b) -> ’a list -> ’b list = <fun >

Cosi facendo abbiamo che, ad esempio

# let f x = x+1 in map f [1; 2; 3];;- : int list = [2; 3; 4]

L’applicazione parziale sulla funzione map diventa ad esempio:

# let f x = x+1 in map f;;val map : (’a -> ’b) -> ’a list -> ’b list = <fun >

Example 28 Supponiamo di avere a disposizione i seguenti oggetti: una funzione f , un valore“speciale” a e una lista l di n elementi. Vogliamo definire il risultato dell’applicazione composizio-nale di f agli elementi della lista, in altre parole vogliamo definire le seguenti quantita

fr = f(x1, f(x2, f(. . . f(xn−1, f(xn, a)) . . .)))

fl = f(f(. . . f(. . . f(f(a, x1), x2) . . .), xn−1), xn) .

che denotano la chiusura, rispetto agli elementi della lista l, dell’applicazione della funzione f adestra (fr) e sinistra (fl). Tali valori sono definibili usando due funzioni foldr e foldl che inSimpleCAML si possono definire cosi:

# let rec foldr f a l = match l with| [] -> a| x :: xs -> f x (foldr f a xs);;

val fold_right : (’a -> ’b -> ’b) -> ’b -> ’a list -> ’b = <fun ># let rec foldl f a l = match l with

| [] -> a| x :: xs -> foldl f (f a x) xs;;

val fold_left : (’a -> ’b -> ’a) -> ’a -> ’b list -> ’a = <fun >

Ovviamente, se la funzione f è associativa e commutativa allora usare le due funzioni dà lo stessorisultato. Vale anche che, essendo funzioni polimorfe, data una qualungue funzione g definita come

g [ ] = v

g (x :: xs) = f x (g xs)

allora g è definibile usando la foldr. Dimostriamo che, per ogni lista l, vale che

g l = foldr f v l .

27

Lo possiamo dimostrare per induzione sulla struttura della lista l: se l = [ ] allora vale

g [ ]def= v

def= foldr f v [ ]

mentre, se l = x :: xs, dobbiamo verifcare se g x :: xs?= foldr f v x :: xs. Per ipotesi su g

sappiamo cheg (x :: xs)

def= f x (g xs)

mentre per definizione di foldr sappiamo che

foldrf v (x :: xs)def= f v (foldrf v xs)

ed il teorema segue per l’ipotesi induttiva su xs

g xs = foldr f v xs .

3.4 EccezioniQuanto vale n! se n < 0? In realtà noi ci preoccupiamo di definire n! per n ≥ 0, anche perchéassumiamo n! = 0 se n < 0, e questo modo di ragionare funziona fintanto che le formule nondevono essere implementate. Diversamente, se dobbiamo fornire un’implementazione delle nostrefunzioni in un qualunque linguaggio, dobbiamo presumibilmente definire funzioni che gestisconoun intero set di possibili valori di input, anche perchè non possiamo sapere quale utilizzo verràfatto delle funzioni che scriviamo. In tal caso, è più conveniente pensare al fattoriale come unafunzione definita come segue

n! =

⊥, se n < 0

0, se n = 0

n · (n− 1)!, se n > 0

dove il valore ⊥ denota un valore speciale. Si noti che non stiamo dicendo ⊥= 0, ma piuttostousiamo un valore speciale per denotare un evento “eccezionale”, il calcolo di un fattoriale negativo.In generale, individuare questi tipi di eventi eccezionali è importante tanto quanto individuare icasi generali di definizione di un algoritmo. I linguaggi di programmazione moderni definisconoquesti comportamenti tramite le eccezioni. Tali eventi, la cui formalizzazione è molto “imperativa”,sono presenti anche in Ocaml; notate che nel frammento SimpleCAML che noi consideriamo nonvi sono eccezioni tuttavia, per comodità, le useremo nei prossimi capitoli. Le eccezioni si dichiaranousando una keyword exception ed un nome che le identifica

exception NomeEccezione

ed in generale sono lanciate come segue

raise NomeEccezione .

Example 29 Ad esempio consideriamo la seguente funzione sub : IN→ IN+ ∪ {⊥}

sub m n! =

{⊥, se m < n

m− n, altrimenti .

In Ocaml possiamo definire l’eccezione come segue# exception NegativeNumber ;;

exception NegativeNumber

e poi utilizzarla nella definizione della funzione# let sub x y = if x<y then raise NegativeNumber else x-y;;val sub : int -> int -> int = <fun ># sub 4 3;;- : int = 1# sub 3 4;;Exception: NegativeNumber.

28

Esercizi. Segue una serie di esercizi che richiedono, per essere risolti, alcune o tutte le caratte-ristiche di SimpleCAML/Ocaml che abbiamo discusso.

1. Si definisca una funzione h che associ la funzione f(x)x ad ogni f(x).

# let h = ( fun f -> ( fun x -> f(x)/.x ));;val h : (float -> float) -> float -> float = <fun >

Ad esempio, se x→ 0 allora sin(x)/x→ 1

# (h (sin ))(0.1);;- : float = 0.998334166468

2. Si definiscano due funzioni mutuamente ricorsive odd e even che verifichino se un numero siapari o dispari.

# let rec even n = if n = 0 then true else odd (n-1)and odd n = if n = 0 then false else even (n-1);;val even : int -> bool = <fun >val odd : int -> bool = <fun >

Verificare che le funzioni siano definite correttamente.

# even 4 & even 6;;- : bool = true# odd 4 || odd 5;;- : bool = true

3. Definire una funzione di ordine superiore predl che data una lista l ed un predicato booleanop restituisca la lista dei risultati della valutaizone di p sugli elementi di l. Successivamente,definire l’operatore di & su liste come segue

lAnd p [x1; . . . ;xk] = p(x1)& . . .&p(xk)

facendo uso della funzione predl.

# let predl p l = map p l;;val predl : (’a -> ’b) -> ’a list -> ’b list = <fun >

Da cui

# let iszero x = match x with| 0 -> true| _ -> false ;;

val iszero : int -> bool = <fun ># predl iszero [0;1;2];;- : bool list = [true; false; false]

E poi si possono usare funzioni note, ad esempio

# let lAnd p l = foldr (&) true (predl p l);;val lAnd : (’a -> bool) -> ’a list -> bool = <fun >

e possiamo quindi ottenere

# lAnd iszero [0;1;2];;- : bool = false# lAnd iszero [0;0;0];;- : bool = true

29

4. Definire una funzione filter che data una lista l ed un predicato p restituisca la lista deglielementi in l che soddisfano p;

filter p l = [x1; . . . ;xk] ∀i ∈ {1, . . . , k}.p(xi) k ≤ n

Definire ora la funzione filter usando la foldr.

let filter p = foldr (fun x acc -> if p x then x::acc else acc) [];;val filter : (’a -> bool) -> ’a list -> ’a list = <fun >

5. Definire una funzione ricorsiva check tale che, aplpicata ad una lista l ed un predicato p,la funzione restituisca true se e solo se p vale sull’ultimo elemento di l. Se l è vuota checkrestituisce false.

# let rec check p l =match l with| [] -> false| [x] -> p x| x::y::xs -> check p (y::xs);;

val check : (’a -> bool) -> ’a list -> bool = <fun ># check iszero [0;1;2;0];;- : bool = true

6. Date le definizoni di foldr e foldl riflettere sulle relazioni che devono esistere tra il tipodegli degli elementi della lista, il dominio di f ed a;

7. Calcolare la lunghezza di una lista usando foldr o foldl;

# let len = foldl (fun x lst -> x+1) 0;;val len : ’_a list -> int = <fun >

8. Rovesciare l’ordina degli elementi che appaiono in una lista utilizzando foldl ;

# let rev = foldl (fun lst x -> x::lst) [];;val rev : ’_a list -> ’_a list = <fun ># rev [1;2;3];;- : int list = [3; 2; 1]

9. Sommare e moltiplicare gli elementi di una lista usando foldr o foldl;

# let sum = foldl (fun acc x -> acc + x) 0;;val sum : int list -> int = <fun ># let prod = foldl (fun acc x -> acc * x) 1;;val prod : int list -> int = <fun ># sum [1;2;3;4];;- : int = 10# prod [1;2;3;4];;- : int = 24

10. Calcolare il valore del massimo/minimo elemento contenuto in una lista dove per ipotesi ivalori contenuto della lista sono maggiori di 0 e minori di 99;

# let max = foldl (fun x y -> if x>y then x else y) 0;;val max : int list -> int = <fun ># let min = foldl (fun x y -> if x<y then x else y) 99;;val min : int list -> int = <fun ># max [1;2;1];;- : int = 2# min [3;4];;- : int = 3

30

11. Partizionare una lista l in due liste l1 ed l2 tali che l1 contenga gli elementi che soddisfanoun predicato p (passato come parametro), e l2 gli elementi che non lo soddisfano;

# let partition p = foldr (fun x (tlst ,flst)->if p x then (x::tlst ,flst) else (tlst ,x::flst))

([] ,[]);;val partition : (’a -> bool) -> ’a list -> ’a list * ’a list = <fun >

# partition iszero [1;2;0;3;0];;- : int list * int list = ([0; 0], [1; 2; 3])# partition odd [1;2;3;4;5];;- : int list * int list = ([1; 3; 5], [2; 4])

12. Concatenare una lista di liste (i.e. una matrice) in un’unica lista (i.e. un vettore);

# let concat = foldr ( @ ) [];;val concat : ’_a list list -> ’_a list = <fun >

13. Definire una funzione che, data una lista l ed un valore k ∈ IN, restituisca l’elemento k-esimodi l;

# exception Erroraccio ;;exception Erroraccio# let rec nth n lst = match n,lst with

| _,[] -> raise Erroraccio| 1, (x :: xs)-> x| k, (x :: xs)-> nth (n-1) xs;;

val nth : int -> ’a list -> ’a = <fun ># nth 23 [1];;Exception: Erroraccio.

14. Definire una funzione che data una lista l restituisca l’ultimo l’elemento di l, cercare di usarela funzione nth;

# let last lst = let lastind = len lst in nth lastind lst;;val last : ’_a list -> ’_a = <fun >

15. Definire una funzione che calcoli xi, per un generico x ed i, e chiamarla power.

# let rec power i x =if i = 0 then 1.0else x *. (power (i - 1) x);;val power : int -> float -> float = <fun >

Successivamente, testarla

# power 5 2.0;;- : float = 32

e poi definire, dato un dx fissato ed una funzione f generica, l’approssimazione numericadella derivata di f in x, i.e.

f ′(x) =f(x+ dx)− f(x)

dx

let dx = 1e-10;;val dx : float = 1e-10let deriv f = (fun x -> (f (x +. dx) -. f x) /. dx);;val deriv : (float -> float) -> float -> float = <fun >

Fissare uno degli argomenti di power, e calcolarne la derivata in 10

31

# let f = power 3;;val f : float -> float = <fun ># f 10.0;;- : float = 1000# let f’ = deriv f;;val f’ : float -> float = <fun ># f’ 10.0;;- : float = 300.000237985

Se iterate, che succede con la derivata seconda?

32

Capitolo 4

Scrivere interpreti in Ocaml

Le poche cose su Ocaml viste fino ad ora sono sufficienti per realizzare un semplice intepretedi un linguaggio imperativo/funzionale. In questo capitolo vedremo brevemente come definireun interprete di un linguaggio di programmazione imperativo, discuteremo in cosa differisca da uncompilatore. Per arrivare a definire l’interprete del linguaggio While definiremo prima l’interpretedi due linguaggi che permettono di definire le espressioni che ci interessano in While: Express eσ-Express.

4.1 Interpretazione vs compilazioneL’inteprete di un linguaggio di programmazione è un programma che si occupa di eseguire program-mi scritti in tale linguaggio. Il compilatore di un linguaggio di programmazione è invece un pro-gramma che si occupa di tradurre programmi scritti in tale linguaggio in un formato direttamenteeseguibile da un calcolatore (linguaggio macchina).

Più precisamente, un interprete (Fig. 1) prende in input un programma da eseguire e l’inputper tale programma (ad esempio, potrebbe prendere in input il programma che esegue il calcolodel fattoriale e il numero di cui si vuole calcolare il fattoriale) esegue una dopo l’altra le istruzionicontenute nel programma e restituisce l’output del programma (nell’esempio, il valore del fattoria-le). Un compilatore (Fig. 2) prende in input un programma (ad esempio il programma che esegueil calcolo del fattoriale) e restituisce un file eseguibile contenente la traduzione del programma inlinguaggio macchina. Tale file in linguaggio macchina potrà essere eseguito con qualunque input(nell’esempio, con qualunque valore di cui si vuole calcolare il fattoriale) e restituirà per ogni input,l’output corrispondente (il risultato del calcolo del fattoriale).

Le principali differenze (in termini di vantaggi e svantaggi) tra l’interpretazione e la compila-zione di un linguaggio sono le seguenti:

Figura 4.1: Schema di funzionamento di un interprete

33

Figura 4.2: Schema di funzionamento di un compilatore

• La compilazione offre di solito vantaggi dal punto di vista dell’efficienza nell’esecuzione deiprogrammi in linguaggio macchina rispetto all’esecuzione fatta da un interprete.

• L’interpretazione consente di eseguire i programmi in un ambiente “protetto” (l’interpretestesso) consentendo di evitare che i programmi eseguano operazioni “pericolose”. I linguaggidi programmazione usati per realizzare pagine web o programmi che vengono eseguite tramitel’accesso alla rete sono spesso interpretati.

Come funziona un interprete. Un interprete di un linguaggio di programmazione esegueprogrammi scritti usando tale linguaggio. In altre parole un interprete può essere visto come un’implementazione della semantica del linguaggio.

La sintassi dei linguaggi di programmazione spesso consentono di scrivere programmi “scorretti”a cui non corrisponde una semantica, ovvero programmi che possono raggiungere uno stato in cuinon si riesce ad applicare nessuna regola della semantica (e.g. si pensi al caso dell variabili libereincontrato precedentemente).

Al fine di evitare di eseguire tali programmi che prima o poi si bloccherebbero, un interpretenormalmente esegue alcuni controlli statici. I controlli statici si possono dividere in due categorie:

• il type checking, ovvero il controllo che il programma sia ben scritto dal punto di vista deitipi (i.e. si pensi all’espressione 3+2.0 in Ocaml);

• le analisi, ovvero il controllo di proprietà di correttezza cercando di seguire il flusso diesecuzione del programma.

Nel seguito vedremo come implementare in Ocaml un interprete dei linguaggi Express, σ-Express e While. Nel prossimo capitolo ci occuperemo dell’ implementazione di un type checkere di un un analizzatore per il linguaggio While.

4.2 Express: il linguaggio delle sole espressioniConsideriamo il solo linguaggio delle espressioni su interi e booleani, denominato Express, definitecome segue.

Definition 30 (Express-syntax)

E ::= n∣∣ true

∣∣ false∣∣ ¬E ∣∣ E bop E

dove n ∈ Z e bop ∈ {+,−, ∗./, mod ,=, <=,&&, ||}.

Notate che queste sono tutte e sole le espressioni senza variabili! Inoltre, per semplificareleggermente la definizione dell’interprete del linguaggio assumiamo che l’uguaglianza = sia definita

34

solo su interi. Ricordiamo che per confrontare due espressioni booleane e1 ed e2 si può usare laseguente formula

(e1&&e2) || (¬e1&&¬e2) .

Definiamo un interprete per questo linguaggio.

Implementare la sintassi. Per implementare la sintassi la prima cosa da fare è definire i tipiche prenderemo in considerazione. Più precisamente, dobbiamo definire i tipi che rispondono alleseguenti domande:

(i) Qual’è il risultato della valutazione di una espressione intera / booleana?

(ii) Che tipo hanno le espressioni?

Implementare la sintassi del linguaggio Express a questo livello vuol dire definire in Ocaml lastruttura dei tipi che rispondono a quelle domande. Di conseguenza abbiamo che:

(ii) Una epressione intera deve valutare ed un tipo intero, e quella booleana ad un booleano. Lacosa più naturale da farsi è mappare i valori interi del linguaggio Express negli interi diOcaml, e fare la stessa cosa con i booleani.

(* tipo dei valori (risultato della valutazione di espressioni) *)type eval =

Bool of bool| Int of int;;

(iii) Una volta definiti i tipi Int e Bool possiamo definire un tipo più generale exp che denoti leespressioni. Tale tipo deve permettere di costruire ciascuna delle possibili definizioni sintat-tiche date nella definizione precedente, per cui avremo, per ogni e1 bop e2, dove bop denotaun operatore, un tipo opportuno di espressione

Bop of exp * exp .

Si noti che, poichè si possono combinari i vari operatori, allora il tipo che dobbiamo definiredeve essere abbastanza potente da poter avere una dimensione qualunque. In tal senso, untipo ricorsivo ci permette di definire con facilità tipi di lunghezza variabile.

(* tipo delle espressioni *)type exp =

Num of int (* un numero *)| Add of exp*exp (* somma *)| Sub of exp*exp (* sottrazione *)| Mul of exp*exp (* moltiplicazione *)| Div of exp*exp (* divisione *)| Mod of exp*exp (* resto *)| True (* costante true *)| False (* costante false *)| Eq of exp*exp (* test per l’uguaglianza *)| Leq of exp*exp (* test per la disuguaglianza *)| Not of exp (* negato di un ’espressione *)| And of exp*exp (* congiunzione di espressioni *)| Or of exp*exp;; (* disgiunzione di espressioni *)

Implementare la semantica. La prima cosa di cui abbiamo bisogno è la semantica operazionaledi Express. Sarete convinti che tale semantica sia definita dala seguente relazione di transizione.

35

(Axm1)n⇒ n

(Not1)e⇒ true

¬e⇒ false

(Not2)e⇒ false

¬e⇒ true

(Op)e1 ⇒ v1 e2 ⇒ v2 v1 op v2 = v

e1 op e2 ⇒ v

Che altro non sono che alcune delle regole di semantica operazionale delle espressioni di Sim-pleCAML con ¬ al posto di not. Discutiamo adesso l’implementazione di questa semantica inOcaml. Come per la sintassi, possiamo iniziare ponendoci delle domande:

(i) Dobbiamo mai effettuare dei controlli sui tipi a runtime? Può accadere che una espressionesia valutato con dei parametri dai tipi incompatibili? Se dovessimo fare controllo dei tipi aruntime, quando potremo farlo? Direttamente nella valutazione di una espressione?

Ecco come possiamo, rispondendo a queste domande, implementare in Ocaml la semantica dellinguaggio Express.

(i) Ovviamente essendo un interprete non possiamo assumere alcun controllo di tipi eseguitoapriori sul codice che dobbiamo interpretare e, quindi, dobbiamo esplicitamente controllarela correttezza. Intuitivamente, le operazioni aritmetiche di base dovranno controllare che iloro argomenti siano entrambi interi, ovvero Int, mentre le operazioni booleane dovrannocontrollare che siano solo booleani, ovvero Bool. Iniziamo con il dichiarare un’eccezione cheidentifichi questo tipo di errore.

(* eccezione sollevata a tempo di esecuzione (nella semantica)* quando si valuta un ’espressione contenente un errore di tipo *)

exception TypeMismatch of exp;;

Adesso, dato che il controllo di tipi e la valutazione della semantica delle espressioni possonoessere fatte nello stesso momento (i.e da cui il nome “controllo a runtime dei tipi”) possiamodefinire la semantica. Nel definirla faremo uso di due funzioni ausiliarie, intval e boolval,le quali controllano se l’espressione e passata loro come argomento abbia effettivamente tipoInt, nel caso di intval e Bool, nel caso di boolval.

(* implementazione della semantica di un’espressione e.* Solleva TypeMismatch se e contiene un errore di tipo.*)

let rec sem_exp e =match e with

Num n -> Int n| Add (e1,e2) -> Int (intval e1 + intval e2 )| Sub (e1,e2) -> Int (intval e1 - intval e2 )| Mul (e1,e2) -> Int (intval e1 * intval e2 )| Div (e1,e2) -> Int (intval e1 / intval e2 )| Mod (e1,e2) -> Int (intval e1 mod intval e2 )| True -> Bool true| False -> Bool false| Eq (e1,e2) -> Bool (intval e1 = intval e2 )| Leq (e1,e2) -> Bool (intval e1 <= intval e2 )| Not e’ -> Bool (not (boolval e’ ))| And (e1,e2) -> Bool (boolval e1 && boolval e2 )| Or (e1,e2) -> Bool (boolval e1 || boolval e2 )

(* funzione accessoria che controlla che l’espressione e valuti* ad un intero e restituisce il valore intero stesso in modo* che possa essere elaborato usando le operazioni su int di

36

* ocaml.* Solleva TypeMismatch se e non ha tipo intero.*)

and intval e sigma =match (sem_exp e) with

Int n -> n| _ -> raise (TypeMismatch e)

(* funzione accessoria che controlla che l’espressione e valuti* ad un booleano e restituisce il valore booleano stesso in modo* che possa essere elaborato usando le operazioni su bool di* ocaml.* Solleva TypeMismatch se e non ha tipo booleano.*)

and boolval e =match (sem_exp e) with

Bool b -> b| _ -> raise (TypeMismatch e);;

Si noti che, come stabilito, il controllo dei tipi viene fatto dipendentemente dall’operatoreche stiamo considerando. Così, ad esempio, nel valutare una Add si controllano i tipi con laintval, mentre nel valutare una Eq si usa la boolval.

Alcuni esempi di valutazione di espressioni.

# sem_exp (Mul( Num 3, Num 2));;- : eval = Int 6# sem_exp (Mul( Num 3, True ));;Exception: TypeMismatch True.# sem_exp (Mul( Add( Num 3, Num 5), Sub( Num 10, Num 2) ));;- : eval = Int 64

4.3 σ-Express : il linguaggio delle espressioni con variabiliConsideriamo il linguaggio σ-Express definito dalla seguente sintassi

Definition 31 (σ-Express-syntax)

E ::= n∣∣ true

∣∣ false∣∣ id

∣∣ ¬E ∣∣ E bop E

dove n ∈ Z, id ∈ V ar è una generica variabile dall’insieme V ar di tutte le possibili variabili ebop ∈ {+,−, ∗./, mod ,=, <=,&&, ||}.

Si nota immediatamente che queste espressioni possono contenere variabili, ma il linguaggionon permette di definire valori espliciti per le variabili (i.e. non ci sono assegnamenti). In pratical’interpretazione di una espressione di σ-Express sarà dipendendete da una struttura (statica) chefornisce i valori per le variabili. Formalmente, useremo una memoria (store) statico.

Implementare la semantica. Vediamo, per differenze rispetto a Express, come implementarela sintassi del nuovo linguaggio.

• Gli identificatori di variabili possono essere ragionevolmente stringhe, come in ogni altrolinguaggio di programmazione.

(* tipo degli identificatori *)type ide = string ;;

• Lo store statico può essere definito cosi: sia l’insieme dei valori V = Z ∪ {true, false}, unouno store σ è una una funzione che applicata ad una variabile ne fornisce il valore corrente,dunque

σ : V ar → V

37

se V ar denota l’insieme dei possibili identificatori. Per ipotesi in questo caso lo store èstatico, quindi in generale possiamo assumere che lo store sia definito per i nomi di variabiliche compaiono all’interno delle espressioni che vogliamo valutare. Questo significa che, ingenerale, se

σ = {(x1, y1), . . . (xn, yn)}

allora∀x ∈ V ar\{x1, . . . , xn}. σ(x) =⊥ .

Questo significa che possiamo implementare lo store usando una eccezione come segue

(* eccezione sollevata a tempo di esecuzione (nella semantica)* quando si usa in un’espressione una variabile non inizializzata *)

exception UnboundIde of ide;;

e che, (per ipotesi) chi definisce uno store lo definisca come

let mystore = function"x_1" -> y_1

| "x_2" -> y_2|.......| "x_n" -> y_n| _ -> raise (UnboundIde x);;

• Aggiorniamo la definizione della sintassi di Express come segue

(* tipo delle espressioni *)type exp =

Num of int (* un numero *)| Val of ide (* il valore di una variabile *)....| Or of exp*exp;; (* disgiunzione di espressioni *)

dove il costrutto Val of ide implementa la definizione di una variabile in una espressione.

Noteremo come nel linguaggio While il vincolo sulla staticità dello store verrà rimosso perpermettere all’utente di specificare variabili direttamente all’interno dei programmi.

Implementare la semantica. La semantica di σ-Express si definisce come segue.

(Axm1)(n, σ)⇒ n

(Val)x ∈ V ar σ(x) = v

(x, σ)⇒ v

(Op)(e1, σ)⇒ v1 (e2, σ)⇒ v2 v1 op v2 = v

(e1 op e2, σ)⇒ v

(Not1)(e, σ)⇒ true

¬(e, σ)⇒ false

(Not2)(e, σ)⇒ false

¬(e, σ)⇒ true

Si noti che, come ipotizzato, la semantica di una espressione dipende dallo store in cui si valutal’espressione. Una immediata conseguenza sarà che la sem_exp avrà un nuovo tipo della forma

val sem_exp : exp -> (ide -> eval) -> eval = <fun>

In Express tale store non era necessario data l’assenza delle variabili. Possiamo dunqueimplementare la semantica di σ-Express come segue

38

(* implementazione della semantica di un’espressione e dato lo* store sigma.* Solleva TypeMismatch se e contiene un errore di tipo.* Solleva UnboundIde se e contiene una variabile non inizializzata.*)

let rec sem_exp e sigma =match e with

Num n -> Int n| Val x -> sigma x| Add (e1,e2) -> Int (intval e1 sigma + intval e2 sigma)| Sub (e1,e2) -> Int (intval e1 sigma - intval e2 sigma)| Mul (e1,e2) -> Int (intval e1 sigma * intval e2 sigma)| Div (e1,e2) -> Int (intval e1 sigma / intval e2 sigma)| Mod (e1,e2) -> Int (intval e1 sigma mod intval e2 sigma)| True -> Bool true| False -> Bool false| Eq (e1,e2) -> Bool (intval e1 sigma = intval e2 sigma)| Leq (e1,e2) -> Bool (intval e1 sigma <= intval e2 sigma)| Not e’ -> Bool (not (boolval e’ sigma))| And (e1,e2) -> Bool (boolval e1 sigma && boolval e2 sigma)| Or (e1,e2) -> Bool (boolval e1 sigma || boolval e2 sigma)

(* stessa funzione accessoria di Express *)and intval e sigma =

match (sem_exp e sigma) withInt n -> n

| _ -> raise (TypeMismatch e)(* stessa funzione accessoria di Express *)and boolval e sigma =

match (sem_exp e sigma) withBool b -> b| _ -> raise (TypeMismatch e);;

Testiamo la nostra implementazione. Definiamo uno store

σ = {(x, 35), (y, 12)}

ovvero

# let mystore = function"x" -> Int 35| "y" -> Int 12| v -> raise (UnboundIde v);;val mystore : ide -> eval = <fun >

e testiamo alcune espressioni

# sem_exp (Mul( Num 2, Val "x")) mystore ;;- : eval = Int 70# sem_exp (Mul( Num 3, Add( Num 3, Val "y"))) mystore ;;- : eval = Int 45# sem_exp (Mul( Val "z", Add( Num 3, Val "y"))) mystore ;;Exception: UnboundIde "z".

Nell’ultimo caso, come richiesto, l’eccezione viene sollevata dato che z non è definita.

4.4 While: un linguaggio imperativoLa versione del linguaggio While a cui ci riferiamo è un sottoinsieme minimo di un linguaggioimperativo senza procedure. Richiamiamo la sintassi del linguaggio While.

39

Definition 32 (While-syntax)

E ::= n∣∣ true

∣∣ false∣∣ id

∣∣ ¬E ∣∣ E bop E

C ::= skip∣∣ x := E

∣∣ if E then C else C∣∣ while E do C

∣∣ C;C

dove n ∈ Z, id ∈ V ar è una generica variabile e bop ∈ {+,−, ∗./, mod ,=, <=,&&, ||}.Si noti immediatamente che le espressioni di σ-Express sono valide in While.

Implementare la sintassi. Per implementare la sintassi la prima cosa da fare è, come in σ-Express ed Express, definire i tipi che prenderemo in considerazione. Più precisamente, l’equi-valenza tra le espressioni di σ-Express e di While ci permette di riusare parte delle definizioniprecedenti.

Abbiamo le seguenti definizioni equivalenti.type ide = string ;;

type eval =Bool of bool

| Int of int;;

type exp =Num of int

| Val of ide (* il valore di una variabile *)....| Or of exp*exp;;

Dobbiamo tuttavia estendere la strutture dei tipi per riflettere la sintassi dei comandi di While.Possiamo definire un tipo com per i comandi che consideriamo in While. Ovviamente in questocaso i tipi sono maggiormente “strutturati” nel senso che, ad esempio, un assegnamento sarà dellaforma

ide = exp

mentre un if-then-else sarà della forma

if exp then com else com .

(* tipo dei comandi *)type com =

Skip (* il comando che non fa nulla *)| Assign of ide*exp (* assegnamento *)| Cseq of com list (* sequenza di comandi *)| If of exp*com*com (* costrutto condizionale *)| While of exp*com;; (* costrutto iterativo *)

Si noti che il dominio dei valori su cui diamo una semantica, gli eval, non è mai cambiato.Inoltre, si noti la differenza nell’implementazione del costrutto sequenziale

c0; c1

che non è implementato cometype com =

....| Cseq of com * com....

il che sarebbe la soluzione corretta. Infatti, l’usare liste di Ocaml nei comandi While (i.e. inCseq of com list il list appartiene ad Ocaml) corrisponde a mischiare la sintassi del linguaggioWhile con Ocaml, il che è sbagliato. Tuttavia, l’usare una lista ci permette, nei pochi programmiWhile che definiremo, di scrivere una sequenza di comandi

c0; c1; . . . ; cn−1; cn

come un lista maggiormente “leggibile” della forma

40

Cseq ([ c_0; c_1; ....; c_n ])

invece che come annidamento di svariati Cseq

Cseq ( c_0 , Cseq( c_1 , Cseq (....)) )

Implementare la semantica. Consideriamo le stesse memorie di σ-Express rimuovendo ilvincolo di staticità.

σ : V ar → V

Adesso la memoria di un programma cambia dinamicamente nel tempo, sia nei valori che essa con-tiene associati agli identificatori, sia per la creazione di nuovi identificatori. In generale denotiamocon σ[x 7→ v] lo store in cui la variabile x è aggiornata al nuovo valore v, ovvero

σ[x 7→ v](y) =

{v se x = y

σ(y) altrimenti.

La semantica di While la si da definendo due relazioni di transizione

⇒ per valutare le espressioni;

→ per valutare i comandi usando, se necessario, la ⇒.

Ovviamente, anche in questo caso usiamo la relazione ⇒ di σ-Express, ovvero

〈e, σ〉 ⇒ v .

per un’espressione e e uno store σ in cui v sia il risultato della valutazione di e in σ. La semanticadei comandi viene data esplicitamente dalla relazione di transizione → che dato un comando c euno store σ fornisce un nuovo store σ′ risultato dell’esecuzione del comando c, ovvero

〈c, σ〉 → σ′ .

La relazione → è definita come segue:

(Skip)〈 skip , σ〉 → ρ

(Assign)〈e, σ〉 ⇒ v

〈x := e, ρ〉 → σ[x 7→ v]

(Cond1)〈e, σ〉 ⇒ true 〈c1, σ〉 → σ′

〈 if e then c1 else c2, σ〉 → ρ′

(Cond2)〈e, σ〉 ⇒ false 〈c2, σ〉 → σ′

〈 if e then c1 else c2, σ〉 → σ′

(While1)〈e, σ〉 ⇒ true 〈c, σ〉 → σ′ 〈while edo c, σ′〉 → σ′′

〈while edo c, σ〉 → σ′′

(While2)〈e, σ〉 ⇒ false

〈while edo c, σ〉 → σ

(ComSeq)〈c1, σ〉 → σ′ 〈c2, σ′〉 → σ′′

〈c1; c2, σ〉 → σ′′

Questa semantica è ovviamente data in termini della sequenzializzazione “;” e non della lista dicomandi, come detto precedentemente, ma a questo punto risulta abbastanza evidente che si possaottenere una semantica “equivalente” per la lista di comandi, data la semantica del “;”, riflettere sucome sia possibile.

41

Discutiamo adesso l’implementazione di questa semantica in Ocaml. Dovremo iniziare imple-mentando questo nuovo tipo di memoria modificabile. Risulta naturale immaginare lo store comeuna struttura che si modifica nel tempo, partendo dalla memoria inizialmente vuota, medianteoperazioni di raffinamento.

Uno store inizialmente vuoto σ0 tale che σ0(x) =⊥ per ogni identificatore x è dato da

(* funzione che costruisce uno store vuoto *)let emptystore = fun x -> raise (UnboundIde x);;

L’operazione di modifica/aggiornamento di uno store definito la possiamo quindi implementarecome segue

(* funzione che aggiorna uno store sigma assegnando all ’identificatore* x il valore d *)

let update sigma x d = fun y -> if x=y then d else sigma y;;

A questo punto possiamo importare in toto la definizione della funzione sem_exp di σ-Express.

exception TypeMismatch of exp;;

let rec sem_exp e sigma =match e with

Num n -> Int n| Val x -> sigma x

...| Or (e1,e2) -> Bool (boolval e1 sigma || boolval e2 sigma)

and intval e sigma = ....and boolval e sigma = ....

Possiamo implementare separatamente la semantica dei comandi definiendo una funzione, ov-viamente ricorsiva, denominata sem_com.

(* implementazione della semantica di un comando c dato lo* store sigma.* Solleva TypeMismatch se si incontra un errore di tipo.* Solleva UnboundIde se si incontra una variabile non inizializzata.*)

let rec sem_com c sigma =match c with

Skip -> rho| Assign (x,e) -> update sigma x (sem_exp e sigma)| Cseq (c’::cl) -> sem_com (Cseq cl) (sem_com c’ sigma)| Cseq [] -> sigma| If (b,c1,c2) ->

if boolval b sigmathen sem_com c1 sigmaelse sem_com c2 sigma

| While (b,c’) ->if boolval b sigmathen sem_com c (sem_com c’ sigma)else sigma;;

Si noti che in questo caso la funzione effettua il controllo dei tipi a runtime per il fatto che, inpratica, usi la funzione sem_exp la quale, a sua volta, può sollevare delle eccezioni. Si noti inoltreche, se avessimo adottato il tipo corretto per la sequenzializzazione, avremo dato questa semantica

let rec sem_com c sigma =match c with

...| Cseq (c’, c’’) -> sem_com c’’ (sem_com c’ sigma)

...

42

Invece, in questo caso, ci portiamo dietro un pezzo di sintassi nella valutazione di Cseq (c’::cl)dato che valutiamo la sem_com su (Cseq cl).

Ora che abbiamo finito con la definizione della semantica di questo semplice linguaggio possiamofinalmente scrivere programmi While. Riconoscete questo programma?

let fact n = Cseq [Assign ("n",Num n);Assign ("res",Num 1);While (Not (Leq (Val "n",Num 1)),

Cseq [Assign ("res", Mul (Val "res",Val "n"));Assign ("n",Sub (Val "n",Num 1));

])];;

Testatelo con

let sigma = sem_com (fact 3) emptystore ;;sigma("res");;

43

Capitolo 5

Cenni di analisi statica

L’analisi statica consiste nel definire algoritmi che testino proprietà dei programmi senza eseguirli.In pratica, l’analisi statica lavora solo guardando la sintassi con cui i programmi sono scritti, e noneseguendoli. In questo capitolo vedremo due tipi comuni di analisi statica.

5.1 Type-checking del linguaggio While

Se, in un qualche linguaggio, io dichiaroint x;

e poi eseguo un assegnamento della forma

x = true

cosa succede? Non sempre succede la stessa cosa, ogni linguaggio fa le sue scelte. Ad esempio inJava l’output del compilatore sarebbe qualcosa del genere....Test.java :42: incompatible typesfound : booleanrequired: int

int x = false;^

1 error

Questo avviene perchè il compilatore nota che x sia una variabile dichiarata intera ma che, nelprogramma, sia assegnata ad un valore booleano. Questo tipo di controllo si chiama “type-checking”.Tecnicamente il type-checking è l’analisi che consiste nel controllare che i valori assegnati ad unavariabile (e.g. in questo caso false) siano di un tipo di dato (e.g. in questo caso bool) ammissibileper il tipo della variabile stessa (e.g. in questo caso int).

Nei linguaggi che noi consideriamo il tipo ammissibile coincide con il tipo della variabile stessamentre, in alcuni linguaggi con struttura di tipi maggiormente sofisticata (i.e. Java), tale nozioneconsiste nell’avere una relazione (spesso denominata super-tipo e sotto-tipo a denotare che si trattadi una rlazione d’ordine) tra i tipi dell’assegnamento e della variabile. Ovviamente i linguagginon-tipati non hanno alcun problema di questo tipo.

Come sembra intuitivo, alcuni linguaggi utilizzano un type-checking statico, ovvero effettua-no questo controllo al momento della compilazione, e rifiutano di compilare un programma incaso di errore. Altri, invece, effettuano il type-checking a runtime, e il compilatore incorporaautomaticamente nei programmi eseguibili la logica per valutare se un assegnamento è ammissibile.

Nel nostro caso vogliamo aggiungere controlli di type-checking statico al lingugaggio While. Laprima cosa da fare è quindi definire una estensione del linguaggio con le dichiarazioni di variabili,cosa che adesso non esisteva dato che in un comando come

Assign (”n”,Num 3);

non c’è scritto da nessuna parte che n sia di tipo intero.

44

Definition 33 (While-types) Estendiamo la sintassi While introducendo il concetto di program-ma P inteso come una lista di dichiarazioni di variabili D, seguita da un comando C:

D ::= int id∣∣ bool id

∣∣ D;D

P ::= C∣∣ D;C

dove id è un identificatore di variabile e C è un comando definito come nei capitoli precedenti.

Dobbiamo, come nei casi precedenti, implementare la sintassi dei programmi, e poi la lorosemantica.

Implementare la sintassi. La sintassi dei programmi può essere implementata in Ocamlusando, come al solito, dei tipi.

(* tipo dei tipi usati nelle dichiarazioni di variabili *)type types = Int_type | Bool_type ;;

(* tipo delle dichirazioni di variabili *)type decl = types*ide;;

(* tipo di un programma *)type prog = Program of decl list*com;;

Si noti che anche in questo caso, come per Cseq, usiamo decl list * com per implementare unalista di dichiarazioni seguita da un comando, il programma.

Implementare la semantica. Dato un programma P , sia

Γ : V ar(P )→ {int,bool}

il typing environment una funzione dalle variabili di P a tipi ottenuto dalle dichiarazioni che sitrovano all’inizio di P . Per semplicità si assume che se una variabile è dichiarata più volte in P ,il tipo di tale variabile in Γ sarà quello della prima dichiarazione. Ad esempio, sia P il seguenteprogramma:

int x; int y; bool x;x:=3; y:=5+x;

la Γ corrispondente sarà la funzione definita su {x, y} tale che

Γ(x) = int Γ(y) = bool .

La procedura di type checking per le espressioni sarà descritta dalla relazione ternaria ` su untyping enviroment, un’espressone e un tipo. Intuitivamente, tale relazione sarà usata come segue:quando vale

Γ ` e : int

si intenderà che, dato il typing environment Γ ottenuto dalle dichiarazioni di tipo, l’espressione eè corretta dal punto di vista dei tipi e ha complessivamente tipo intero.

La relazione ` per le espressioni è definita induttivamente usando regole di inferenza. Gliassiomi sono dati da.

(Axm1)Γ ` n : int

(Axm2)Γ ` true : bool

(Axm3)Γ ` false : bool

45

Mentre i casi ricorsivi sono i seguenti.

(Var)x ∈ dom(Γ)

Γ ` x : Γ(x)

(Sum)Γ ` e1 : int Γ ` e2 : int

Γ ` e1 + e2 : int(regole analoghe per − .∗, /, mod )

(Eq)Γ ` e1 : int Γ ` e2 : int

Γ ` e1 = e2 : bool(regola analoga per <=)

(And)Γ ` e1 : bool Γ ` e2 : bool

Γ ` e1&&e2 : bool(regola analoga per ||)(Not)

Γ ` e : bool

Γ ` ¬e : bool

Per quanto riguarda i comandi, una relazione per esprimere il type checking sarà una relazionebinaria e non ternaria, in quanto un comando non ha un tipo dato che non viene valutato in unvalore. La relazione in questo caso verrà usata come segue: con

Γ ` c

si intenderà che il comando c è corretto per quanto riguarda i tipi, in un typing environment Γ.La relazione per i comandi è definita con un solo assioma

(Axm)Γ ` skip

e le seguenti definizioni ricorsive

(Assign)Γ ` e : Γ(x)

Γ ` x := e

(Cond)Γ ` e : bool Γ ` c1 Γ ` c2

Γ ` if e then c1 else c2

(While)Γ ` e : bool Γ ` cΓ ` while edo c

(Seq)Γ ` c1 Γ ` c2

Γ ` c1; c2

Implementiamo questa relazione di transizione in Ocaml. La prima cosa da fare è pensare adeeventuali comportamenti eccezionali. Ad esempio, cosa succede se si incontra una variabile nondichiarata? Oppure, se si scopre un errore di tipo, quale sarà il valore restituito dalla funzione cheimplementeremo.

Usaremo delle eccezioni per rispondere ad entrambe queste domande. Le definiamo come segue.

(* eccezione sollevata durante il type -checking quando si* incontra in un ’espressione una variabile non dichiarata* (ovvero non presente tra le dichiarazioni di variabili)*)

exception UndeclaredVar of ide;;

(* eccezione sollevata durante il type -checking quando si* individua un errore di tipo *)

exception TypeError of exp;;

A questo punto, preoccupiamoci di definire una funzione che costruisce, data una lista didichiarazioni di variabili, la funzione Γ. Possiamo definirla come segue.

(* funzione che costruisce un ambiente dei tipi (ovvero una* funzione da variabili a tipi) a partire da una lista di* dichiarazioni di tipo.* L’ambiente dei tipi solleva UndeclaredVar se viene

46

* interrogato con un identificatore non presente nella lista* delle dichiarazioni*)

let rec build_env = function(t,x) :: dl ->

fun y ->if y=x then telse (build_env dl) y

| [] -> fun y -> raise (UndeclaredVar y);;

o, se preferite, come

let rec build_env l = match l with| [] -> fun y -> raise (UndeclaredVar y)| (t,x) :: dl -> fun y -> if y=x then t else (build_env dl) y ;;}

Questa funzione sarà usata per definire la semantica di un programma. Prima di arrivare adusare tale funzione nella gestione dei programmi dobbiamo comunque implementare la relazioneche abbiamo discusso prima sulle espressioni.

(* funzione che controlla che un’espressione e non contenga* errori di tipo assumendo che le variabili abbiano i tipi* specificati dall ’ambiente env.* Solleva TypeError se si incontra un errore di tipo.* Solleva UndeclaredVar se si incontra un identificatore non* presente nell ’ambiente env.*)

let rec exp_type e env =match e with

Num n -> Int_type| ( True | False ) -> Bool_type| Val x -> env x| ( Add (e1 ,e2)

| Sub (e1,e2)| Mul (e1,e2)| Div (e1,e2)| Mod (e1,e2)) -> if (( exp_type e1 env = Int_type) &&

(exp_type e2 env = Int_type ))then Int_type else raise (TypeError e)

| ( Eq (e1,e2) | Leq (e1,e2) )-> if (( exp_type e1 env = Int_type) &&

(exp_type e2 env = Int_type ))then Bool_type else raise (TypeError e)

| Not e’ -> if (exp_type e’ env = Bool_type)then Bool_type else raise (TypeError e)

| ( And (e1,e2) | Or (e1,e2) )-> if (( exp_type e1 env = Bool_type)

&& (exp_type e2 env = Bool_type ))then Bool_type else raise (TypeError e)

;;

Mentre la definizione della relazione sui comandi diventa una funzione che restituisce true ofalse se i comandi sono ben tipati.

(* funzione che controlla che un comando non contenga errori* di tipo assumendo che le variabili abbiano i tipi* specificati dall ’ambiente env.* Solleva TypeError se si incontra un errore di tipo.* Solleva UndeclaredVar se si incontra un identificatore non* presente nell ’ambiente env.*)

47

let rec type_check c env =match c with

Skip -> true| Assign (x,e) ->

if (exp_type e env = env x) then trueelse raise (TypeError e)

| Cseq (c’::cl) -> type_check c’ env && type_check (Cseq cl) env| Cseq [] -> true| If (b,c1,c2) ->

if (exp_type b env = Bool_type)then type_check c1 env && type_check c2 envelse raise (TypeError b)

| While (b,c’) ->if (exp_type b env = Bool_type)then type_check c’ envelse raise (TypeError b)

;;

A questo punto cosa diventa un programma con il type-checking annesso? Intuitivamente, sepensassimo a come definire una regola operazionale potremmo scrivere

Γ(dl) ` c 〈c, σ〉 → σ′

〈Program (dl, c), σ〉 → σ′

dove Γ(dl) denota il typing environment costruito dalle dichiarazioni presenti in dl. In questo caso,possiamo implementare questa regola come segue

(* funzione che esegue un programma dopo aver controllato che* non contenga errori di tipo.* RESTITUISCE: lo store ottenuto al termine dell ’esecuzione.* SOLLEVA: UndeclaredVar se si incontra una variabile non* dichiarata , TypeError se si incontra un errore di tipo ,*)

let sem_prog (Program (dl,c)) =if (type_check c (build_env dl))then sem_com c emptystoreelse emptystore

;;

Si noti che, in pratica, associamo una semantica diversa dallo store vuoto solo se il programmanon contiene errori di tipo, come atteso. Tuttavia, per costruzione, o il programma “schianta”, oesegue correttamente, potenzialmente non terminando. Quindi il ramo then del condizionale nonviene mai eseguito.

Esempi.

• Vediamo adesso qualche semplice esempio per chiarirci le idee. Prima definiamo un ambiente“a mano” (anche se lo potremo fare con un programma!)

let mydecl = [(Int_type ,"x");( Bool_type ,"y");( Int_type ,"y")];;let myenv = build_env mydecl ;;

In pratica, build_env costruisce le coppie che ci servono, infatti

myenv "x";; (* Int_type *)myenv "y";; (* Bool_type *) (* la prima dichiarazione vince *)

Per provare a controllare i tipi di alcuni comandi possiamo fare, ad esempio, le seguentioperazioni

48

let c’ = Add (Val "x",Num 1);;exp_type c’ myenv ;;let c’’ = Add (Val "y",Num 1);;exp_type c’’ myenv ;;

Provatele e vedete cosa succede.

• Un esempio d’uso del type-checker diventa il seguente programma (ormai noto) ma, stavolta,con la dichiarazione delle variabili che vengono utilizzate!

let fact n = (Program( [(Int_type ,"n");( Int_type ,"res")] ,(Cseq [

Assign ("n",Num n);Assign ("res",Num 1);While (Not (Leq (Val "n",Num 1)),

Cseq [Assign ("res", Mul (Val "res",Val "n"));Assign ("n",Sub (Val "n",Num 1));

])])

));;

Lo possiamo testare con

let r = sem_prog fact;;

r "res";; (* Int 24 *)

• Adesso costruiamo un programma che si comporti come segue

(* -------------------------* flag := 1;* if (flag = 0) then {* res := 4;* }* else {* res := true;* res2 := 77;* }* -------------------------*)

Da cui, seguendo la specifica, otteniamo il seguente programma While.

let p = (Program( [(Int_type ,"flag");( Bool_type ,"res");( Int_type ,"res2")],

(Cseq [Assign ("flag",Num 1) ;If (Eq(Val "flag",Num 0),

Cseq [Assign ("res",Num 4) ;Skip

],Cseq [

Assign ("res",True) ;Assign ("res2",Num 77)

])])

));;

Questo programma si testa come segue.

49

let r = sem_prog p;;

r "res";; (* Bool true *)r "res2";; (* Num 77 *)

5.2 Analisi dataflow del linguaggio While

Consideriamo il seguente programma

int x;int y;

x = y + 3;

se si cerca di compilarlo il compilatore si lamenta del fatto che l’espressione y+3 usa la variabile yche non è inizializzata. In generale, se si eseguisse questo programma si osserverebbe un errore aruntime che, nel caso il programma fosse scritto in linguaggio While sarebbe una eccezione dellaforma UnboundIde y.

L’analisi dataflow che consideriamo si occupa di verificare la seguente proprietà: ogni variabileche viene valutata nello store σ è stata precedentemente inizializzata. Questa proprietà garantisceche l’eccezione UnboundIde non venga mai sollevata.

L’analizzatore dataflow non richiede di modificare la sintassi del linguaggio. Vediamo diretta-mente l’algoritmo di analisi.

Implementare la semantica. Formalmente consideriamo la relazione

X |= e

dove X ⊆ ℘(V ar) ed e una espressione. Il significato è che le variabili usate nell’espressione ecompaiono nell’insieme X. Tale relazione la si definisce con gli assiomi

(Axm1)X |= n

(Axm2)X |= true

(Axm3)X |= false

ed usando i seguenti casi ricorsivi.

(BinOp)X |= e1 X |= e2X |= e1 op e2

(per ogni op binario)

(Not)X |= e

X |= ¬e

A qeusto punto, definiamo una relazione sui comandi in modo tale che

(c,X) Y

se in c vengono inizializzate delle variabili, allora le aggiungiamo all’insieme X che contiene levariabili già inizializzate e che possono essere usate dentro c. Tale relazione si definisce come seguecon degli assiomi

(Skip)( skip , X) X

(Assign)X |= e

(x := e,X) X ∪ {x}

50

e le seguenti definizioni ricorsive

(Cond)X |= e (c1, X) Y (c2, X) Z

( if e then c1 else c2, X) Y ∩ Z

(While)X |= e (c,X) Y

(while edo c,X) X

(Seq)(c1, X) Y (c2, Y ) Z

(c1; c2, X) Z

Nota che il costrutto condizionale deve usare l’interesezione degli insiemi ottenuti dato che levariabili inizializzate sono tutte e sole quelle che sono inizializzate in entrambi i sotto-comandic1 e c2. Per ragioni simili nel caso del costrutto iterativo non possiamo essere sicuri di eseguirenemmeno una volta il suo corpo c, dunque non possiamo considerare inizializzate le variabili checontiene, tuttavia richiediamo che l’analisi controlli anche c.

Il risultato di questa relazione di transizione, combinata con il type-checking, è che vale ilseguente teorema: dato un programma Program (dl, c) allora

Γ(dl) ` c ∧ ∃X.(c, ∅) X ⇒ ∃σ′.〈c, σ〉 → σ′ ∨ 〈c, σ〉 ↑ .

Ovvero, se il programma è ben tipato e l’analisi dataflow termina correttamente, allora o il pro-gramma termina senza generare eccezioni, oppure non termina, sempre non generando eccezioni.In altre parole l’insieme dei programmi che non generano eccezioni sono un sottoinsieme strettodell’interesezione dell’insieme

{Program (dl, c) | Γ(dl) ` c}

con l’insieme{Program (dl, c) | ∃X.(c, ∅) X}

Implementiamo questa analisi, la prima struttura che ci interessa rappresenta un insieme.Denotiamo con 1X la funzione caratteristica dell’insieme X, ovvero

1X(x) =

{true se x ∈ Xfalse altrimenti

.

Conviene rappresentare la funzione caratteristica come segue

1X∪{x}(y) =

{true se x = y

1X(y) altrimenti.

e con la definizione di base1∅(y) =⊥ .

Possiamo implementare la funzione caratteristica di un insieme come segue.

(* funzione che costruisce un insieme vuoto , rappresentato dalla sua* funzione caratteristica *)

let empty_set = fun x -> false ;;

(* funzione che consente di aggiungere un elemento x a un insieme s *)let add_to_set x s = fun y -> if (x=y) then true else s y;;

(* funzione che calcola l’intersezione di due insiemi s1 e s2 *)let intersection s1 s2 = fun x -> s1 x && s2 x;;

L’ultima delle funzioni si definisce notando che

1X∩Y (y) = 1X(y) ∧ 1Y (y) .

Le relazioni che dobbiamo implementare faranno uso delle seguenti eccezioni.

51

(* eccezione sollevata durante la data -flow -analysis quando si* incontra in un ’espressione una variabile non inizializzata *)

exception UnboundError of ide;;

La relazione |= si implementa come segue.

(* funzione che controlla che le variabili usate in un’espressione e* siano state inizializzate , assumendo che le variabili inizializzate* siano contenute in s.* Solleva UnboundError se si incontra una variabile non inizializzata.*)

let rec check_var_exp e s =match e with

Num n -> true| Val x -> if (s x) then true else raise (UnboundError x)| (True | False) -> true| ( Add (e1,e2)

| Sub (e1,e2)| Mul (e1,e2)| Div (e1,e2)| Mod (e1,e2)| Eq (e1,e2)| Leq (e1,e2)| And (e1,e2)| Or (e1,e2))) -> check_var_exp e1 s && check_var_exp e2 s

| Not e’ -> check_var_exp e’ s;;

Mentre la relazione come segue.

(* funzione che controlla che le variabili usate in un comando c* siano state inizializzate , assumendo che le variabili inizializzate* siano contenute in s.* Solleva UnboundError se si incontra una variabile non inizializzata.*)

let rec check_var_com c s =match c with

Skip -> s| Assign (x,e) ->

if (check_var_exp e s) then add_to_set x s else empty_set| Cseq (c’::cl) ->

check_var_com (Cseq cl) (check_var_com c’ s)| Cseq [] -> s| If (e,c1,c2) ->

if (check_var_exp e s)then intersection (check_var_com c1 s) (check_var_com c2 s)else empty_set

| While (e,c’) ->if (check_var_exp e s) thenlet _ = check_var_com c’ s in selse empty_set ;;

A questo punto cosa diventa un programma con il type-checking e l’analizzatore dataflowcombinati? Intuitivamente, se scrivessimo

Γ(dl) ` c (c, ∅) c′ 〈c, σ〉 → σ′

〈Program (dl, c), σ〉 → σ′

alllora in questo caso possiamo implementare questa regola come segue

(* funzione che esegue un programma dopo aver controllato che* non contenga errori di tipo e che non vi siano variabili

52

* utilizzate senza inizializzazione.* RESTITUISCE: lo store ottenuto al termine dell ’esecuzione.* SOLLEVA: UndeclaredVar se si incontra una variabile non* dichiarata , TypeError se si incontra un errore di tipo ,* UnboundError se si usa una variabile non inizializzata*)

let sem_prog (Program (dl,c)) =if (type_check c (build_env dl))then let _ = check_var_com c empty_set in sem_com c emptystoreelse emptystore

;;

Si noti che, in pratica, associamo una semantica diversa dallo store vuoto solo se il programmanon contiene errori di tipo e soddisfa l’analisi dataflow, come atteso.

53