Una macchina di riduzione per il λ-calcolo con valutazione dei costi

Capitolo 1
Il λ-Calcolo
1.1 Note storiche
Nella logica matematica e nell’informatica, il λ-calcolo ` e un sistema for-
male realizzato per studiare la definizione di funzioni, la loro applicazione e
la ricorsione. Esso fu inventato da Alonzo Church [1] nel 1930 e, successiva-
mente, venne usato da Kleene [2] per codificare le funzioni calcolabili come
un linguaggio di programmazione astratto (esattamente come la macchina di
Turing pu` o essere considerata come il primo esempio di calcolatore astratto).
Il λ-calcolo ha una sintassi piuttosto semplice (con appena tre regole per la
costruzione dei termini) e una semantica operazionale non complicata (con
una sola operazione, la sostituzione) e, per tali ragioni esso pu` o essere usato
per studiare le propriet` a computazionali dei programmi.
Il primo contatto tra il λ-calcolo e i linguaggi di programmazione reali
avvenneintornoaglianni1956-1960,quandoMcCarthysvilupp` oillinguaggio
di programmazione LISP, ispirato al λ-calcolo e che, di fatto, rappresenta il
primoesempiodilinguaggiodiprogrammazionefunzionale[6].Tuttavial’uso
del λ-calcolo come un paradigma astratto per i linguaggi di programmazione
11
CAPITOLO 1. IL λ-CALCOLO 12
part` ı dal lavoro di tre importanti scienziati: Strachey, Landin [4] e B¨ ohm. Il
primo us` o il λ-calcolo come uno strumento descrittivo per rappresentare le
caratteristiche nei programmi ponendo, in tal modo, le basi per la creazione
diunasemanticaformaledeilinguaggidiprogrammazione[8].Landin,invece,
formalizz` o l’idea che tale semantica poteva essere tradotta in un linguaggio
di programmazione pi` u semplice da capire; egli identific` o nel λ-calcolo ta-
le linguaggio e come esperimento tradusse in quest’ultimo l’ALGOL60 [4].
Inoltre, egli dimostr` o [5] che qualunque linguaggio di programmazione non ` e
nient’altro che il λ-calcolo con l’aggiunta di “zucchero sintattico”. B¨ ohm, in-
fine, fu il primo ad usare il λ-calcolo come un linguaggio di programmazione
vero e proprio, definendo, assieme a W. Gross, il linguaggio CUCH: un misto
tra il λ-calculo e i linguaggi combinatori di Curry. B¨ ohm dimostr` o, inoltre,
come rappresentare in questo linguaggio le pi` u comuni strutture dati [3].
Esisteva, tuttavia, una differenza tra il λ-calcolo e i reali linguaggi di
programmazione funzionali; la maggior parte di questi ultimi ha una politica
di passaggio di parametri “call-by-value” (nel senso che i parametri, prima
di essere passati ad una funzione devono essere valutati), mentre la regola
di riduzione del λ-calcolo utilizza una politica “call-by-name”(nel senso che i
parametri vengono passati all’interno di una funzione senza essere valutati).
L’idea fu quella di catturare il comportamento della strategia di riduzione
call-by-value all’interno del λ-calcolo, definendo una strategia di riduzione
opportuna.Plotkin,tuttavia,dimostr` ochetalesoluzioneeraerratainquanto
ilλ-calcolo` eintrinsecamentecall-by-name[7].Pertaleragione,perdescrivere
la valutazione call-by-value, egli propose un calcolo differente, con la stessa
sintassi del λ-calcolo, ma con una differente regola di riduzione.
In questa tesi verr` a descritta una versione pi` u generale del λ-calcolo: il
λΔ-calcolo;intalelinguaggiolaregoladiriduzione` eparametricarispettoad
CAPITOLO 1. IL λ-CALCOLO 13
un sottoinsieme Δ dei termini (chiamato insieme dei valori di input). Scelte
differentidiΔcipermettonodidefinirediversilinguaggi,inparticolareledue
istanze descritte in precedenza (call-by-name e call-by-value). La caratteri-
stica principale del λΔ-calcolo ` e che, attraverso esso, ` e possibile dimostrare
propriet` a importanti per una grande classe di linguaggi. Si ritiene, infine, che
ilλΔ-calcolopossaesserevistocomelabasedeilinguaggidiprogrammazione
funzionali.
CAPITOLO 1. IL λ-CALCOLO 14
1.2 Il Linguaggio dei λ-termini
Un calcolo ` e linguaggio con in aggiunta alcune regole di riduzione. Verr` a
ora data la definizione dei λ-termini, che permettono di definire il linguaggio
del λ-calcolo.
Definizione 1.1 (Il linguaggio Λ).
Sia Var un insieme calcolabile di variabili. L’insieme Λ dei λ-termini ` e un
insieme di parole sull’alfabeto Var
S
{ (, ), ., λ} definito induttivamente
come segue:
• Se x ∈ Var allora x ∈ Λ
• Se M ∈ Λ e x ∈ Var allora λx.M ∈ Λ (Astrazione)
• Se M ∈ Λ e N ∈ Λ allora (M N) ∈ Λ (Applicazione)
´
E importante sottolineare che nella definizione della sintassi dell’appli-
cazione, i termini M ed N devono necessariamente essere separati da uno
spazio. Se si omette tale spazio, si ottengono termine errati rispetto alla
definizione proposta, come mostrato nel seguente esempio:
Esempio 1.1. Si consideri il seguente termine: (λx.x y), esso rappresenta
l’applicazione tra il termine λx.x e il termine y. Se si considera, invece, il
termine (λx.xy), ottenuto eliminando lo spazio tra le componenti dell’appli-
cazione, questo non rappresenta un termine lecito per la sintassi presentata,
poich` e manca il secondo termine dell’applicazione.
Spesso faremo riferimento ai λ-termini, chimandoli semplicemente termi-
ni. Il simbolo ≡ denota l’identit` a sintattica dei termini. Per evitare, inoltre,
l’eccessivo numero di parentesi nel caso dell’applicazione, useremo la seguen-
te abbreviazione: (MN
1
N
2
...N
n
) denoter` a (...((MN
1
)N
2
)...N
n
).
Definiamo ora il concetto di sottotermine:
CAPITOLO 1. IL λ-CALCOLO 15
Definizione 1.2 (Sottotermine).
Un termine N ` e un sottotermine di M se e solo se vale una delle seguenti
condizioni:
• M ≡ N,
• M ≡ λx.M
0
e N ` e un sottotermine di M
0
,
• M ≡ (P Q) e N ` e un sottotermine o di P o di Q.
Un termine N occorre in un termine M se e solo se N ` e un sottotermine
di M. All’interno del λ-calcolo, inoltre,` e fondamentale definire il concetto di
variabili libere:
Definizione 1.3 (Variabili libere).
L’insieme delle variabili libere di un termine M, denotato da FV(M), ` e
definito ricorsivamente come segue:
• Se M ≡ x allora FV(M) ={x},
• Se M ≡ λx.M
0
allora FV(M) = FV(M
0
)−{x},
• Se M ≡ (P Q) allora FV(M) = FV(P)∪FV(Q).
Viceversa, una variabile si definisce legata in M se non ` e libera in M.
Un termine M, inoltre, viene definito chiuso se se solo se FV(M) = ∅.
Viceversa un termine si definisce aperto e se solo se contiene almeno una
variabile legata.
La sostituzione di una variabile libera con un termine ` e l’operazione sin-
tattica di base sull’insieme Λ ed` e su di essa che si basa la regola di riduzione
(che rende il linguaggio un vero e proprio calcolo). La sostituzione, tuttavia,
CAPITOLO 1. IL λ-CALCOLO 16
deve preservare lo stato di una variabile: per esempio, x pu` o essere rimpiaz-
zata dal termine M ≡ λy.(z y) nel termine λu.(x u), ottenendo il termine
λu.(λy.(z y) u); tale sostituzione, invece, non sarebbe stata lecita nel termine
λz.(x z), poich` e nel termine ottenuto λz.(λy.(z y) z), la variable z, che in
M era libera, sarebbe diventata legata. Tale osservazione viene formalizzata
dalla seguente definizione:
Definizione 1.4. Il predicato “M ` e libera per x in N” ` e definito per indu-
zione su N:
• M ` e libera per x in x;
• M ` e libera per x in y;
• Se M ` e libera per x sia in P che Q allora M ` e libera per x in (P Q);
• Se M ` e libera per x in N e x6≡ y e y 6∈ FV(M) allora M ` e libera per
x in λy.N.
SiaM liberaperx inN; alloraN[M/x] denotala sostituzione simultanea
di tutte le occorrenze libere di x in N by M. Chiaramente,
FV(N[M/x]) =



FV(N) se x6∈ FV(N),
(FV(N)−{x})∪FV(M) altrimenti.
Ad esempio, λx.(u (x y)) [(x y)/u] non ` e definito poich` e (x y) non ` e libera
per u in λx.(u (x y)), mentre λx.(u (x u)) [(u (λz.z))/u] ≡ λx.(u λz.z (x u
λz.z)).
Nella notazione matematica standard, il nome di una variabile legata
` e senza significato; ad esempio,
P
1≤i≤n
i e
P
1≤j≤n
j denotano entrambi la
CAPITOLO 1. IL λ-CALCOLO 17
somma dei primi n numeri naturali. Anche nel linguaggio Λ ` e naturale con-
siderare i termini senza fare riferimento ai nomi delle variabile legate. Tale
osservazione viene formalizzata dalla seguente definizione:
Definizione 1.5 (α-Regola).
Dato un termine M:
1. λx.M →
α
λy.M[y/x] se y ` e libera per x in M e y 6∈ FV(M).
2. =
α
` e la chiusura riflessiva, simmetrica, transitiva e contestuale di →
α
.
Dopo aver descritto la sintassi del λ-calcolo e alcune delle sue propriet` a,
occorre definire come, di fatto, avviene il calcolo vero e proprio. L’unica
regola di computazione che il λ-calcolo offre` e la β-regola, basata sulla regola
di sostituzione definita in precedenza.
Definizione 1.6 (β-Regola).
Sia →
β
la pi` u piccola relazione su Λ tale che:
(λx.P Q) →
β
P[Q/x]
e chiusa rispetto alle seguenti regole:
• Se P →
β
P’ allora λx.P →
β
λx.P’ ∀x ∈ V
• Se P →
β
P’ allora (P Z) →
β
(P’ Z)
• Se P →
β
P’ allora (Z P) →
β
(Z P’)
Un termine della forma (λx.P Q) ` e chiamato β-redesso, mentre P[Q/x] ` e
chiamato β-contratto.
CAPITOLO 1. IL λ-CALCOLO 18
Un termine M` e in forma normale se non ha occorrenze di β-redessi (cio` e
nessun sottotermine di M ` e un β-redesso), mentre ha una forma normale
se si riduce ad un termine in forma normale.
´
E bene notare che non tutti i
termini hanno una forma normale: se, ad esempio, consideriamo i termini (D
D) e λx.(D D)(con D ≡ λx.(x x)), ` e immediato verificare che (D D) →
β
(D
D) e λx.(D D) →
β
λx.(D D).
Dalla definizione fornita della β-regola si pu` o osservare che, in presenza di
un redesso (λx.P Q), la sostituzione P[Q/x]` e indipendentemente dalla strut-
tura di Q. Questo comporta che la computazione di un tale calcolo, di fatto,
presenta una strategia di valutazione call-by-name (poich` e Q non deve essere
necessariamente valutato prima di venire sostituito all’interno dell’astrazio-
ne). Per rendere il calcolo pi` u generale, dando la possibilit` a di gestire anche
le strategie di valutazione call-by-value, ` e necessario estendere la β-regola. Il
λΔ-calcolo rappresenta una possibile soluzione all’estensione della regola di
valutazione.
CAPITOLO 1. IL λ-CALCOLO 19
1.3 Il λΔ-calcolo
Come gi` a accennato in precedenza, il λΔ-calcolo rappresenta una versio-
ne pi` u generale del λ-calcolo. Esso ` e parametrico e, in quanto tale, permette
di specificare la tipologia dei termini che possono essere passati come argo-
menti di funzioni. Di fatto il λΔ-calcolo ` e il linguaggio Λ con l’aggiunta di
un insieme Δ ⊆ Λ di valori di input che soddisfano una condizione di chiu-
sura. Informalmente, i valori di input rappresentano termini parzialmente
valutati che possono essere passati come parametri. Attraverso tale insieme` e
possibile, per esempio, scegliere una strategia di passaggio di parametri call-
by-name o una call-by-value. La maggior parte delle varianti conosciute del
λ-calcolo pu` o essere ottenuto dal λΔ-calcolo, istanziando l’insieme Δ nella
maniera opportuna. L’insieme Δ dei valori in input e la riduzione →
Δ
sono
definiti nel modo seguente:
Definizione 1.7. Sia Δ ⊆ Λ
1. La Δ riduzione (→
Δ
) ` e la chiusura contestuale della seguente regola:
(λx.M N) → M[N/x] se e solo se N ∈ Δ
(λx.M N) ` e chiamato Δ redesso (o semplicemente redesso) e M[N/x]
` e chiamato Δ contratto o semplicemente contratto
2. (→
∗
Δ
) e =
Δ
sono, rispettivamente, la chiusura riflessiva e transitiva di
→
Δ
e la chiusura riflessiva, simmetrica e transitiva di →
Δ
3. Un insieme Δ ⊆ Λ ` e detto insieme dei valori di input se vengono
soddisfatte le seguenti condizioni:
• Var ⊆ Δ
CAPITOLO 1. IL λ-CALCOLO 20
• Se P, Q ∈ Δ allora P[Q/x]∈ Δ per ogni x ∈ Var
• Se M ∈ Δ e M →
Δ
N, allora N ∈ Δ
La scelta Δ = Λ da origine al classico λ-calcolo call-by-name; se, invece,
consideriamo l’insieme Γ = Var
S
{λx.M | M ∈ Λ} e poniamo Δ = Γ, allora
otteniamo un puro (poich` e mancano le costanti) λ-calcolo call-by-value.
Nel λ-calcolo la computazione termina quando non sono pi` u presenti
redessi. Verranno considerate due strategie per la ricerca dei redessi:
• NotLazy: la ricerca dei redessi viene effettuata anche all’interno dello
scope di un λ.
• Lazy: la ricerca dei redessi non viene mai effettuata all’interno dello
scope di un λ.
Un termine senza redessi viene definito come segue:
Definizione 1.8 (Forme normali). Un termine ` e in forma normale Δ (Δ-
nf)senonhaΔ-redessi,mentrehaunaformanormaleΔ,o` e Δ-normalizzabile
se si riduce ad una forma normale Δ; l’insieme delle Δ-nf ` e indicato Δ-NF.
La struttura di un termine in forma normale ` e in funzione dell’insieme di
input Δ e della strategia di valutazione, come illustrato di seguito:
• Δ = Λ con Strategia Not-Lazy (Λ-nf)
– Un termine M ` e in forma normale se ha la seguente struttura:
x | λx
1
... λx
n
.N con N ∈ Λ-NF | (x M
1
... M
m
) con M
i
∈ Λ-NF
– Un termine M ` e in forma normale di testa (Λ-hnf) se presenta la
seguente struttura:
x | λx
1
... λx
n
.(y M
1
... M
m
) con M
i
∈ Λ
CAPITOLO 1. IL λ-CALCOLO 21
• Δ = Λ con Strategia Lazy (ΛL-nf)
Un termine M ` e in forma normale se presenta la seguente struttura:
x | (x M
1
... M
m
) con M
i
∈ ΛL-NF | λx.P con P ∈ Λ
• Δ = Γ con Strategia Not-Lazy (Γ-nf)
Un termine M ` e in forma normale se presenta la seguente struttura:
x | λx
1
... x
m
.N con N ∈ Γ-NF | (x M
1
... M
m
) con M
i
∈ Γ-NF |
(λx.P Q M
1
... M
m
) con P, Q, M
i
∈ Γ-NF e Q / ∈ Γ
• Δ = Γ con Strategia Lazy (ΓL-nf)
Un termine M ` e in forma normale se presenta la seguente struttura:
x | λx
1
... x
n
.N | (λx.P Q M
1
... M
m
) con P, Q, M
i
∈ ΓL-NF e Q / ∈ Γ
Definizione1.9. Untermine` e Δ-fortementenormalizzabilese` eΔ-normalizzabile
e non esiste una sequenza infinita di Δ-riduzioni che partono da esso.
´
E facile verificare che ogni termine ha la seguente forma:
λx
1
...x
n
.ζM
1
...M
m
(n, m ≥ 0)
dove i vari M
i
rappresentano gli argomenti di M (1 ≤ i ≤ m) e ζ viene
definita testa di M. Quest’ultima pu` o essere o una variabile (variabile di
testa)oun’applicazionedellaforma(λz.PQ),laquale,asuavoltapu` oessere
o un redesso (redesso di testa) o meno, a seconda del fatto se Q appartiene
o no all’insieme Δ. A seconda dell’insieme dei valori di input Δ presi in
considerazione, pu` o variare la struttura delle forme normali.
Esempio 1.2. Consideriamo il seguente λ-termine: (λx.x (y z)). Se sce-
gliamo Δ = Γ il termine ha la seguente forma normale: (λx.x (y z)). Se
consideriamo, invece, Δ = Λ il termine ha come forma normale: (y z).
CAPITOLO 1. IL λ-CALCOLO 22
La naturale interpretazione di un termine della forma λx.M (astrazione)
` e di considerarlo come una funzione il cui parametro formale ` e x. Il termine,
invece, dalla forma (λx.M N) (applicazione), con N ∈ Δ pu` o essere visto
comel’applicazionedellafunzioneλx.M alparametroattualeN;intalmodo,
la regola di riduzione modella la sostituzione del parametro formale x con
il parametro attuale N all’interno del corpo della funzione M. Inoltre, la
Δ-nf, se esiste, pu` o essere a sua volta vista come il risultato finale di una
computazione.
´
E bene sottolineare che il λ-calcolo, di fatto, ` e un linguaggio
di ordine superiore, poich` e gli argomenti e i risultati delle funzioni sono loro
stessi ancora delle funzioni.
Il seguente teorema, del quale non verr` a fornita la dimostrazione, mostra
cometaleinterpretazionedelλΔ-calcolosiaesatta;daesso,infatti,pu` oessere
ricavata la considerazione che se il processo di computazione termina, allora
il risultato di tale computazione ` e unico.
Teorema 1.1 (Confluenza). Se M →
∗
Δ
N
1
e M →
∗
Δ
N
2
, allora esiste Q tale
che N
1
→
∗
Δ
Q e N
2
→
∗
Δ
Q.
Il teorema porta ad un importante corollario:
Corollario 1.1. La forma normale Δ di un termine, se esiste, ` e unica.
Supponiamo che M →
∗
Δ
N e supponiamo che esistano pi` u di una sequen-
za di Δ-riduzioni da M ad N. Il teorema di standardizzazione afferma che,
nel caso l’insieme dei valori di input rispetta una particolare propriet` a, esi-
ste sempre la possibilit` a di raggiungere N da M, riducendo i redessi in un
determinato ordine.
La sequenza di riduzione standard pu` o essere formalizzata nel seguente
modo:
CAPITOLO 1. IL λ-CALCOLO 23
Definizione 1.10.
1. Un simbolo λ in un termine M ` e attivo se e solo se ` e il primo simbolo
che compare in un Δ-redesso
2. La Δ-sequenzializzazione (M)
◦
di un termine M ` e una funzione da Λ
in Λ definita come segue:
• (x M
1
... M
m
)
◦
= x (M
1
)
◦
... (M
m
)
◦
• (λx.P Q M
1
... M
m
)
◦
= (λx.P)
◦
(Q)
◦
(M
1
)
◦
... (M
m
)
◦
, se Q ∈ Δ
• (λx.P Q M
1
... M
m
)
◦
= (Q)
◦
(λx.P)
◦
(M
1
)
◦
... (M
m
)
◦
, se Q / ∈ Δ
• (λx.P)
◦
= λx.(P)
◦
3. Il grado di un redesso R in M` e il numero di λ attivi in M che occorrono
alla sinistra di (R)
◦
in (M)
◦
4. Il redesso principale di un termine M, se esiste, ` e il redesso di grado
minimo. La riduzione principale M →
p
Δ
N denota che N ` e ottenuto
da M riducendo il redesso principale in M. Inoltre, →
∗p
Δ
` e la chiusura
riflessiva e transitiva di →
p
Δ
5. Una sequenza M ≡ P
0
→
Δ
P
1
→
Δ
... →
Δ
N ` e standard se e solo se il
grado del redesso contratto in P
i
` e minore o uguale al grado del redesso
contratto in P
i+1
, per ogni i < n
Esempio 1.3 (Riduzioni standard).
1. Sia Δ = Λ, e sia M ≡ (λx.(x (K I)) (I I)). Cos` ı M ha grado 0, (K I)
ha grado 1 e (I I) ha grado 2 nel termine M. La seguente sequenza di
riduzione ` e standard:
(λx.(x (K I)) (I I)) →
Λ
((I I) (K I)) →
Λ
(I (K I)) →
Λ
(I λy.I)
CAPITOLO 1. IL λ-CALCOLO 24
2. Sia M definito come in precedenza, e Δ = Γ. Cos` ı (I I) ha grado 0 e,
(K I) ha grado 1. E’ da notare che adesso M non ` e pi` u un redesso. La
seguente sequenza di riduzione ` e standard:
(λx.(x (K I)) (I I)) →
Γ
(λx.(x (K I)) I) →
Γ
(I (K I)) →
Γ
(I λy.I) →
Γ
λy.I
´
E importante notare che il grado di un redesso pu` o cambiare durante la
riduzione; in particolare, il redesso di grado minimo ha sempre grado zero.
Inoltre,lesequenzediriduzionedigrado0e1sonosemprestandard.
´
Efacile
verificareche,perogniM,laΛ-sequenzializzazione` e(M)
◦
≡M;inquesticasi
il redesso di grado 0 ` e sempre quello che compare pi` u a sinistra.
La nozione di insieme di valori standard di input ` e data nella definizione
successiva, ed ` e la chiave per ottenere la propriet` a di standardizzazione.
Definizione 1.11 (Valori di input standard).
Un insieme Δ di valori di input ` e standard se e solo se M / ∈ Δ e M →
∗
Δ
N
non riducendo ad ogni passo il redesso principale, questo implica N / ∈ Δ.
A questo punto ` e possibile enunciare il teorema di Standardizzazione:
Teorema1.2(Standardizzazione). M →
∗
Δ
N seesoloseesisteunasequenza
di riduzione standard M ≡ M
1
→
Δ
M
2
→
Δ
... →
Δ
M
n
≡ N (n ≥ 0)
Teorema 1.3.
Condizione necessaria e sufficiente affinch` e il ΛΔ-calcolo abbia la propriet` a
di standardizzazione ` e che Δ sia standard.
Dimostrazione.
La condizione di sufficienza ` e una conseguenza del Teorema di Standardiz-
zazione. Per dimostrare la necessariet` a, assumiamo che Δ non sia standard;
possiamo trovare un termine M / ∈ Δ tale che M →
∗
Δ
N ∈ Δ, senza ridurre il