Corrispondenza di Curry-Howard

Università degli Studi Roma Tre
Facoltà SMFN, Dipartimento di Matematica
Tesi di Laurea Magistrale
Corrispondenza di
Curry-Howard:
dal λ-calcolo tipato semplice al
λ-calcolo infinitario
3 maggio 2014
Candidata:
Cecilia Fiorese
[email protected]
.....................................
Relatori:
Prof. Vito Michele Abrusci
Prof. Marco Pedicini
.....................................
.....................................
Indice
1 Introduzione
1.1 Logica intuizionista . . . . . . .
1.2 Deduzione naturale . . . . . . .
1.3 λ-calcolo . . . . . . . . . . . . .
1.3.1 λ-calcolo puro . . . . . .
1.3.2 λ-calcolo tipato semplice
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
3
4
5
10
10
15
2 Corrispondenza di Curry-Howard
2.1 Assioma . . . . . . . . . . . . . .
2.2 Congiunzione moltiplicativa . . .
2.3 Disgiunzione moltiplicativa . . . .
2.4 Congiunzione additiva . . . . . .
2.5 Disgiunzione additiva . . . . . . .
2.6 Indebolimento . . . . . . . . . . .
2.7 Contrazione . . . . . . . . . . . .
2.8 Taglio . . . . . . . . . . . . . . .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
18
19
19
21
24
26
29
30
31
.
.
.
.
.
.
.
33
33
33
34
35
36
36
38
3 Altri sistemi di calcolo tipato
3.1 Il sistema T . . . . . . . . . . . . . . . .
3.1.1 Sintassi e calcolo . . . . . . . . .
3.1.2 Potere espressivo . . . . . . . . .
3.2 Il Sistema F . . . . . . . . . . . . . . . .
3.2.1 Sintassi e calcolo . . . . . . . . .
3.2.2 Rappresentazione dei tipi semplici
3.2.3 Strutture libere . . . . . . . . . .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
4 Teoremi di normalizzazione
42
4.1 Riducibilità e normalizzazione nel λ-calcolo tipato semplice . . 42
4.2 Riducibilità e normalizzazione nel sistema F . . . . . . . . . . 45
1
INDICE
5 λ-calcolo infinitario e ludica computazionale
5.1 Un λ-calcolo poliadico infinitario Λ8 . . . . .
5.1.1 Topologia sui λ-termini . . . . . . . . .
5.1.2 Sottocalcolo affine . . . . . . . . . . . .
5.1.3 Uniformità e isomorfismo con il lambda
5.2 Ludica computazionale e termini infinitari . .
5.3 Derivazioni in MELLP e termini di Λ8 . . .
2
. . . . .
. . . . .
. . . . .
calcolo
. . . . .
. . . . .
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
.
48
48
50
55
56
58
63
6 Il λ-calcolo infinitario è elementare
68
6.1 Logica lineare elementare . . . . . . . . . . . . . . . . . . . . . 68
6.2 λ-calcolo infinitario lineare . . . . . . . . . . . . . . . . . . . . 71
A Spazi Metrici
78
B Spazi Topologici
81
C Topologia di Scott
84
Capitolo 1
Introduzione
La corrispondenza di Curry-Howard fu formulata per la prima volta da William Alvin Howard nel 1980 [15] sulla base del lavoro di Haskell Brooks
Curry [7]. Essa fa uso del λ-calcolo tipato, uno dei più comuni sistemi formali per la rappresentazione dei programmi a partire da dimostrazioni logiche.
Il paradigma proofs-as-programs sviluppato da Howard costituisce dunque
un notevole caso di interazione tra due discipline scientifiche: la logica e l’informatica.
Il λ-calcolo fu introdotto dal matematico Alonzo Church nel 1932 [5], con
l’obiettivo di analizzare formalmente le funzioni e il loro calcolo. Le prime
sono espresse per mezzo di un linguaggio formale, che stabilisce quali siano
le regole per formare un termine, e il calcolo dà un sistema di riscrittura,
mostrando come i termini possano essere ridotti e semplificati.
La combinazione di semplicità ed espressività ha reso il λ-calcolo uno strumento frequente in diversi campi scientifici. Un λ-termine può essere considerato come un programma, e la sua riduzione (ovvero il calcolo effettuabile
a partire da esso) l’esecuzione del programma. Da un lato, esso costituisce un
modello semplice ed elegante della nozione di calcolabilità, dall’altro mostra
come vengono calcolati i valori di una funzione, senza passare per il modello della macchina di Turing. Quest’ultimo aspetto lo rende interessante dal
punto di vista informatico: tutti i linguaggi di programmazione funzionale
hanno un nucleo costituito dal λ-calcolo (o una qualche sua versione). Anche il λ-calcolo tipato fu sviluppato grazie al contributo di Church, che nel
1940 [6] introdusse il tipaggio semplice a partire dal quale furono derivati in
seguito diversi approcci di tipizzazione del linguaggio, tra cui il sistema F che
permette la rappresentazione delle dimostrazioni della logica proposizionale
intuizionista del secondo ordine.
3
CAPITOLO 1. INTRODUZIONE
1.1
4
Logica intuizionista
A partire dal λ-calcolo puro si può costruire quello tipato mediante due principali tipi di approccio, uno di Church l’altro di Curry, che si differenziano
per la costruzione dei tipi in relazione con i termini del calcolo.
Dall’esigenza di costruire un sistema formale che permette di studiare gli oggetti funzionali nascosti dietro le dimostrazioni logiche, la corrispondenza di
Curry-Howard stabilisce una relazione tra tipi e proposizioni, tra dimostrazioni e programmi, tra eliminazione dei tagli ed esecuzioni dei programmi. In
particolare induce un isomorfismo tra due punti di vista: la deduzione naturale, vista come modello delle dimostrazioni logiche e delle loro trasformazioni,
e il λ-calcolo tipato, come modello dei programmi e del calcolo.
Viene introdotto il concetto di tipo di oggetto. Ogni formula logica è
un tipo di oggetto e per le dimostrazioni si ha la corrispondenza:
• π dimostrazione di A ù oggetto di tipo A
• π dimostrazione di A da A1 , . . . , An ù oggetto di tipo programma di
input A1 , . . . , An e output A
• π dimostrazione con cut ù programma da eseguire
• π dimostrazione cut-free ù programma eseguito
• riduzione di una dimostrazione π a una dimostrazione cut-free
ù esecuzione del programma π
Ogni passo di riduzione di un λ-termine rappresenta un passo di esecuzione
del programma ad esso correlato. Non tutti i programmi però hanno la
proprietà che ogni loro esecuzione termini, il λ-calcolo tipato serve a isolare
i programmi che terminano sempre la propria esecuzione. Tali programmi
sono associati ai termini che possono essere normalizzati.
La corrispondenza di Curry-Howard nasce e si sviluppa in un’ottica intuizionista. Mentre nella logica classica le dimostrazioni possono avere diverse
letture, ovvero a seconda delle ipotesi usate si sviluppa poi la dimostrazione
relativa al contesto scelto, dall’altra parte la logica intuizionista ha una visione della dimostrazione come esecuzione di un programma attraverso una
macchina, quindi con fissati input (ipotesi) e un unico output (tesi). Si ha
quindi che nella logica classica tutte le dimostrazioni di una data formula A
vengono identificate come la stessa dimostrazione, cioè dimostrazioni diverse
della stessa formula sono tra loro equivalenti, la logica intuizionista mette
invece in luce la pluralità delle dimostrazioni, ognuna delle quali rappresenta
un programma che permette di ottenere come output sempre la formula A.
CAPITOLO 1. INTRODUZIONE
5
Il limite principale di questa visione è certamente la necessità di avere un
output unico. Da questa esigenza seguono varie modificazioni o restrizioni
delle regole del calcolo dei seguenti (LK).
1.2
Deduzione naturale
La deduzione naturale [9] si sviluppa dall’idea di visualizzare una dimostrazione graficamente attraverso un albero, con zero o più ipotesi e un’unica
conclusione.
Notazione: Si usa
..
.
A
per indicare una deduzione di A.
Una deduzione naturale di A indica una dimostrazione con conclusione A.
Ogni deduzione di A è rappresentata da un albero finito le cui foglie sono
etichettate dalla formula coinvolta nel passo di dimostrazione.
Le foglie possono avere due tipi di interpretazione: una foglia si dice viva
se la foglia è una formula con una parte attiva nella dimostrazione, ovvero
è un’ipotesi; si dice morta (e si cancella con una barra nell’albero) se la
formula non svolge più alcun ruolo nella dimostrazione.
La costruzione dell’albero si basa su regole di introduzione e di eliminazione
dei connettivi, le prime mostrano la nascita del connettivo, le altre il suo uso.
Regole di introduzione:
..
.
A
A^B
..
.
B
p^iq
A
..
.
B
AÑB
..
.
A
A_B
pÑ iq
p_1iq
CAPITOLO 1. INTRODUZIONE
6
..
.
B
p_2iq
A_B
pDiq
A[a/ ξ]
DξA
..
.
A
@ξA
p@iq
con ξ non libera sia in A che in tutte le ipotesi presenti nella deduzione
di A.
Regole di eliminazione:
..
.
A^B
A
p^1q
..
.
A^B
B
..
.
A
p^2q
..
.
AÑB
B
..
.
A_B
pÑ q
A
..
.
B
..
.
C
C
C
A
..
.
DξA
C
C
pDq
p_q
CAPITOLO 1. INTRODUZIONE
7
..
.
@ξA
Ara{ξ s
p@q
Una regola si dice globale se è una regola della deduzione naturale in
cui si hanno condizioni globali sulle premesse, si fa particolare attenzione
alle ipotesi coinvolte precedententemente rispetto a quelle che concludono la
formula finale della dimostrazione. Regole globali sono, per esempio, pÑ iq,
p_q, pDq in cui le premesse sono una o più deduzioni; p@iq ha una globalità
ancora più forte che si riconduce al fatto che la variabile ξ deve essere libera non solo localmente in A ma globalmente in tutta la deduzione, in tutte
le ipotesi coinvolte. Le regole che non sono globali si dicono locali, ovvero
hanno come ipotesi solo formule. Le regole p^iq, pÑ q ma anche quelle di
introduzione per la congiunzione e di eliminazione per la disgiunzione sono
regole locali.
Osservazioni:
• Le regole di introduzione si rifanno alla struttura già conosciuta delle
regole del calcolo dei seguenti. Si presenta una regola per ogni connettivo a parte per la disgiunzione, difatti si può concludere A _ B
dimostrando solo A o solo B.
• Le regole di eliminazione presentano in alcuni casi una formula ausiliaria C. Tale formula ha un ruolo parassitario e non è strutturalmente
legata a nessuna formula presente, nel calcolo dei seguenti è una formula
del contesto. È chiaro tale ruolo per esempio nella regole di eliminazione della disgiunzione: sapendo che è vero A _ B, non si può concludere
nulla sulle formule coinvolte, a meno che non esista una deduzione naturale sia da A che da B con conclusione C e dunque da A _ B si
ottiene C.
• Nella deduzione naturale, il connettivo principale è l’implicazione, perchè
permette di dare il concetto intuitivo di programma, ma soprattutto
perchè sostituisce la dualità: infatti non esistono più formule negate,
dal momento che diventano ipotesi della deduzione dopo essere state trasformate nella loro formulazione positiva. Per esempio se nel
calcolo dei seguenti si ha, come contesto o conclusione del seguente,
$ A, B, nella deduzione naturale la formula A diventa ipotesi/input
dell’implicazione, ovvero A Ñ B.
CAPITOLO 1. INTRODUZIONE
8
Si definisce deduzione normale una deduzione naturale senza cut. I
cut per la deduzione naturale sono formati da due regole che si susseguono
una di introduzione e una di eliminazione, entrambe dello stesso connettivo.
Ovvero del tipo:
i
C Per il teorema di eliminazione del taglio, data una deduzione è sempre
possibile ottenere, tramite operazioni di conversione, un’unica deduzione normale, la cui esistenza e unicità sono garantite dal teorema di Church-Rosser
Teorema 1.8. Infatti ogni deduzione naturale corrisponde a un termine del
λ-calcolo e ridurre un taglio risulterà nient’altro che eseguire un redesso; si
dimostrerà che, dopo un numero finito di passi di riduzione di questo tipo,
si ottiene sempre la forma normale di un λ-termine.
Esempi:
1.
.
1..
A
A^B
B
.
2..
B
p^iq
p^2q
..
si riduce a 2.
B
.
1..
A
2.
A_B
p_iq
A
.
2..
B
.
3..
C
C
C
p_q
.
1..
A
si riduce a .
2..
C
Le conversioni della deduzione naturale mettono inoltre in luce la commutatività delle regole p_q e pDq:
CAPITOLO 1. INTRODUZIONE
• Commutatività di
9
p_q con una qualsiasi regola prq:
A
..
.
B
..
.
C
C
..
.
A_B
p_q
C
..
. prq
D
Ó
A
..
.
C
..
.
..
.
C
prq
D
A_B
B
..
.
..
.
D
D
• Commutatività di
pDq con una qualsiasi regola prq:
A
..
.
..
.
DξA
C
pDq
C
..
. prq
D
Ó
A
..
.
..
.
C
..
.
DξA
D
D
prq
pDq
prq
p_q
CAPITOLO 1. INTRODUZIONE
1.3
10
λ-calcolo
In questa sezione si introduce il λ-calcolo puro e quello tipato [17] [9].
In generale il λ-calcolo è un calcolo formale, sviluppato per rappresentare le
funzioni e il sistema deduttivo sui numeri naturali. Le funzioni sui numeri
naturali possono essere rappresentate da funzioni ricorsive o tramite macchine di Turing. Con il λ-calcolo si fondono queste due visioni: da una parte è
un calcolo di funzioni, in cui i simboli @ e λ rappresentano rispettivamente la
composizione di funzioni e il passaggio di parametri; dall’altra è un calcolo di
sostituzioni. Il λ-calcolo permette quindi di rappresentare le funzioni come
fosse un linguaggio di programmazione.
1.3.1
λ-calcolo puro
I termini del λ-calcolo, detti λ-termini, sono sequenze finite di simboli formate
da variabili x, y, . . ., parentesi e dal simbolo λ.
Definizione 1.1 (Termini) I termini del λ-calcolo puro si costruiscono in
modo induttivo:
- variabile: sia V l’insieme delle variabili, ogni variabile x, y, z . . . P V è
un λ-termine;
- astrazione: se t è un λ-termine, allora λx.t è un λ-termine, t è detto
suo sottotermine;
- applicazione: se t, u sono λ-termini, allora ptqu è un λ-termine, t e u
sono detti suoi sottotermini.
In breve, si usa la notazione:
t : x, y . . .
|
λx.t
| ptqu
Il simbolo λ è detto astrazione in quanto cattura le variabili, ovvero indica
le variabili del termine le cui occorrenze vengono sostituite nel calcolo. Il
termine ptqu è detto applicazione e rappresenta la composizione del termine
t con il termine u.
Definizione 1.2 (Variabili libere e legate) Le occorrenze delle variabili
di un termine t che seguono il simbolo λ si dicono variabili legate, mentre
ulteriori occorrenze di variabili presenti nel termine si dicono variabili libere. In particolare, le occorrenze libere di una variabile x in un termine t si
definiscono per induzione:
CAPITOLO 1. INTRODUZIONE
11
se t x, allora l’occorrenza di x è libera;
se t puqv, allora le occorrenze libere di x in t sono quelle di x in u e v;
se t λy.u, le occorrenze libere di x in t sono quelle di x in u a meno che
x y, in quel caso nessuna occorrenza di x in t è libera.
Un termine che non ha varibili libere si dice chiuso.
Si indicano con F v ptq e Bv ptq rispettivamente gli insiemi delle variabili libere
e legate di un termine t.
Esempio: Nello stesso termine è possibile che la stessa variabile abbia sia
occorrenze libere che legate. Prendendo per esempio il termine
t pxqλx.x
si ha che
F v ptq F v ppxqq
Bv ptq Bv ppxqq
”
”
F v pλx.xq txu H txu
”
”
Bv pλx.xq H
txu txu
Si noti che apparentemente F v ptq e Bv ptq sono lo stesso insieme, ma
in realtà si distinguono in quanto la variabile x che appare non è la
stessa: quella in F v ptq è la prima occorrenza di x in t, mentre quella
in Bv ptq è la seconda. Dunque la variabile x nel termine t è sia libera
che legata, in quanto ha un’occorrenza libera e una legata.
Definizione 1.3 (Sostituzione) Siano t, u temini e x una variabile. Si definisce il termine tru{xs come il termine che risulta sostituendo le occorrenze
libere di x in t con u. Più precisamente, si definisce la sostituzione in un
termine t per induzione strutturale come segue:
se t y,
tru{xs "
u se x y
y se x y
se t pv1 qv2 ,
tru{xs pv1 ru{xsqv2 ru{xs
se t λy.v,
tru{xs "
λz.v ru{x, z {y s se z R F v ptq e x y
t
altrimenti
con v ru{x, z {y s si intende una sostituzione simultanea delle x con u e delle
y con z.
CAPITOLO 1. INTRODUZIONE
12
Si introduce sui λ-termini una relazione di equivalenza, che identifica i termini
che si distinguono solo per il nome delle variabili, ovvero termini per cui
esistono una o più sostituzioni per cui risultano lo stesso termine.
Definizione 1.4 (α-equivalenza) Dati due termini t, t1 si definisce la relazione α per induzione strutturale:
se t x, allora t α t1 se e solo se t1 è una variabile e a meno di sostituzioni
risulta t t1 ;
se t puqv, allora t α t1 se e solo se t1
pu1qv1 con u α u1 e v α v1;
se t λx.u, allora t α t1 se e solo se t1 λx1 .u1 , con ury {xs u1 ry {x1 s per
ogni varibile y x, x1 .
Se t α t1 , t e t1 si dicono α-equivalenti.
Esempio: Il termine λy.xy è α-equivalente al termine λx.yx. Infatti, λy.xy ru{x, z {y s λy.yxru{y, z {xs λz.uz .
Il calcolo di un λ-temine si costruisce tramite l’operazione di riduzione.
Definizione 1.5 (β-riduzione) Si definisce la β-riduzione:
pλx.tqu Ñβ tru{xs
ovvero la trasformazione che, individuata l’applicazione λx.t al parametro u,
costruisce un nuovo λ-termine tru{xs sostituendo in t ogni occorrenza della
variabile legata x con il termine u.
pλx.tqu si dice redesso, tru{xs contratto.
Un termine t si dice riducibile se almeno uno dei suoi sottotermini può essere
ancora ridotto.
Esempio: Il termine pλx.xy q applicato al termine u
nel modo seguente:
λz.zpyq si β-riduce
pλx.xyqt Ñβ pxyqrt{xs ty λz.zpyqy
Un termine u si riduce a un termine v quando esiste una sequenza di βriduzioni da u a v
u t0 , t1 , . . . , tn1 , tn v
tali che per ogni i 0, 1, 2, . . . , n 1, ti 1 è ottenuto da ti sostituendo un
redesso con il suo contratto. Si scrive che u Ñ v, indicando il fatto che per
ottenere v sono stati eseguiti più di un passo di β-riduzione. In particolare,
Ñ è la chiusura riflessiva e transitiva di Ñβ e u, v si dicono β-equivalenti
CAPITOLO 1. INTRODUZIONE
13
Definizione 1.6 (Termine normale) Un termine t si dice normale se nessuno dei suoi sottotermini può essere ridotto.
Definizione 1.7 (Forma normale) Una forma normale per un termine t
è un termine u tale che t Ñ u e u è normale.
La proprietà più significativa della β-riduzione è sicuramente quella detta di
Church-Rosser, che garantisce l’unicità della forma normale e la confluenza
del λ-calcolo. Tale proprietà segue teorema 1.8.
Teorema 1.8 (Church-Rosser) La riduzione del λ-calcolo è confluente,
ovvero:
se t Ñ u e t Ñ v allora esiste w tale che u Ñ w e v
u
t
Ñ w.
v
w
Figura 1.1: Diagramma di confluenza
Immediata conseguenza della proprietà di Church-Rosser è l’unicità della
forma normale.
Corollario 1.9 Sia t un termine, se t ammette una forma normale, questa
è unica.
Dimostrazione:
Se t Ñ u e t Ñ v con u, v due forme normali per t, allora per il
teorema di Church-Rosser esiste un termine w tale che u Ñ w e
v Ñ w per qualche w. Avendo supposto che u, v sono in forma normale, si ha che i due termini non possono essere ridotti ulteriormente,
quindi deve essere u v. CAPITOLO 1. INTRODUZIONE
14
Per ottenere la forma normale di un termine t, non esiste un modo unico. Si
può procedere con la riduzione del termine usando vari approcci. Si introduce
il concetto di strategia normalizzante. Dato un termine t, ogni strategia
normalizzante per t produce una differente sequenza di riduzione, ovvero
una sequenza di termini t0 Ñβ t1 Ñβ . . . Ñβ tn , tale che t0 t, ogni ti è
ottenuto riducendo il termine precedente e tn è la forma normale di t. Per
ogni termine t si cerca la strategia ottimale che permette di ridurre il più
possibile la sequenza di riduzione del termine.
Una delle strategie più note che spesso risulta ottimale è la β-riduzione sinistra: dato un termine non normale t la riduzione procede riducendo di volta
in volta il redesso più a sinistra nel termine.
Proposizione 1.10 Ogni termine del λ-calcolo può essere scritto, in un
unico modo, nella forma
λx1 .λx2 . . . . λxn .pv qu1 u2 . . . um
dove x1 , x2 , . . . , xn sono variabili, v o una variabile o un redesso e u1 , . . . , um
termini.
Se v λx.u, il redesso pλx.uqt è detto redesso di testa.
Definizione 1.11 (Forma normale di testa) Una forma normale di testa per un termine t è un termine della forma
λx1 .λx2 . . . . λxn .py qu1 u2 . . . um
dove y è una della xi o un’ulteriore variabile e gli uj sono termini.
Definizione 1.12 (Termine risolubile) Un λ-termine t è detto risolubile
se, per ogni termine u, esistono variabili x1 , . . . , xk e termini u1 , . . . , uk , v1 , . . . , vl
tali che
ptru1{x1, . . . , uk {xk sqv1 . . . vl Ñβ u
Si hanno anche le seguenti definizioni equivalenti:
t è risolubile se e solo se esistono variabili x1 , . . . , xk e termini u1 , . . . , uk , v1 , . . . , vl
tali che ptru1 {x1 , . . . , uk {xk sqv1 . . . vl Ñβ I : λx.x;
t è risolubile se e solo se, data una variabile x che non occorre in t, esistono
termini u1 , . . . , uk , v1 , . . . , vl tali che ptru1 {x1 , . . . , uk {xk sqv1 . . . vl Ñβ x.
Lemma 1.13 Per ogni λ-termine t, le seguenti condizioni sono equivalenti
1. t è risolubile;
CAPITOLO 1. INTRODUZIONE
15
2. t è β-equivalente ad una forma normale di testa;
3. la riduzione di testa di t termina con una forma normale di testa.
Con riduzione di testa si intende la riduzione che procede riducendo progressivamente il redesso di testa del termine.
Definizione 1.14 (Normalizzabile) Un termine t si dice normalizzabile
se esiste una sequenza di riduzioni per t di lunghezza finita, altrimenti si dice
non normalizzabile.
Esempio: Non tutti i termini del λ-calcolo puro sono normalizzabili. Per
esempio, il termine Ω pλx.xxqλx.xx si riduce a se stesso, produce
cioè una sequenza di riduzioni infinita. Quello che principalmente causa
questo loop è il fatto che il termine Ω non è altro che risultato di un
termine, ∆ λx.xx, applicato a se stesso.
Definizione 1.15 (Fortemente normalizzabile) Un termine t si dice fortemente normalizzabile se tutte le sequenze di riduzioni hanno lunghezza
finita.
Osservazione: Un termine fortemente normalizzabile è banalmente anche
normalizzabile.
Esempio: Il termine λf x.f pf pf xqqqpλx.xqλxy.y Ñ λxy.y è fortemente normalizzabile, si riduce infatti alla forma normale indipendentemente dalla strategia usata.
Il termine pλxy.y qΩλf x.f pf xq Ñ λf x.f pf xq con una riduzione di testa, ma se si inizia dalla riduzione di Ω si ottiene, come si è visto, una
sequenza infinita di riduzioni, il termine è perciò normalizzabile ma non
fortemente.
Lemma 1.16 Un termine t è fortemente normalizzabile se e solo se esiste
un numero ν ptq che limita la lunghezza di ogni sequenza di riduzione di t.
1.3.2
λ-calcolo tipato semplice
Tramite la corrispondenza di Curry-Howard ad ogni dimostrazione può essere
associato un programma: ogni formula A è considerata un tipo e ogni sua
dimostrazione è di tipo A.
Definizione 1.17 (Tipi) Data una formula A, si definisce il tipo A. I tipi
sono definiti induttivamente, come per le formule, nel modo seguente:
CAPITOLO 1. INTRODUZIONE
16
1. i tipi atomici T1 , . . . , Tn sono tipi
2. se U e V sono tipi, allora U xV e U
ÑV
sono tipi
3. gli unici tipi si ottengono da 1 e 2
Definizione 1.18 (Termini) I termini del λ-calcolo tipato, come in quello
puro, sono costruiti in modo induttivo:
- Le variabili xT , y T , z T . . . sono termini di tipo T .
Spesso indicati anche con x : T, y : T, z : T . . ..
- Se u e v sono termini rispettivamente di tipo U e V allora xu, v y è un
termine di tipo U ^ V . u e v sono sottotermini di xu, v y.
La coppia ordinata di u e v viene rappresentata con xu, v y.
- Se t è un termine di tipo U xV allora π 1 t e π 2 t sono rispettivamente
termini di tipo U e V , t è sottotermine di entrambi.
I due termini π 1 t e π 2 t rappresentano le proiezioni di t.
- Se v è un termine di tipo V e xU è una variabile di tipo U allora λxU .v
è un termine di tipo U Ñ V , v è un suo sottotermine.
λxU .v rappresenta una funzione che ad ogni u di tipo U associa il
termine v ru{xs.
- Se t e u sono termini rispettivamente di tipo U Ñ V e U allora ptqu è
un termine di tipo V , con t e u suoi sottotermini.
ptqu rappresenta analogamente al λ-calcolo puro l’applicazione.
Osservazione: Nel λ-calcolo puro si defisce quindi una lista infinita di variabili, mentre il λ-calcolo tipato permette di avere una lista infinita di variabili
per ogni tipo. Il λ-calcolo tipato risulta essere quindi più ricco e anche più
corretto, in quanto non c’è ambiguità nel tipo di input da considerare e il
tipo di output che si ottiene. Dato per esempio un λ termine py qx dove y è
l’implicazione:
nel λ-calcolo puro di Church: y può essere tipato come y : A Ñ B che
applicato a un termine x : A si ha py qx : B, ma anche come y : C Ñ D
con x : C e quindi si ottiene py qx : D e cosı̀ via.
nel λ-calcolo tipato di Curry-Howard: si parte dal λ-termine y di tipo
programma A Ñ B e x : A ottenendo cosı̀ py qx : B senza alcuna
ambiguità.
CAPITOLO 1. INTRODUZIONE
17
Ogni termine rappresenta un programma e il tipo di un programma indica
la sua specifica, ovvero i valori di input e di output.
Analogamente al λ-calcolo puro, per il λ-calcolo tipato si definisce la
riduzione e la forma normale.
Definizione 1.19 (Riduzione) Un termine t si riduce a un termine t1 ,
t ; t1 , nel modo seguente:
π 1 xu, v y ; u
π 2 xu, v y ; v
pλxU .vqu ; vru{xs
il primo termine si dice redesso, quello ottenuto dopo la riduzione si dice
contratto.
; è la chiusura riflessiva e transitiva di ; e indica più passi di riduzione.
Osservazione: Il redesso e il contratto sono sempre dello stesso tipo. Ad
esempio, se u : U e v : V , π 1 xu, v y : U si riduce a u : U .
Definizione 1.20 (Forma Normale) Un termine t è normale se nessuno
dei suoi sottotermini è in una delle seguenti forme:
π 1 xu, v y
π 2 xu, v y
pλxU .vqu
Un termine t ha una forma normale u se esiste una successione di riduzioni
t t0 ; t1 ; . . . ; tn u, ovvero t ; u, tale che u è un termine normale.
Il λ-calcolo tipato è anch’esso un calcolo confluente in quanto soddisfa il teorema 1.8.
A differenza del λ-calcolo puro, nel calcolo semplicemente tipato tutti i termini sono fortemente normalizzabili, infatti termini come Ω non sono tipabili:
un termine non può essere applicato a se stesso qualunque sia il suo tipo.
Capitolo 2
Corrispondenza di
Curry-Howard
La corrispondenza di Curry-Howard [9] è un isomorfismo fra due strutture:
la deduzione naturale e il λ-calcolo semplicemente tipato. Per descrivere tale
corrispondenza (dagli appunti del corso di Tipi e logica lineare [1]), si considerano i seguenti della logica lineare e se ne da una lettura intuizionista, in
cui una sola formula è vista come output e tutte le altre costituiscono l’input,
e infine si costruisce il λ-termine rappresentante tale dimostrazione.
Più nel dettaglio, i seguenti vengono modificati: si sposta nella parte sinistra
del seguente ($) il duale di una o più formule, che vengono in questo modo
considerate come input del programma, mentre nella parte destra rimane
al massimo una formula che ha invece il ruolo di output. In questo modo
non esistono formule negate, infatti ogni volta che una formula è duale di
un’altra, tale formula si sposta nella parte sinistra del seguente con la sua
formulazione positiva.
Dal momento che si vuole costruire un programma che possa essere eseguito
da una macchina, e visto che ogni macchina produce un unico risultato, si ha
la necessità di avere un unico input. Le regole LK possono essere interpretate in modi diversi, a seconda delle formule cosiderate come ipotesi (input)
e quella che indica la tesi (output); si costruisce poi da ognuna di tali interpretazioni facilmente il λ-termine corrispondente. Viene inoltre mostrato
l’albero che rappresenta graficamente il termine, in cui i nodi sono formule,
ogni padre è conseguenza logica dei figli, le foglie sono le ipotesi e la radice
è la conclusione.
18
CAPITOLO 2. CORRISPONDENZA DI CURRY-HOWARD
2.1
19
Assioma
L’assioma, pAxq, corrisponde alla funzione identità con un input e output di
tipo A. Si ha che:
$ A, AK pAxq
diventa
A$A
pAxq
con programma
xA : A.
L’albero corrispondente sarà costituito da un solo punto
A
2.2
Congiunzione moltiplicativa
La regola della congiunzione moltiplicativa (o del tensore),
$ Γ, A $ B, ∆ pbq
$ Γ, ∆, A b B
può essere interpretata in tre modi.
1. Ponendo come ipotesi i contesti con
Γ ΦK
∆ ΨK
si ottiene
$ ΦK, A $ B, ΨK
$ ΦK, ΨK, A b B
e si ha cosı̀ l’introduzione del connettivo ^ :
Φ$A
Ψ$B
Φ, Ψ $ A ^ B
prm, Rq
pbq,
CAPITOLO 2. CORRISPONDENZA DI CURRY-HOWARD
Φ
Ψ
A
B
20
A^B
Figura 2.1: Rappresentazione dell’albero di prm, Rq
I seguenti Φ $ A, Ψ $ B corrispondono rispettivamente ai termini
srx : Φs : A
try : Ψs : B.
Tali termini sono però indipendenti l’uno dall’altro e, non interagendo
tra loro, sarebbero necessarie due macchine per programmarli.
Questa formulazione del tensore non è un programma ma introduce il
tipo coppia:
A ^ B di tipo xs, ty.
2. Se l’output è una formula C in ∆ si ha:
Γ ΦK
∆ ΨK , C
B
DK
quindi il seguente diventa
$ ΦK, A $ B, ΨK, C
$ ΦK, ΨK, A b DK
dal momento che pA b DK qK
zione dell’implicazione:
AK _ D A Ñ D, si ottiene l’elimina-
Φ$A
D, Ψ $ C
Φ, Ψ, A Ñ D $ C
pÑ, Lq
In questo caso, si rappresenta l’uso del programma:
w : A Ñ D è applicato a srx : Φs : A,
sostituendo poi in
CAPITOLO 2. CORRISPONDENZA DI CURRY-HOWARD
21
Φ
A
AÑD
D
Ψ
C
Figura 2.2: Rappresentazione dell’albero di
pÑ, Lq
try : D, z : Ψs
si ottiene il λ-termine
trwpsrx : Φsq{y : D, z : Ψs : C.
3. Analogamente, può rappresentare l’uso del programma w : B
questo caso però
Γ ΦK , C
∆ ΨK
Φ, D $ C
Ψ$B
Φ, Ψ, B Ñ D $ C
2.3
Ñ D, in
A DK
pÑ, Lq
Disgiunzione moltiplicativa
La regola della disgiunzione moltiplicativa, (`),
$ Γ, A, B p`q
$ Γ, A ` B
ha quattro interpretazioni.
1. Se si ha come input il contesto
Γ ΦK
si ha una formulazione che non può essere programmabile in quanto ha
due output, A e B:
CAPITOLO 2. CORRISPONDENZA DI CURRY-HOWARD
22
$ ΦK, A, B
$ ΦK, A ` B
Φ $ A, B
Φ$A_B
2. Nel caso in cui l’input è sia il duale del contesto sia il duale della
formula, ovvero
Γ ΦK
A DK
si ottiene l’introduzione dell’implicazione:
$ ΦK, DK, B
$ ΦK, DK ` B
e dal momento che DK ` B
D Ñ B si ha:
Φ, D $ B
Φ$DÑB
pÑ, Rq
Φ
D
B
D
ÑB
Figura 2.3: Rappresentazione dell’albero di pÑ, Rq: formula D tra parentesi
indica una foglia morta, viene infatti inglobata poi in A Ñ B
La regola del `, vista in questo modo rappresenta la creazione del
programma w : D Ñ B, il λ-termine corrispondente è:
λx.srx : D, y : Φs : D
Ñ B.
Viene usato il programma come oggetto, la variabile x non è più libera
ma incorporata nel programma, l’astrazione λ opera come quantificatore.
CAPITOLO 2. CORRISPONDENZA DI CURRY-HOWARD
23
3. Analogamente al punto precedente, si ottiene la creazione del programma w : D Ñ A, con
Γ ΦK
B
DK
$ ΦK, A, B
$ ΦK, A ` DK
Γ, D $ A
Γ$DÑA
pÑ, Rq
4. Se, di nuovo, una formula C del contesto è l’ouput, si può interpretare
la regola come l’uso di entrambe le componenti di una coppia.
Γ ΦK , C
A DK
B
EK
si ha:
$ ΦK, C, DK, E K
$ ΦK, C, DK ` E K
Da pDK ` E K qK
D ^ E, si ottiene:
Φ, D, E $ C
Φ, D ^ E $ C
D
E
prm, Lq
Φ
C
Figura 2.4: Rappresentazione dell’albero di prm, Lq
Il λ-termine corrispondente è:
srx : Φ, y : D, z : E s : C
trx : Φ, xy, zy : D ^ E s
CAPITOLO 2. CORRISPONDENZA DI CURRY-HOWARD
2.4
24
Congiunzione additiva
La regola della
modi.
$ Γ, A $ Γ, B (&)
$ Γ, A&B
congiunzione additiva, p&q, può essere
interpratata in tre
1. Ponendo come input il contesto
Γ ΦK
si ottiene l’introduzione della congiunzione
$ ΦK, A $ ΦK, B
$ ΦK, A ^ B
Φ$A
Φ$B
Φ$A^B
Φ
Φ
A
B
p^, Rq
A^B
Figura 2.5: Rappresentazione dell’albero di
p^, Rq
Entrambi i seguenti delle ipotesi hanno stessi input che si contraggono
nella conclusione.
Visto come λ-termine, rappresenta l’introduzione della coppia:
dai due termini srx : Φs : A e trx : Φs : B si ottiene xs, ty : A ^ B.
2. Ponendo come input da una parte tutte le formule del contesto tranne
una e la formula A, dall’altra analogamente con la formula B, si ha:
Γ ΦK , C
A DK
B
EK
CAPITOLO 2. CORRISPONDENZA DI CURRY-HOWARD
25
$ ΦK, C, DK $ ΦK, C, E K
$ ΦK, C, DK ^ E K
Per pDK ^ E K qK
D _ E, si ottiene:
Φ, D $ C
Φ, E $ C
Φ, D _ E $ C
Φ
D
Φ
E
D_E
C
p_, Lq
C
C
Figura 2.6: Rappresentazione dell’albero di
p_, Lq
Si ha quindi l’eliminazione del _ che rappresenta il comando di condizione if-then-else: A _ B può essere ottenuto da $ Γ, A oppure (then)
da $ Γ, B, in entrambi i casi si ottiene la formula C.
Nell’albero, A e B sono foglie morte perchè poi inglobate in A _ B.
3. L’ultima interpretazione considera come input da una parte il duale del
contesto e il duale della formula A, dall’altra solo il duale del contesto:
Γ ΦK , C
A DK
Si ottiene però un seguente con due output, B e C, e ciò non permette
di costruire un programma.
Φ, D
$C
Φ $ B, C
Φ, D $ B, C
Analogamente se si considera solo B insieme al contesto come input
nella parte destra, ovvero con
Γ ΦK , C
B
E K.
CAPITOLO 2. CORRISPONDENZA DI CURRY-HOWARD
2.5
26
Disgiunzione additiva
Le due regole della disgiunzione additiva,
`,
$ Γ, A p`1q
$ Γ, A _ B
$ Γ, B p`2q
$ Γ, A _ B
hanno due interpretazioni ciascuna, che introducono gli oggetti di tipo immersione e di tipo proiezione.
Per la prima regola si hanno i seguenti casi.
1. Se
Γ ΦK
si ha l’introduzione del connettivo
_:
$ ΦK, A
$ ΦK, A _ B
Φ$A
Φ$A_B
p_1, Rq
Φ
A
A_B
Figura 2.7: Rappresentazione dell’albero di
p_1, Rq
Il λ-termine permette di introdurre il primo oggetto di tipo immersione:
il termine trx : Φs : A viene inglobato nel termine i1 ptq : A _ B.
CAPITOLO 2. CORRISPONDENZA DI CURRY-HOWARD
27
2. Se invece:
Γ ΦK , C
A DK
si ha l’eliminazione del connettivo
B
EK
^:
$ ΦK, C, DK
$ ΦK, C, DK _ E K
Dal momento che pDK _ E K qK
D ^ E, si ottiene:
Φ, D $ C
Φ, D ^ E $ C
p^1, Lq
D^E
D
Φ
C
Figura 2.8: Rappresentazione dell’albero di
p^1, Lq
Il λ-termine indica l’uso della coppia come proiezione della prima componente:
la proiezione del termine trx : Φ, y : Ds : D ^ E è il termine P1 ptq : D.
Per quanto riguarda la seconda regola, analogamente si ottiene l’immersione
di B e la proiezione della seconda componente.
1. Se
Γ ΦK
si ha l’introduzione del connettivo
_:
Φ$B
Φ$A_B
p_2, Rq
CAPITOLO 2. CORRISPONDENZA DI CURRY-HOWARD
28
Φ
B
A_B
Figura 2.9: Rappresentazione dell’albero di
p_2, Rq
Il λ-termine descrive il secondo oggetto di tipo immersione:
il termine trx : Φs : B viene inglobato nel termine i2 ptq : A _ B.
2. Se
Γ ΦK , C K
A DK
si ha l’eliminazione del connettivo
B
EK
^:
Φ, E $ C
Φ, D ^ E $ C
p^2, Lq
D^E
E
Φ
C
Figura 2.10: Rappresentazione dell’albero di
p^2, Lq
Il λ-termine indica l’uso della coppia come proiezione della prima componente:
la proiezione del termine trx : Φ, y : Ds : D ^ E è il termine P2 ptq : E.
CAPITOLO 2. CORRISPONDENZA DI CURRY-HOWARD
2.6
29
Indebolimento
La regola dell’indebolimento, pwq,
$Γ
$ Γ, A pwq
può essere interpretata in due modi.
1. Se
Γ ΦK
si ha la concezione dell’assurdo, ovvero dal contesto Φ segue qualsiasi
formula A:
$ ΦK
$ ΦK, A
Φ$
pw, Rq
Φ$A
Φ
K
A
Figura 2.11: Rappresentazione dell’albero di pw, Rq
2. Se
Γ ΦK , C
A DK
si interpreta come una regola in cui si possono aggiungere ipotesi che
poi non sono però usate per la dimostrazione.
$ ΦK, C
$ ΦK, C, A
CAPITOLO 2. CORRISPONDENZA DI CURRY-HOWARD
30
Φ D
C
Figura 2.12: Rappresentazione dell’albero di pw, Lq
Φ$C
Φ, D $ C
pw, Lq
Il λ-termine rappresenta una funzione in cui si aggiunge una variabile
che non gioca alcun ruolo nella formulazione:
srx : Φs : C diventa s1 rx : Φ, y : Ds : C
Vedendo i termini come funzioni, si ha f pxq
alcuna dipendenza da y.
2.7
f px, yq in cui non c’è
Contrazione
La regola di contrazione, pcq,
$ Γ, A, A pcq
$ Γ, A
si può interpretare come contrazione degli output o come contrazione degli
input.
1. Se
Γ ΦK
si ha la contrazione degli output, ma si ottiene un seguente con due
output quindi non programmabile:
$ ΦK, A, A
$ ΦK, A
Φ $ A, A
Φ$A
CAPITOLO 2. CORRISPONDENZA DI CURRY-HOWARD
2. Ponendo invece
Γ ΦK , C
31
A DK
si ottiene la contrazione degli input:
$ ΦK, C, DK, DK
$ ΦK, C, DK
Φ, D, D $ C
Φ, D $ C
A
A
pc, Lq
Φ
C
Figura 2.13: Rappresentazione dell’albero di pc, Lq
Il λ-termine rappresenta l’operazione di diagonalizzazione, ovvero si
identificano le due variabili di tipo D come la stessa variabile, in cui
quindi più occorenze di un’ipotesi vengono considerate come una sola:
srx : D, y : D, z : Φs : C diventa
s1 rw : D, z : Φs srw{x : D, w{y : D, z : Φs : C.
Vedendo i termini come funzioni, si passa da una funzione in due variabili, f px, y q, ad una funzione ad una variabile definita a partire dalla
prima, g pwq f pw, wq.
2.8
Taglio
La regola del taglio, pcutq,
$ Γ, A $ AK, ∆
$ Γ, ∆
(cut)
CAPITOLO 2. CORRISPONDENZA DI CURRY-HOWARD
si può vedere con
Γ ΦK
32
∆ ΨK , C
nel modo seguente
$ ΦK, A $ AK, ΨK, C
$ ΦK, ΨK, C
Φ$A
Ψ, A $ C
(cut)
Φ, Ψ $ C
Rappresenta la composizione di due λ-termini:
srx : Φs : A e try : A, z : Ψs : C
applicati l’uno all’altro diventano il termine
trsrx : Φs{y, z : Ψs : C
si sostituisce cioè la variabile di tipo A con un termine di tipo A.
Graficamente:
Φ
Φ
i due alberi A ,
Ψ
A
C
A
si compongono in uno solo
Ψ
C
.
Capitolo 3
Altri sistemi di calcolo tipato
Girard nel suo libro Proos and types [9] presenta ulteriori sistemi di calcolo
tipato finalizzati ad ottenere una maggiore espressività del calcolo stesso. A
tale scopo si introducono nuovi tipi, o nuovi termini (o entrambi), da cui segue
la definizione di sistemi come il sistema T di Go:del e il sistema F. Il primo
permette di proporre un miglioramento di espressività del calcolo a discapito
certamente della semplicità e componibilità concettuale, ma rimane limitato
alla sola rappresentazione dei booleani e degli interi. Il sistema F è invece
più completo grazie all’aggiunta di un nuovo schema logico che consente di
lavorare con tipi di dati comuni (liste, alberi . . . ). Entrambi questi sistemi
vengono descritti e discussi in questo capitolo, con particolare attenzione al
confronto dei loro rispettivi poteri espressivi.
3.1
3.1.1
Il sistema T
Sintassi e calcolo
Definizione 3.1 (Tipi) Si definiscono solo due tipi: quello degli interi, Int,
e quello delle costanti booleane, Bool.
Definizione 3.2 (Termini) I termini si costruiscono tramite operazioni di
introduzione e eliminazione.
Int-introduction:
• 0 è una costante di tipo Int;
• se t è di tipo Int, allora St è di tipo Int, dove S è la funzione
successore;
33
CAPITOLO 3. ALTRI SISTEMI DI CALCOLO TIPATO
34
Int-elimination: se u, v e t sono rispettivamente di tipo U ,
U Ñ pInt Ñ U q e Int, allora Ruvt è di tipo U, dove R è un operatore
di ricorsione, definito da
"
Ruvm ;
u
se m 0
v pRuvnqn se m n
1
Bool-introduction: T e F sono le costanti di tipo Bool, ovvero rappresentano i valori di verità;
Bool-elimination: se u, v, t sono rispettivamente di tipo U , V e Bool, allore
Duvt è di tipo U ., dove D è l’operatore if . . . then . . . else, definito per
casi
"
u se b T
Duvb ;
v se b F
Definizione 3.3 (Conversione:) Le regole di riduzione sono le stesse del
λ-calcolo tipato semplice più le seguenti:
Ruv0 ; u
Ruv pStq ; v pRuvtqt
DuvT ; u
DuvF ; v
Teorema 3.4 (Normalizzazione) In T tutte le sequenze di riduzioni sono
finite e permettono di ottenere la stessa forma normale.
Dimostrazione:
Per estenzione del teorema di Church-Rosser, non è difficile estendere
la dimostrazione al sistema T, procedendo per induzione sui termini. 3.1.2
Potere espressivo
Perchè si garantisca che un oggetto di tipo Int rappresenti davvero un intero,
uno di tipo Bool un booleano, . . . si ha il seguente Lemma:
Lemma 3.5 Sia t un termine normale chiuso:
• se t è di tipo Int, allora t è della forma n, per qualche n P N;
• se t è di tipo Bool, allora t è della forma T o F;
• se t è di tipo U xV , allora t è della forma xu, v y;
• se t è di tipo U
Ñ V , allora t è della forma λx.v.
CAPITOLO 3. ALTRI SISTEMI DI CALCOLO TIPATO
35
In particolare, se t è un termine di tipo Int Ñ Int di T, induce una funzione
|t| da N a N definita da:
|t|pnq m
sse
tn ; m
Analogamente, un termine chiuso del tipo Int Ñ Bool induce un predicato
|t| su N:
|t|pnq T sse tn ; T
Le funzioni |t| sono calcolabili: l’algoritmo di normalizzazione restituisce
|t|pnq come una funzione di n, quindi le funzioni rappresentabili in T sono
ricorsive.
Visto come algoritmo, il calcolo di |t| equivale ad una sequenza di riduzioni
per t che termina con la forma normale di t. Il teorema di normalizzazione
garantisce la terminazione di tutti gli algoritmi ottenuti da funzioni definite
in T.
È sufficiente l’Aritmetica di Peano (PA) per esprimere la riducibilità di un
termine t e dei suoi sottotermini e mostrare che con un numero finito di passi
si ottiene la forma normale di t, ovvero in PA è dimostrabile che |t| sia totale.
Inoltre anche il viceversa è vero: se f è una funzione ricorsiva e dimostrabilmente totale in PA, allora si può trovare un termine di tipo Int Ñ Int in T
tale che f pnq |t|pnq per ogni n.
Il potere espressivo del sistema T è però limitato alle funzioni di PA, il
sistema F risulta essere più completo e ricco.
3.2
Il Sistema F
Nella versione più classica del sistema F, i tipi vengono costruiti dalle variabili
di tipo variabili X, Y, Z . . . per mezzo dell’implicazione e della quantificazione
universale. Le regole della costruzione dei termini sono quelle del semplice
λ-calcolo tipato a cui vanno aggiunti i seguenti schemi di regole per il secondo
ordine:
generalizzazione: se t è un termine di tipo A e se la variabile di tipo X
non è libera nel tipo di una variabile libera t, allora ΛX.t è un termine
di tipo @X, A;
estrazione: se t è un termine di tipo @X.A e se B è un tipo, allora ttuB è
un termine di tipo ArB {X s.
CAPITOLO 3. ALTRI SISTEMI DI CALCOLO TIPATO
3.2.1
36
Sintassi e calcolo
Definizione 3.6 (Tipi) I Tipi sono definiti a partire dai tipi variabile X, Y, Z, . . .
attraverso due operazioni:
• se U e V sono tipi, allora U
ÑV
è un tipo;
• se V è un tipo, e X un tipo variabile, allora @X.V è un tipo.
Definizione 3.7 (Termini) Si hanno cinque tipi di schemi per costruire i
termini:
1. variabili: xT , y T , z T , . . . sono variabili di tipo T ;
2. applicazione: se t e v sono rispettivamente di tipo U
ptqu è di tipo V ;
ÑV
e U , allora
3. λ-astrazione: se xU è una variabile di tipo U e v di tipo V , allora λxU .v
è di tipo U Ñ V ;
4. astrazione universale: se v è un termine di tipo V , allora si costruisce
ΛX.v di tipo @X.V , dove X non è una variabile libera nel tipo di varibile
di v;
5. applicazione universale: se t è un termine di tipo @X.V e U è un tipo,
allora ptqU è un termine di tipo V rU {X s.
Definizione 3.8 (Conversione) Il sistema viene fornito di una conversione analoga a quella definita per il λ-calcolo puro
pΛX.vqU ; vrU {X s
che soddisfa la proprietà di Church-Rosser, quindi l’unicità della forma normale.
3.2.2
Rappresentazione dei tipi semplici
Booleani
Il tipo Bool è definito come @X.X
sono:
T : ΛX.λxX .λy X .x
Ñ X Ñ X, gli oggetti di questo tipo
F : ΛX.λxX .λy X .y
CAPITOLO 3. ALTRI SISTEMI DI CALCOLO TIPATO
37
Si definisce, analogamente come per il sistema T, l’operatore D: se u, v, t
sono rispettivamente di tipo U ,V e Bool, allora Duvt è di tipo U secondo la
seguente definizione:
Duvt : tU uv
Si verifica che
DuvT ; u
DuvF ; v
Prodotto di tipi
Si definisce U xV , dove U e V sono tipi, come il tipo @X.pU
Gli oggetti di questo tipo sono le coppie:
Ñ V Ñ X q Ñ X.
xu, vy : ΛX.λxU ÑV ÑX .xuv
Data una coppia, si definiscono le proiezioni delle componenti.
π 1 t : tU pλxU .λy V .xq
π 2 t : tV pλxU .λy V .y q
Si ha infatti che
π 1 xu, v y ; u
π 2 xu, v y ; v.
Tipo vuoto
Si può definire il tipo Emp come @X.X. L’unico oggetto di questo tipo è
U t : tU
Tipo somma
Se U, V sono tipi, si può definire il tipo U V come
@X.pU Ñ X q Ñ pV Ñ X q Ñ X. Gli oggetti di questo tipo sono costruiti nel
modo seguente:
i1 u : ΛXλxU ÑX λy V ÑY .xu
i2 u : ΛXλxU ÑX λy V ÑY .yu
con u : U
con u : V
Dato un oggetto di tipo somma si definiscono le iniezioni canoniche tramite
l’operazione
δx.uy.vt : tU pλxU .uqpλy V .v q
Si ha:
δx.uy.v pi1 rq ; urr{xs
con s, v : U
V.
δx.uy.v pi2 sq ; urs{y s
CAPITOLO 3. ALTRI SISTEMI DI CALCOLO TIPATO
38
Tipo esistenziale
Si definisce il tipo DX.V come @Y p@V
sono
Ñ Y q Ñ Y . Gli oggetti di questo tipo
xU, vy : ΛY pλ[email protected] ÑY .xU vq
con v : V rU {X s e U un tipo.
I termini di questo tipo si costruiscono per mezzo delle regole
..
.
ArB {X s
DXA
pD2iq
A
..
.
..
.
DXA
B
B
pD2q
Il tipo esistenziale permette di definire la funzione
∆X.x.wt : tW pΛX.λxV .wq
che definisce la regola di conversione
p∆X.x.wqxU, uy wrU {X srv{xV rU {X ss
con w : W , t : DX.V , X tipo variabile e x : V , dove le uniche occorrenze
libere di X nel tipo variabile di w sono di tipo x.
3.2.3
Strutture libere
La rappresentazione dei tipi (anche di quelli precedentemente descritti) avviene tramite strutture libere, ovvero costruzioni di tipi descritte da due
classi di funzioni, i costruttori e distruttori.
I costruttori sono funzioni f1 , . . . , fn che generano una struttura Θ. Ogni
elemento di Θ è quindi rappresentato in modo unico da una successione di
applicazioni dell fi . Tali funzioni sono rispettivamente di tipo S1 , . . . , Sn ,
dove ogni tipo è della forma Si : T1i Ñ T2i . . . Ñ Tki Ñ Θ.
Ponendo S i Si rX {Θs, il tipo che rappresenta Θ è definito come
T : @X.S 1
Ñ S2 Ñ . . . Ñ Sn Ñ X
CAPITOLO 3. ALTRI SISTEMI DI CALCOLO TIPATO
39
I distruttori sono funzioni che, applicate ad oggetti di tipo T , permettono
di descrivere l’utilizzo di tali oggetti. Per esempio la funzione D mostra
l’utilizzo dei booleani, ovvero distinguere i casi nella programmazione del
If. . . Then. . . Else.
Mostrare formalmente la rappresentazione dei costruttori risulta complesso,
si capirà la loro forma meglio negli esempi. In breve, un costruttore deve
essere una funzione fi con ki argomenti di tipo Tji rT {X s che restituisce un
valore di tipo T .
Tipi semplici
I tipi semplici sono casi particolari di strutture libere. Vedendoli come tali,
vengono ora mostrati i costruttori e la forma del tipo seguendo il sistema
appena descritto sulle strutture libere.
• Bool
Il tipo Bool ha come costruttori f1 e f2 che sono entrambi la funzione
costante, ovvero di tipo S1 , S2 X, è infatti T @X.X Ñ X Ñ X e
il distruttore è la funzione D che utilizza i booleani per distinguere i
casi nella programmazione del If. . . Then. . . Else;
• Prodotto di tipi
Il tipo risultante dal prodotto di tipi ha un unico costruttore f1 di tipo
S1 U Ñ V Ñ X, è T @X.pU Ñ V Ñ X q Ñ X e i distruttori sono
le due proiezioni π 1 , π 2 ;
• Somma di tipi
Il tipo risultante dalla somma di tipi ha due costruttori f1 e f2 , di tipo
S1 U Ñ X e S2 V Ñ X, è T @X.pU Ñ X q Ñ pV Ñ X q Ñ X e
il distruttore è la funzione δ che definisce la riduzione;
• Emp
Il tipo vuoto non ha costruttori, ovvero l’arità della funzione costruttore
è n 0.
Tipi induttivi
Vengono ora descritte delle strutture molto più complesse, che rappresentano
tipi i cui oggetti si costruiscono induttivamente.
• Int
Il tipo Int ha due costruttori f1 e f2 , di tipo S1
ed è
X e S2 X Ñ X,
CAPITOLO 3. ALTRI SISTEMI DI CALCOLO TIPATO
T
40
@X.X Ñ pX Ñ X q Ñ X
Gli oggetti di questo tipo hanno la seguente forma (che è una versione
tipata dei numerali di Church)
n : ΛXλxX λy X ÑX ylooomooon
py . . . py xq . . .q
n
Si costuiscono gli oggetti di tipo Int iterando la funzione successore
Sn : n 1
0 : ΛXλxX λy X ÑX x
St : ΛXλxX λy X ÑX y ptXxy q
con t : Int
Il distruttore in questo caso è una funzione di iterazione definita nel
modo seguente:
Ituf t : tU uf
con t : Int
In particolare si ha
Ituf p0q : u
Ituf pStq : f pItuf tq
• List
Sia U un tipo, si vuole costruire il tipo ListU , i cui oggetti sono sequenze finiti di oggetti di tipo U , pu1 , . . . , un q.
I costruttori di questo tipo sono due: f1 di tipo S1 X che costituisce
la lista vuota e f2 di tipo S2 U Ñ X Ñ X che rappresenta la concatenazione di un elemento in una lista. Il tipo associato a una lista è
quindi
T ΛX Ñ pU Ñ X Ñ X q Ñ X
I costruttori si definiscono come segue:
r s nil : ΛXλxX λyU ÑX ÑX x
ru1, . . . , un, t1, . . . , tms consputq : ΛXλxX λyU ÑX ÑX yuptXxyq
CAPITOLO 3. ALTRI SISTEMI DI CALCOLO TIPATO
41
Una lista di oggetti di tipo U ha quindi la seguente forma nel sistema
F
ru1, u2, . . . , uns ΛXλxX λyU ÑX ÑX yu1pyu2 . . . pyunxq . . .q
dove y cons e x nil.
Il comportamento delle liste è molto simile a quello degli interi. In
particolare, anche in questo caso si ha un operatore di iterazione sulle
liste:
Itwf t : tW wf
Ñ W Ñ W e t : ListU , che soddisfa
Itwf pnilq : w
Itwf pconsputqq : f uItwf t
con W tipo, w : W , f : U
• BinaryTree
Con il sistema F si possono definire anche oggetti gli alberi binari finiti,
molto utilizzati nell’ambito della programmazione.
Il tipo BinTree ha due costruttori: f1 di tipo S1 X, che indica
l’albero con una sola radice, e f2 di tipo S2 X Ñ X Ñ X, che
definisce l’operazione di costruzione di un albero a partire da due alberi.
Il tipo associato è
T
ΛX Ñ pX Ñ X Ñ X q Ñ X
I costruttori si definiscono come segue:
nil : ΛXλxX λy p X
Ñ X Ñ X qx
couplepuv q : ΛXλxX λy p X Ñ X Ñ X qy puXxy qpvXxy q
Anche per il tipo BinTree si ha un operatore di iterazione definito da
Itwf t : tW wf
con W tipo, w : W , f : W
Ñ W Ñ W e t : BinT ree, che soddisfa
Itwhpnilq ; w
Itwf pcouplepuv qq f pItwf uqpItwf v q
Capitolo 4
Teoremi di normalizzazione
La normalizzazione per il sistema F [9] risulta complessa da definire. Si procede prendendo in esame innanzitutto il caso del λ-calcolo tipato semplice, in
cui si considerano solo i termini riducibili (come accennato nel primo capitolo
i termini irriducibili non si possono tipare) e dalle proprietà sulla riducibilità
segue il teorema di forte normalizzazione. I risultati sul λ-calcolo tipato semplice si estendono al sistema F, ma si applica l’induzione su una struttura che
non è ben fondata: si ha infatti il problema che al secondo ordine non vale
la proprietà della sottoformula. Anche per la sostituzione ci sono problemi
di struttura, che però si risolvono definendo il tipo ArB {X s e la riducibilità
di tipo B: procedendo come nel caso del λ-calcolo tipato semplice, si ottiene
la forte normalizzazione per i tutti i termini del sistema F.
4.1
Riducibilità e normalizzazione nel λ-calcolo
tipato semplice
Definizione 4.1 Si definisce un insieme REDT di termini riducibili di tipo
T per induzione sui tipi:
1. per t di tipo atomico T , t è riducibile se è fortemente normalizzabile;
2. per t di tipo U xV , t è riducibile se π 1 t e π 2 t sono riducibili;
3. per t di tipo U Ñ V , t è riducibile se, per ogni termine riducibile u di
tipo U , ptqu è riducibile di tipo V .
Definizione 4.2 Un termine si dice neutro se non inizia con un simbolo
astrazione, ovvero se è in una delle seguenti forme
x
π1t
π2t
42
ptqu
CAPITOLO 4. TEOREMI DI NORMALIZZAZIONE
43
Proposizione 4.3 L’insieme dei termini riducibili verifica le seguenti proprietà per ogni tipo T :
(CR 1) se t P REDT , allora t è fortemente normalizzabile;
(CR 2) se t P REDT e t ; t1 , allora t1
P REDT ;
(CR 3) se t è neutro e se per tutte le riduzioni di t si ottiene un termine
t1 P REDT , allora t P REDT .
In particolare,
(CR 4) se t è neutro e normale, allora t P REDT .
Dimostrazione:
Si procede per induzione sui tipi. Lemma 4.4 (Riducibilità del tipo coppia) Se u, v sono riducibili allora
xu, vy è riducibile.
Dimostrazione:
Per la proprietà (CR 1) si procede per induzione su ν puq ν pv q mostrando che π 1 xu, v y e π 2 xu, v y sono riducibili per poi concludere per il
punto 2 della definizione.
π 1 xu, v y si può ridurre a
- u che è riducibile per ipotesi;
- π 1 xu1 , v y con u ; u1 . u1 è riducibile per (CR 2) e si ha che
ν pu1 q ν puq, per ipotesi induttiva π 1 xu1 , v y è riducibile;
- π 1 xu, v 1 y con v ; v 1 , si conclude analogamente al punto precedente.
Quindi π 1 xu, v y è riducibile per (CR 3), procedendo allo stesso modo
lo è anche π 2 xu, v y. Si conclude che xu, v y è riducibile. Lemma 4.5 (Riducibilità per l’astrazione) Se per ogni termine u di tipo U , v ru{xs è riducibile, allora λx.v è riducibile.
Dimostrazione:
Si deve mostrare che pλx.v qu è riducibile per ogni u. Si procede per
induzione, come per il lemma precedente, su ν pv q ν puq.
pλx.vqu si può ridurre a
- v ru{xs che è riducibile per ipotesi;
CAPITOLO 4. TEOREMI DI NORMALIZZAZIONE
44
- pλx.v 1 qu con v ; v 1 . v 1 è riducibile per (CR 2) e si ha che
ν pv 1 q ν pv q, per ipotesi induttiva pλx.v 1 qu è riducibile;
- pλx.v qu1 con u ; u1 , si conclude analogamente al punto precedente.
Quindi λx.v è riducibile. Si può ora dimostrare il teorema.
Teorema 4.6 (Riducibilità) Tutti i temini tipati semplici sono riducibili.
Applicando la proprietà (CR 1) si ottiene:
Corollario 4.7 (Normalizzazione forte) Tutti i termini tipati semplici
sono fortemente normalizzabili.
Per dimostrare il teorema di riducibilità, oltre ai risultati precedenti,
è necessaria la riducibilità per sostituzione in parallelo al fine di ottenere
un’ipotesi induttiva più forte nel caso dell’astrazione.
Proposizione 4.8 Sia t un termine con variabili libere in tx1 , . . . , xn u. Se
u1 , . . . , un sono termini riducibili di tipo U1 , . . . , Un , allora tru1 {x1 , . . . , un {xn s
è riducibile.
Dimostrazione:
Si procede per induzione su t.
– se t xi , allora tru{xs ui che è riducibile per ipotesi;
– se t π 1 w, per ipotesi induttiva wru{xs è riducibile quindi anche
π 1 pwru{xsq è riducibile e coincide con tru{xs, segue la tesi;
– se t π 2 w, si procede come per π 1 w;
– se t xv, wy, per ipotesi induttiva v ru{xs e wru{xs sono riducibili,
segue dal lemma che tru{xs xuru{xs, v ru{xsy è riducibile;
– se t pwqv, per ipotesi induttiva v ru{xs e wru{xs sono riducibili,
segue dal lemma che tru{xs pwru{xsqv ru{xs è riducibile;
– se t λy.w di tipo V Ñ W per ipotesi induttiva wru{x, v {y s è
riducibile per ogni v di tipo V , segue dal lemma che tru{xs λy.wru{xs è riducibile. CAPITOLO 4. TEOREMI DI NORMALIZZAZIONE
4.2
45
Riducibilità e normalizzazione nel sistema F
Definizione 4.9 (Candidato di riducibilità) Sia A un tipo, si definisce
candidato di riducibilità di tipo A un insieme R di termini di tipo A che
soddisfa le seguenti condizioni:
(CR 1) ogni termine in R è fortemente normalizzabile;
(CR 2) se t P R e t ; t1 , allora t1
P R;
(CR 3) se t è semplice e ogni volta che si converte un redesso di t si ottiene un
termine t1 P R, allora t P R.
Dalla (CR 3) si ha in particolare che
(CR 4) Se t è neutrale e normale, allora t P R.
Si noti che R non è mai vuoto, in quanto contiene sempre almeno le variabili
di tipo U .
Se R e S sono candidati di riducibilità di tipo U e V , si può definire un
insieme R Ñ S di termini di tipo U Ñ V :
tPR
se e solo se per ogni upu P Rq si ha ptqu P S
Definizione 4.10 (Riducibilità parametrica) Sia R una sequenza di candidati di riducibilità dei tipi corrispondenti, si definisce riducibilità parametrica un insieme REDT rR{X s di termini di tipo T rU {X s come segue
Xi, allora REDT rR{X s Ri;
se T V Ñ W , allora REDT rR{X s REDV rR{X s Ñ REDW rR{X s;
±
se T Y.W allora REDT rR{X s è l’insieme di temini t di tipo
T rU {X s tali che, per ogni tipo V e candidato di riducibilità S di questo
tipo, allora tV P REDW rR{X, S {Y s.
1. se T
2.
3.
Lemma 4.11 REDT rR{X s è un candidato di riducibilità di tipo T rU {X s.
Dimostrazione:
Si procede per induzione sui tipi:
– se T
Xi è ovvio in quanto REDT rR{X s Ri;
CAPITOLO 4. TEOREMI DI NORMALIZZAZIONE
46
– se T V Ñ W , per ipotesi induttiva REDV rR{X s e REDW rR{X s
sono cadidati di riducibilità di tipo T rU {X s e quindi lo è anche
anche REDT rR{X s per il punto 2 della definizione;
– se T
(CR 1)
± Y.W , allora si verificano le proprietà.
se t P REDT rR{X s, sia V un tipo arbitrario e S un candidato
di riducibilità di tipo V , allora per definizione
tV P REDW rR{X, S {Y s e per ipotesi induttiva tV è fortemente normalizzabile, dal fatto che ν ptq ¤ ν ptV q segue che t
è fortemente normalizzabile;
(CR 2) se t P REDT rR{X s e t ; t1 per tutti i tipi V e candidati
di riducibilità S, si ha che tV P REDW rR{X, S {Y s e tV ;
t1 V , per ipotesi induttiva t1 V P REDW rR{X, S {Y s, segue
t1 P REDW rR{X s;
(CR 3) se t è neutro e tutti i t1 ottenuti da t son in REDT rR{X s,
allora sia V un tipo arbitrario e S un candidato di riducibilità di tipo V , si ha che tV ; t1 V , perchè t è neutrale per
ogni conversione in t, e t1 V P REDW rR{X, S {Y s, perchè t1 P
REDT rR{X s. Per ipotesi induttiva tV P REDW rR{X, S {Y s
e quindi t P REDW rR{X s. Il seguente lemma mostra che la riducibilità parametrica ha un buon comportamento rispetto alla sostituzione.
Lemma 4.12 (Lemma di sostituzione)
REDT rV {Y s rR{X s REDT rR{X, REDV rR{X s{Y s
Per l’astrazione e l’applicazione universale si ottengono i seguenti risultati.
Lemma 4.13 Se per ogni tipo V e candidato S, wrV {Y s P REDW rR{X, S {Y s,
allora ΛY.w P RED± Y.W rR{X s.
Dimostrazione:
Si deve dimostrare che pΛY.wqV P REDW rR{X, S {Y s per ogni tipo V
e candidato di riducibilità S.
Si procede per induzione su ν pwq. Convertendo un redesso di pΛY.wqV
si può ottenere:
– pΛY.w1 qV con ν pw1 q ν pwq che ı̀n REDW rR{X, S {Y s per ipotesi
induttiva;
– wrV {Y s che per ipotesi è in REDW rR{X, S {Y s.
CAPITOLO 4. TEOREMI DI NORMALIZZAZIONE
segue dalla proprietà (CR 3) che ΛY.w
Lemma 4.14 Se t
ogni tipo V .
47
P RED± Y.W rR{X s. P RED± Y.W rR{X s, allora tV P REDW rV {Y srR{X s per
Dimostrazione:
Per ipotesi tV P REDW rR{X, S {Y s per ogni S candidato di riducibilità. Ponendo S REDV rR{X s segue da lemma di sostituzione.
Per concludere si ha la seguente definizione di riducibilità.
Definizione 4.15 (Termine riducibile) Un termine t di tipo T si dice riducibile se è in REDT rSN {X s, con X1 , . . . , Xm tipo variabili libere di T e
SNi è l’insieme dei termini fortemente normalizzabili di tipo Xi .
Si può dimostrare che
Teorema 4.16 Tutti i termini di F sono riducibili.
Anche per il sistema F è necessario un risultato pig̀enerale che permette la
sostituzione due volte in parallelo e da cui segue il teorema ponendo Ri SNi
e uj xj .
Proposizione 4.17 Sia t un termine di tipo T e siano tutte le variabili libere
di t tra x1 , . . . , xn di tipo U1 , . . . , Un e tutti i tipi variabili libere U1 , . . . , Un
di T tra V1 , . . . , Vm . Se R1 , . . . , Rm sono candidati di riducibilità di tipo
V1 , . . . , Vm e u1 , . . . , un termini di tipo U1 rV {X s, . . . , Un rV {X su appartenti a
REDU1 rR{X s, . . . , REDUn rR{X s, allora trV {X sru{xs P REDT rR{X s.
Dimostrazione:
Si dimostra in modo ±
simile al caso del λ-calcolo tipato semplice, aggiungendo i casi per
Y.W e ΛY.w in cui si ottiene la tesi usando i
lemmi ad essi relativi. Infine per il teorema e la proprietà (CR 1), si ottiene la normalizzazione forte.
Lemma 4.18 Tutti i termini di F sono fortemente normalizzabili.
Capitolo 5
λ-calcolo infinitario e ludica
computazionale
In questo capitolo viene descritto il λ-calcolo infinitario introdotto da Damiano Mazza [18] basato su un frammento della logica lineare intuizionista.
Tale calcolo è dotato di una metrica che rende l’insieme dei termini uno spazio metrico incompleto, il cui completamento viene ottenuto producendo un
λ-calcolo affine infinitario. Quest’ultimo, quozientato con una determinata
relazione di equivalenza, risulterà isomorfo all’usuale λ-calcolo. Si mostrano inoltre alcuni risultati relativi all’usuale topologia sui λ-termini definita
in [4], mettendola in relazione con il nuovo spazio topologico ottenuto con il
λ-calcolo affine infinitario.
Nel secondo paragrafo dopo aver definito la ludica computazionale di Terui [22], si presenta una corrispondenza nel senso di Curry-Howard tra le
derivazioni nella logica moltiplicativa esponenziale polarizzata e i termini infinitari definiti da Mazza nel suo articolo, tali termini vengono definiti tramite
i disegni della ludica computazionale.
5.1
Un λ-calcolo poliadico infinitario Λ8
Definizione 5.1 (Termini) Sia V un insieme infinito non numerabile di
N
variabili e Vinj
il sottoinsieme delle funzioni inettive di V N . Si definisce
Λ08
Λh8
1
¤
V tKu
¤
¤
N
Λh8 tλx.t|t P Λh8, x P Vinj
u ttu|t P Λh8, u P pΛh8qNu
48
CAPITOLO 5. λ-CALCOLO INFINITARIO E LUDICA COMPUTAZIONALE49
L’ insieme dei termini è
Λ 8 :
¤
P
Λh8
h N
L’altezza di un termine t è definita come il minimo h tale che t P Λh8 .
Si denota con B pΛ8 q il sottoinsieme di ΛN8 delle sequenze di altezza limitata
h, ovvero:
se u P B pΛ8 q allora esiste h P N tale che per ogni i P N l’altezza di u è al massimo h.
Le nozioni standard di variabile libera e legata, α-equivalenza e sostituzione
sono definite come nel normale λ-calcolo.
N
, si definisce sru{xs per
In particolare, dato s P Λ8 , u P pΛh8 qN e x P Vinj
induzione:
xru{xs "
upiq se esiste i P N : xpiq x
x
se per ogni i P N : xpiq x
pλy.tqru{xs λy.tru{xs
ptvqru{xs tru{xsv’ con v’piq vru{xs
Definizione 5.2 (Riduzione one-step) La riduzione one-step è definita
da pλx.tqu Ñ tru{xs
Ñ ,
La riduzione, denotata da
riduzione one-step.
è la chiusura transitiva e riflessiva della
Definizione 5.3 (Termini finiti) Se S è un insieme tale che K R S e S pNq
il sottoinsieme di S N delle funzioni con supporto finito, allora gli elementi di
S pNq sono sequenze finite xs0 , s1 , . . . , sn1 y con sn1 K e sn p K, per ogni
p P N. I termini finiti sono generati da:
t, u :: K
|
x
|
λx0 . . . xn1 .t
| txu0, u1, . . . , un1y
e si denota con Λp l’insieme dei termini finiti.
Il calcolo Λp è semplicemente un λ-calcolo poliadico (indicato dalla p al pedice) con un termine speciale (K) che ha il ruolo di una variabile che non si
può sostituire. Le operazioni di α-equivalenza, sostituzione e riduzione su Λp
sono le stesse del normale λ-calcolo.
Si definisce il calcolo finito con Λ8 per mezzo di un processo di completamento metrico. Per fare questo è necessario definire una topologia su Λ8 , a
CAPITOLO 5. λ-CALCOLO INFINITARIO E LUDICA COMPUTAZIONALE50
tale scopo si considerano i termini come alberi.
Osservazione: I termini vengono visti come alberi di altezza finita ma
con infinite ramificazioni. Questo risulterà utile per molte dimostrazioni per
procedere con un’induzione sull’altezza.
5.1.1
Topologia sui λ-termini
Esiste una topologia naturale sui termini del λ-calcolo [4], detta topologiaalbero. Tale topologia viene ottenuta associando ad ogni termine un albero
di Böhm e poi addattando la topologia di Scott (Appendice C) su questi
alberi ai termini.
Definizione 5.4 (Albero parziale Σ-etichettato) Si definisce posizione
un elemento di P N , l’insieme delle parole finite di N e un alfabeto un
insieme Σ tale che K R Σ.
Un albero parziale è una funzione dall’insieme delle posizioni all’alfabeto
delle etichette, ovvero un elemento di
TpΣq : pΣ Y tKuqP
Sia il supporto di una funzione f P pΣ Y tKuqP l’insieme
supppf q ta P P|f paq Ku, allora un albero parziale è finito se il suo
supporto è finito e ha lunghezza finita se le parole nel suo supporto hanno
lunghezza limitata.
Si denota con T0 pΣq e Th pΣq gli insiemi di tutti gli alberi parziali finiti e di
altezza finita, rispettivamente, sull’alfabeto Σ.
”
N
, y P V u,
Definizione 5.5 (Albero di Böhm) Sia Σ V tλx.y |x P Vinj
si defisce albero di Böhm un elemento di TpΣq.
Dato un λ-termine t il corrispondente albero di Böhm BT ptq si costruisce nel
modo seguente.
Se t non è un termine risolubile, l’albero di Böhm non è definito, ovvero
BT ptq K
Se t è un termine risolubile (Definizione 1.12) e quindi nella forma normale
di testa (Lemma 1.13) t λx.yt1 . . . tn , il λ-termine viene rappresen-
CAPITOLO 5. λ-CALCOLO INFINITARIO E LUDICA COMPUTAZIONALE51
tato dall’albero
BT ptq λx.y
BT pt1 q... BT ptn q
Si indica con tpaq il simbolo presente nella posizione a di un termine t.
B è l’insieme degli alberi di Böhm.
Osservazione: La definizione di BT ptq non è una definizione induttiva, in
quanto i sottotermini t1 . . . tn potrebbero essere più complessi di t stesso, descrive più che altro un processo che porta ad un possibile albero infinito.
Ogni albero di Böhm corrisponde a un λ-termine. Sia A un albero di
Böhm e tpAq il rispettivo λ-temine, allora si ha:
A K ÝÑ tpAq Ω, con Ω pλx.xxqλx.xx
A λx.y
ÝÑ tpAq λx.y
A λx.y
A1 ...
... An
ÝÑ tpAq λx.ytpA1q . . . tpAnq
Esempio: sia A
λxy.x
y
K
y
λx.x
allora tpAq λxy.xyΩpyλx.xq
La relazione tra alberi di Böhm e λ-termini è quindi uno a uno. Utilizzare
la scrittura funzionale del λ-termine o considerare il rispettivo albero che
lo rappresenta è dunque indifferente. In particolare, è molto utile vedere i
termini come alberi per definire una struttura topologica ed osservare alcune
proprietà sui λ-termini e loro interazioni, legate appunto alla topologia, che
CAPITOLO 5. λ-CALCOLO INFINITARIO E LUDICA COMPUTAZIONALE52
altrimenti non risalterebbero.
Gli alberi di Böhm sono di fatto funzioni parziali, B „ N Ñ Σ, e poichè le
funzioni parziali con la relazione „ formano un cpo (ordine parziale completo, Def C.1), si ha che „ determina una relazione d’ordine parziale anche su
B.
Definizione 5.6 Dati A, B
alberi „ in cui
PB
si definisce una relazione d’ordine tra gli
A „ B se e solo se A risulta da B tagliando alcuni dei suoi sottoalberi.
Definizione 5.7 Si considera il cpo B
O „ Λ è aperto se e solo se
pB, „q con la topologia di Scott.
(i) t P O, BT ptq „ BT pt1 q ñ t P O
(ii) se t P O e BT ptq i tale che ti P O.
”
i
BT pti q, con tBT pti qui
„ B diretto, allora esste
In particolare, lo spazio di funzioni TpΣq può essere dotato della topologia di
semplice convergenza, che si può metrizzare come segue.
Definizione 5.8 Se a n1 . . . nk P P, ponendo αpaq 2n1 1 . . . 2nk 1 , si
defisce
ds pt, t1 q suptαpaq|a P P, tpaq t1 paqu
È immediato verificare che ds è un’ultrametrica limitata, la cui uniformità
ammette come base di entourages gli insiemi
tpt, t1q P TpΣq2| per ogni a P A, tpaq t1paqu
dove A ta P P|αpaq ¥ u, con 0 ¤ 1.
U
Si ha quindi che più gli alberi sono vicini, rispetto a tale distanza, più coincidono su molte posizioni, questo significa che ds produce una topologia di
semplice convergenza.
Lo spazio TpΣq è quindi uno spazio uniforme. A partire da uno spazio
uniforme si definisce la topologia indotta.
Definizione 5.9 Un insieme A „ TpΣq è aperto se per ogni t P A esiste
U P tU u0 ¤1 tale che
U rts tt1 |pt, t1 q P U u „ A
CAPITOLO 5. λ-CALCOLO INFINITARIO E LUDICA COMPUTAZIONALE53
Si verifica che tali aperti sono aperti di Scott.
Proposizione 5.10 Gli insiemi aperti della topologia indotta dall’uniformità sono aperti di Scott.
Dimostrazione:
– Si deve dimostrare che se t P A e t „ t2 allora t2 P A.
Se t P A, allora esiste U tale che U rts tt1 |pt, t1 q P U u „ A. Per
definizione si ha che tpaq t1 paq per ogni a P A e t1 P U rts. Dato
t2 con t „ t2 , allora t2 paq tpaq per ogni posizione a di t, quindi
anche t2 P U . Si ha quindi che t2 P U rts „ A.
”
– Resta da far vedere che se t i ti P A con tti ui diretto, allora
esiste i tale che ti P A. È banale in quanto almeno uno dei ti P U
e quindi ti P U rts „ A
Si conclude che A è un aperto di Scott. Segue la topologia:
H tt1|pt, t1q P U1u è un insieme aperto;
dati A1 , A2 due aperti allora
A1
£
$
$
& A1 se A1 „ A2
& A1
¤
A se A2 „ A1 , A1 A2 A
A2 % H2 altrimenti
% A2
1
A2
se A2 „ A1
se A1 „ A2
altrimenti
sono insiemi aperti. In particolare TpΣq è un insieme aperto.
Considerando la pseudometrica banale
ρpt, t1 q "
0 se t, t1 hanno la stessa altezza
1 altrimenti
su T0 pΣq, si ottiene che la metrica maxtρ, ds u è ancora un’ultrametrica limitata in accordo con la quale una sequenza ptn qnPN P T0 pΣq è di Cauchy se
e solo se è di Cauchy per ds e, per n sufficientemente grande, ogni tn ha la
stessa altezza.
Dunque, il completamento di pT0 pΣq, maxtρ, ds uq è lo spazio Th pΣq degli alberi con altezza finita, ma possibile larghezza infinita.
In seguito si userà come alfabeto di etichettatura l’insieme
CAPITOLO 5. λ-CALCOLO INFINITARIO E LUDICA COMPUTAZIONALE54
ΣV
¤
¤
N
tλx|x P Vinj
u t@u
e come distanza su TpΣq
d maxtρ, ds u
Si può definire per induzione sui termini una famiglia di ultrametriche:
Definizione 5.11 Due termini si definiscono isocefali se sono o uguali o
entrambi astrazioni o entrambi applicazioni.
Dati 0 γ1 , γ2 ¤ 1 si definisce un’ultrametrica d per induzione sui termini:
dpt, t1 q $
discreta
'
'
'
'
'
&1
se
se
o
se
t, t1 P Λ08
t, t1 non sono isocefali
hanno differente altezza
t λx.t1 , t1 λx.t11
'
γ1 dpt1 , t11 q
'
'
!
!
1 ))
'
'
piqq
% γ2 max dpt1 , t1 q, supiPN d(u(i),u
se t t1 u, t1 t11 u1
i
1
1
2
Nel caso dell’astrazione si utilizza l’α-equivalenza per riscrivere t e t1 in modo
tale che le variabili astratte coincidano.
Osservazione: Ponendo γ1 γ2 1{2, si ottiene d maxtds , ρu. Inoltre,
tutte le metriche definite sopra sono uniformemente equivalenti, quindi i
valori γ1 , γ2 non hanno importanza.
Nei risultati che seguono, si indicherà con δ la metrica induttiva ottenuta con
γ1 γ2 1.
Lemma 5.12 Come sottoinsieme di pTpΣq, dq, Λ8 è chiuso.
Dimostrazione:
Sia t un albero che non è un termine. Allora t contiene qualche anomalia, un nodo etichettato da una variabile che non è una foglia o un
nodo etichettato da λx che ha più di un fratello. Tale anomalia occorre
ad una certa posizione a P P. Allora esiste ¡ 0 tale che a P A , ogni
palla aperta centrata in t contiene la stessa anomalia, ciò dimostra che
TpΣq å Λ8 è aperto. Dunque si conclude che Λ8 è chiuso. Lemma 5.13 Per ogni t P Λ8 e n P N, esiste rtn s P Λp tale che
δ prtsn , tq 2n
CAPITOLO 5. λ-CALCOLO INFINITARIO E LUDICA COMPUTAZIONALE55
Dimostrazione:
Si definisce rtn s per induzione si t:
- se t P Λ08 , allora rtsn
-
t per ogni n P N e t è finito per ipotesi;
se t λx.t1 , allora rtsn λx.rt1 sn . Per induzione, rtsn è finito;
se t t1 u, allora rtsn rt1 sn xrup0qsn , . . . , rupn 1qsn y, che per
induzione è finito.
La disuguaglianza si domostra per induzione su t:
- se t P Λ08 , allora
dpt, rtsn q dpt, tq 0 2n per ogni n P N;
- se t λx.t1 , allora
dpt, rtsn q dpλx.t1 , λx.rt1 sn q 12 dpt1 , rt1 sn q 12 2n 2n1 2n;
- se t t1 u, allora
dpt, rtsn q dpt1 u, rt1 sn xrup0qsn , . . . , rupn 1qsn yq !
!
))
piqsn q
21 max dpt1, rt1snq, supiPN d(u(i),[u
i
1
2
!
!
2n
2i 1
))
))
!
!
12 max 2n, supiPN 2ni1 12 2n 2n1 2n. Proposizione 5.14 pΛ8 , δ q è il completamento metrico di pΛp , δ q
1
max
2
2n , supiPN
Dimostrazione:
Si è visto che pΛ8 , dq è completo; dunque poichè Λ8 è chiuso e δ è uniformemente equivalente a d, allora anche pΛ8 , δ q è completo. Dal momento che Λp è denso in Λ8 per il lemma precedente, si può concludere
la tesi per unicità di completamento. 5.1.2
Sottocalcolo affine
Definizione 5.15 (Termine affine) Un termine t P Λ8 è affine se ogni
variabile, libera o legata, appare al massimo una volta in t, in particolare
t : K
|
| txt1, . . . , tny
indica l’i-esima variabile del sistema con i P N, xi xj
xi
|
λx.t
dove xi
per ogni
i j e x la sequenza infinita di tutte le varibili indicizzate da i.
aff
aff aff
Si denota con Λ8 , Λp e B pΛ8 q rispettivamente l’insieme dei termini affini, l’insieme dei termini affini finiti e l’insieme di tutte le sequenze dei
termini affini di altezza limitata.
CAPITOLO 5. λ-CALCOLO INFINITARIO E LUDICA COMPUTAZIONALE56
L’affinità è chiaramente preservata per riduzione, in particolare si indica con
pλx.tqu Ñ tru{xs
la riduzione in cui xi Ñ upiq per ogni i P N.
Ogni termine affine, analogamente al paragrafo precedente, si può vedere
come un albero parziale etichettato, ovvero una funzione
t : N
¤
Ñ Σ tKu
in cui N rappresenta le posizioni, ognuna determinata da una sequenza di
interi.
5.1.3
Uniformità e isomorfismo con il lambda calcolo
Ci sono sicuramente molti più termini in Λaff
8 rispetto all’usuale λ-calcolo.
Per poter costruire un isomorfismo è necessario ridurre l’insieme, si definisce
quindi una relazione di equivalenza per cui si avrà pΛaff
8 { , ñq pΛ, Ñβ q.
Definizione 5.16 (Uniformità) Si definisce la più piccola relazione di
aff
equivalenza parziale, detta uniformità, su Λ8 tale che:
xj per ogni variabile x e i, j P N;
- se t t1 , allora λx.t λx.t1 , per ogni variabile x;
- se t t1 e u, u’ sono tali che upiq u’pi1 q per ogni i, i1 P N, allora
tu t1 u’.
Un termine t è uniforme se t t e si denota con Λu8 l’insieme dei termini
- xi
uniformi.
Intuitivamente la relazione uguaglia termini che sono uguali a meno di permutazioni dei sottotermini. In particolare, sono uguali tutte le occorrenze
della stessa variabile: mentre si distinguono due occorrenze di x indicizzandolo, xi e l’altra xj (i j), non importa quale ha indice i e quale j.
Osservazioni:
- Tutti i termini finiti non sono uniformi: infatti un termine finito txuy
viene visto come txu, K, . . . , K, . . .y in Λaff
8 e chiaramente
txuy txu, K, . . . , K, . . .y, in quanto K non è uniforme a nessuno.
CAPITOLO 5. λ-CALCOLO INFINITARIO E LUDICA COMPUTAZIONALE57
- Per quanto detto nel punto precedente, un termine uniforme non contiene K.
- Se tu è uniforme, allora ogni upiq ha la stessa altezza, quella per esempio
di up0q. Quindi tutti i termini uniformi hanno altezza finita.
- L’uniformità non è stabile per riduzione: se ho un termine uniforme
txu, u, . . .y e u ; u’
txu, u, . . .y ; txu’, u, . . .y
non si può affermare che txu’, u, . . .y sia uniforme. Per risolvere il
problema si sostituiscono tutte le u con la loro riduzione u’ contemporaneamente, e allora sarà facile vedere che txu’, u’, . . .y è anche lui
uniforme.
Definizione 5.17 (Riduzione infinitaria) Si definiscono ñk le relazioni
aff
su Λ8 con k P N come le più piccole relazioni che soddisfano:
- pλx.tqu ñ0 tru{xs, ovvero per k 0 è una semplice riduzione di testa
che corrisponde a un singolo passo di riduzione;
- se t ñk t1 , allora λx.t ñk λx, t1 ;
- se t ñk t1 , allora tu ñk t1 u;
- se tu P Λu8 e up0q ñk u10 , per uniformità la stessa riduzione può essere
fatta per tutti gli upiq (i P N), ottenendo il termini u1i .
Se si pone u’piq ñk u1i per ogni i P N, allora tu ñk 1 tu’.
Si denota con
ñ l’unione di tutte ñk , per k P N.
Proposizione 5.18 Sia t P Λu8 , allora:
- t ñ t1 implica che t1
P Λu8;
- inoltre, per tutti u t, se u ñ u1 , allora u1
t1.
Come visto nell’osservazione, la proposizione afferma che l’uniformità è stabile sotto ñ e quindi che tale relazione è compatibile con le classi di equivalenza
di . Quindi, l’insieme pΛu8 { q può essere dotato della riduzione (one step)
ñ, si vedrà che questo è esattamente l’usuale λ-calcolo non lineare.
CAPITOLO 5. λ-CALCOLO INFINITARIO E LUDICA COMPUTAZIONALE58
Teorema 5.19 (Isomorfismo)
pΛu8{ , ñq pΛ, Ñβ q
nel senso di Curry-Howard, ovvero esistono due mappe
xxyy : Λu8 Ñ Λ
tali che per tutti M P Λ e t P Λu8
1.
2.
3.
4.
rrss : Λ Ñ Λu8
xxrrM ssyy M ;
rrxxtyyss t;
M Ñβ M 1 implica rrM ss ñ rrM 1 ss;
t ñ t1 implica xxtyy Ñβ xxt1 yy.
Le due mappe dell’isomorfismo sono entrambe definite per induzione.
5.2
Ludica computazionale e termini infinitari
In questa sezione si presenta la ludica computazionale introdotta da Terui [22], la quale riprende concetti legati alla ludica di Girard [10]. Si definiscono in particolare i disegni, oggetti principali della ludica, visti come
termini infinitari.
Definizione 5.20 (Termine Sintetico) Si definiscono i seguenti insiemi
di termini:
N0
tKu
Nh
1
N
tλx1, . . . , xn.t|t P P h, xi P x P Vinj
, n P Nu
P0
tzu
Ph
1
ttu1, . . . , un.t|t P N h, ui P pN hqN, n P Nu
Un termine
” h sintetico”è unh termine affine (Definizione 5.15) di N
N hN e P hP .
Sia in N h 1 che in P h 1 , n indica l’ arità del termine.
”
P, con
CAPITOLO 5. λ-CALCOLO INFINITARIO E LUDICA COMPUTAZIONALE59
Osservazione: I termini di arità 0 si indicano con .t e t., rispettivamente
quello negativo e positivo.
f
L’insieme dei termini sintetici non è altro che un’estensione di Λaf
8 a cui
va aggiunto il simbolo z, detto demone, che nella ludica indica la regola per
cui una dimostrazione risulta valida supponendo la conclusione di tale regola
vera oppure si può anche interpretare come un elemento di errore nella dimostrazione.
Introducendo una versione di riduzione inifinitaria (Definizione 5.17) in parallelo, ovvero in cui si effettuato più sostituzioni contemporaneamente, si
può definire la forma normale dei termini sintetici. Si presenta un algoritmo
di ricerca della forma normale che permette di costruire una successione di
termini, la quale all’infinito o diventa stazionaria o restituisce un termine
ancora da ridurre e quindi diverge.
Si definisce per i temini in N
”
P, la riduzione
pλx1, . . . , xn.tqu1, . . . , un ; tru1{x1s . . . run{xns
zu ; z @u P N
e dato un termine sintetico t, si calola nf n ptq, il termine ottenuto all’n-esimo
passo di riduzione, se è possibile ridurre t, altrimenti si ha nf n ptq Ω, tale
simbolo è detto divergenza e indica appunto l’impossibilità di ridurre t.
La successione tnf n ptqunPN viene costruita per induzione sui termini:
nf 0 ppλ~x.t0 q~uq Ω
nf
n 1
ppλx1, . . . , xl .t0qu1, . . . , umq "
nf n pt0 ru1 {x1 s . . . rum {xm sq se l m
Ω
altrimenti
con
nf n ptq t se t z, K
nf pλ~x.t0 q n
"
λ~x.u se nf n pt0 q u Ω
Ω
se nf n pt0 q Ω
nf n pxu1 , . . . , un q xv1 , . . . , vn con xvk piq nf n puk piqq
per ogni 1 ¤ k ¤ m e i P N
nf n pK~uq Ω
CAPITOLO 5. λ-CALCOLO INFINITARIO E LUDICA COMPUTAZIONALE60
Dato un termine sintetito t, se tnf n ptqunPN è stazionaria in u, ovvero esiste
N P N tale che nf n ptq u per ogni n ¡ N , allora la forma normale di t,
nf ptq, sarà proprio u; altrimenti, nf ptq Ω se t è positivo e nf ptq K se
t è negativo. Con nf n ptq si cerca la forma normale del termine t riducendo
ripetutatamente il redesso più a sinistra.
Definizione 5.21 (Disegno) Un disegno è un termine sintetico normale,
in particolare è un disegno positivo se appartiene a P e un disegno negativo
se appartiene a N .
L’insieme dei disegni si indica con D.
Definizione 5.22 (Disegno Atomico) Un disegno si dice atomico se è
positivo ed è o z o ha come unica variabile libera z, oppure è negativo e
chiuso.
Definizione 5.23 (Ortogonalità) Siano t, u due disegni atomici, con t positivo e u negativo. Si dice che t, u sono ortogonali, si indica con t K u (o
u K t, la relazione è simmetrica considerando sempre t positivo e u negativo), se nf ptru{z sq z. Dato un insieme di disegni atomici A, si definisce
il corrispondente insieme ortogonale
AK
tt1 P D| per ogni t P A, t1 K tu.
Osservazione: Per ogni disegno u negativo, si ha che z K u. Non esiste
invece alcun disegno negativo ortogonale a tutti i positivi, infatti se t K u,
per avere u negativo e t z, t e u devono avere la stessa arità.
Proposizione 5.24 Gli insiemi ortogonali soddisfano le seguenti proprietà:
(i) A „ AKK ;
(ii) A „ B implica B K
(iii) AKKK
„ AK;
AK.
Dimostrazione:
(i) Sia t1 P A, per definizione per ogni t P AK si ha che t1 K t, segue
che anche t1 P AK . Allora per ogni t2 P AKK si ha che t2 K t1 ,
dunque t1 P AKK . Per l’arbitrarietà di t1 , si ha la tesi.
CAPITOLO 5. λ-CALCOLO INFINITARIO E LUDICA COMPUTAZIONALE61
(ii) Siano B K tt P D| per ogni bi P B, t K bi u e AK tt P D| per ogni ai
A, t K ai u. Sia t P B K , allora t K bi per ogni bi P B, poichè A „ B
si ha che t K ai per ogni ai P A, segue che t P AK e quindi la tesi
per arbitrarietà di t.
(iii) Per la (i) AK „ pAK qKK e per la (ii), poichè A
l’inclusione inversa pAKK qK „ AK . „
AKK , segue
Gli insiemi ortogonali permettono di dare una definizione di tipo che estende
quella data dal sistema F e dal λ-calcolo tipato semplice.
Definizione 5.25 (Tipo) Si definisce innanzitutto un pre-tipo come un insieme non vuoto di disegni atomici della stessa polarità.
Un tipo è un pre-tipo A tale che AKK A e la sua polarità è quella dei
disegni che contiene.
Osservazione: È immediato vedere che l’insieme di tutti i disegni atomici
negativi T e 0 tzu sono entrambi tipi, ortogonali l’uno con l’altro.
Un tipo si dice proprio se è diverso da T e 0. In particolare gli elementi
( z) di un tipo proprio A hanno tutti la stessa arità ed è l’arità di A.
Segue banalmente che l’arità di AK è la stessa di A.
Osservazione: Si notiche z è presente in tutti i tipi positivi.
Definizione 5.26 (Tensore) Siano t, u disegni atomici positivi. Si definisce
"
z~u~v se t z~u e u z~v
tbu
z
se uno tra t, u è uguale a z
Siano A, B due tipi positivi, si definisce:
A b B tt b u|t P A, u P B u
A b B pA b B qKK .
Osservazione: Se A, B sono entrambi propri di arità n e m rispettivamente,
allora A b B è proprio di arità n m.
Lemma 5.27 (Completezza interna del Tensore) Per tutti i tipi positivi A, B si ha
AbB AbB
P
CAPITOLO 5. λ-CALCOLO INFINITARIO E LUDICA COMPUTAZIONALE62
Dimostrazione:
Se uno tra A, B non è proprio, si ha A b 0 A b 0 0 0KK .
Siano quindi A, B entrambi propri, allora
(…) per la proprietà (i) degli insiemi ortogonali si ha
A b B pA b B qKK A b B;
(„) sia s P A b B
“
∗ se s z poichè z P A B e t b z z b u z, segue che
s P A b B;
~ l’arità di s è m n, quindi s z u~1 . . . u~m v~1 . . . v~n
∗ se s z w
con t z u~1 . . . u~m e u z v~1 . . . v~n . Resta da far vedere che
t P A e u P B.
Definizione 5.28 (Tipo Esponenziale) Sia A un tipo proprio negativo.
Si definisce
:A tzu| per ogni n P N, upiq P Au ”tzu
!A p:AqKK .
Lemma 5.29 (Completezza interna dell’Esponenziale) Per tutti i tipi
negativi propri A, si ha
!A :A.
Dimostrazione:
(…) per la proprietà (i) degli insiemi ortogonali si ha
:A „ p:AqKK !A;
(„) sia t P!A:
∗ se t z allora per definizione z P :A;
∗ poichè l’arità di !A è 1, si può supporre t zu ed è sufficiente
dimostrare che upnq P A per ogni n P N.
Siano u1 zv P AK e s λx.xn~v con xn xpnq, allora
s P p:AqK q.
Infatti, sia w una sequenza di termini di A, si ha
nf ppsqwq nf pwpnq~vq nf pu1 rwpnq{z sq z
in quanto wpnq K u1 . Ma trs{z s ; upnq~v u1 rupnq{z s ha
forma normale z per l’ipotesi t P!A p:AqKK , quindi
upnq K u1 .
Per arbitrarietà di u1 e n, upnq P A per ogni n P N. CAPITOLO 5. λ-CALCOLO INFINITARIO E LUDICA COMPUTAZIONALE63
Per dualità si definiscono i tipi:
A ` B pAK b B K qK
?A p!AK qK .
5.3
Derivazioni in MELLP e termini di Λ8
Con il sistema di regole della Logica Lineare Polarizzata Moltiplicativa ed
Esponenziale a cui si aggiunge la regola del demone (MELLPz ) si ottengono le derivazioni rappresentabili con i disegni. In questa sezione si presenta
f
la corrispondenza considerata in [18] tra MELLPz e i termini di Λaf
8 .
Il sistema logico di MELLPz è data dalle seguenti regole:
Γ$Σ
Γ$A
(z)
A, Γ $ Σ
(cut)
Γ$Σ
Γ$Σ
(1 $)
1, Γ $ Σ
Γ$1
($ 1)
A, B, Γ $ Σ
(b $)
A b B, Γ $ Σ
Γ$A
Γ$B
($ b)
Γ$AbB
!AK , Γ $ A
(! $)
!AK , Γ $
A, Γ $
($!)
Γ $!AK
Definizione 5.30 (Seguente Polarizzato) Un seguente polarizzato è un’espressione della forma Γ $ Σ in cui Γ e Σ sono sequenze finite di formule
positive, con Σ che ha al massimo una formula.
CAPITOLO 5. λ-CALCOLO INFINITARIO E LUDICA COMPUTAZIONALE64
Definizione 5.31 (Interpretazione) L’ interpretazione di una formula A,
denotata con rrAss, è un tipo definito per induzione su A:
rr1ss 1 rrKss 1K
rrA b B ss rrAss b rrB ss rrA ` B ss prrAssK b rrB ssKqK
rr!Ass !rrAss rr?Ass p!rrAssKqK
Definizione 5.32 (Disegno Funzionale) Un disegno funzionale è un disegno negativo della forma λ~x.z~u, tale che z è l’unica variabile libera.
Definizione 5.33 (Tipi Funzione) Dati A, B due tipi positivi, con A di
arità n. Si definisce A $ B come segue:
- A $ 0 è AK ;
- se B è proprio, allora A $ B è l’insieme dei disegni funzionali s tali
che per ogni t P A e u1 P B K si ha nf ptrsru1 {z s{z sq z.
Ogni regola di MELLPz può essere associata al tipo della sua interpretazione che non è altro che un disegno, ovvero un termine infinitario normale.
Questa correlazione si può vedere nel senso di Curry-Howard.
Un seguente polarizzato Γ $ Σ si interpreta interpreta nel modo seguente:
• se Γ C1 , . . . , Cn allora
per n 0, rrΓss 1;
• se Σ B allora
quindi si definisce
rrΓss rrC1ss b . . . b rrCnss e in particolare
rrΣss rrB ss, altrimenti rrΣss 0;
rrΓ $ Σss rrΓss $ rrΣss
L’interpretazione di una dimostrazione π di MELLPz di un seguente
Γ $ Σ è un disegno rrπ ss definito per induzione sull’ultima regola di π. Si ha
allora la seguente corrispondenza.
Γ$Σ
pzq
ù rrπ ss λ~c.z dove ~c è una sequenza di supervariabili in relazione
con le formule in Γ.
CAPITOLO 5. λ-CALCOLO INFINITARIO E LUDICA COMPUTAZIONALE65
.
π 1 ..
.
π 2 ..
Γ$A
A, Γ $ Σ
Γ$Σ
(cut)
ù rrπ ss λ~c.trλ~x.v {z s, con rrπ 1 ss λ~c.t e rrπ 2 ss λ~x~c.v interpretazioni delle dimostrazioni le cui conclusioni sono le premesse della regola,
in cui ~x è una sequenza di arità rrAss e ~c di arità rrΓss.
.
π 1 ..
Γ$Σ
p1 $q
1, Γ $ Σ
ù rrπ ss rrπ 1 ss dove π 1 è la dimostrazione la cui conclusione è la
premessa della regola.
Γ$1
p$ 1q
ù rrπ ss λ~c.z con ~c sequenza di supervariabili in relazione con le
formule di rrΓss.
.
π 1 ..
A, B, Γ $ Σ
A b B, Γ $ Σ
pb $q
ù rrπ ss è definita come per p1 $q.
.
π 1 ..
.
π 2 ..
Γ$A
Γ$B
Γ$AbB
p$ bq
ù rrπ ss λ~c.t b u con rrπ 1 ss λ~c.t e rrπ 2 ss λ~c.u interpretazioni
delle dimostrazioni le cui conclusioni sono le premesse della regola, in
cui ~c è una sequenza di arità rrΓss.
.
π 1 ..
!AK , Γ $ A
!AK , Γ $
p! $q
CAPITOLO 5. λ-CALCOLO INFINITARIO E LUDICA COMPUTAZIONALE66
~1 con rrπ 1 ss λ~x~c.z~u interpretazione della dimoù rrπ ss λ~x~c.x0 u
strazione la cui conclusione è la premessa della regola, in cui sostituendo
~1 in cui x0 è l’unica variabile libera.
ogni xI ~xpiq con xi 1 si ottiene u
.
π 1 ..
A, Γ $
Γ $!AK
p$!q
ù rrπ ss λ~c.z xλ~x.s0 , λ~x.s1 , . . .y con rrπ 1 ss λ~x~c.s interpretazione
della dimostrazione la cui conclusione è la premessa della regola, dove
~x e ~c sono sequenze di astrazioni di supervariabili di arità rrAss e rrΓss
rispettivamente. Fissando in : N Ñ N infinite iniezioni le cui coppie
pk, inpkqq sono disgiunte per ogni n P N, si definiscono le sn come
i disegni ottenuti da s sostituendo ogni variabile ck piq (se presente)
con ck p“
in piqq, si ha che sn s (Definizione 5.16) per ogni n P N e
f v psn q f v psm q H per ogni n m.
Se un termine sintetico rappresenta una dimostrazione, esso è sempre normalizzabile in un disegno. In generale, tutte le dimostrazioni, cut-free o no,
possono essere interpretate dai disegni e questo permette di avere una corrispondenza tra dimostrazioni e termini infinitari analoga a quella di CurryHoward.
Ovviamente non tutti i disegni sono interpretazioni di dimostrazioni MELLPz .
Si introduce a tal proposito una nozione di validità dei disegni.
Definizione 5.34 (Validità) Un disegno è valido se è uniforme e daimonfree, ovvero non contiene z come sottotermine. La validità induce una
nozione di verità sui tipi: un tipo è vero se contiene un disegno valido.
Al massimo uno tra A e AK può essere valido, infatti se t P A e t1 P AK ,
poichè t K t1 uno dei due deve avere un sottotermine z, dal momento che
non si può ottentere per riduzione. Permette inoltre di dare una nozione di
correttezza per MELLPz .
Teorema 5.35 (Correttezza) Sia π una dimostrazione MELLPz di
Γ $ Σ. Allora:
1.
rrπss è uniforme, è un disegno non appena π è cut-free ed è valido non
appena π è in MELLPz ;
2. se π0 è una forma cut-free di π, allora
3.
rrπ0ss P rrΓ $ Σss.
rrπss ñ rrπ0ss;
CAPITOLO 5. λ-CALCOLO INFINITARIO E LUDICA COMPUTAZIONALE67
Come corollario immediato del teorema si ha la completezza di MELLPz .
Teorema 5.36 (Completezza per MELLPz ) Sia s P rrΓ
me. Allora esiste una dimostrazione π di MELLPz tale che
rrπss s.
$ Σss unifor-
Capitolo 6
Il λ-calcolo infinitario è
elementare
In questo capitolo si introduce la logica elementare [3], ovvero il sistema logico
in cui tutte le dimostrazioni sono programmi eseguibili in tempo elementare.
In particolare si mostra che, a partire da Λ8 , si può costruire un λ-calcolo
infinitario lineare elementare, presentato da Mazza in [19].
I termini infinitari servono per rappresentare dati del tipo !A, che contengono
cioè infinite copie di A: dal punto di vista della programmazione, essi indicano
celle di memoria persistente a cui si può accedere un numero infinito di volte
durante l’esecuzione di un programma. Per esprimere tali dati nella logica,
si usa la logica lineare. In particolare si presenta una modifica di Λ8 e
si introduce un calcolo infinitario lineare; infine si mostra, a partire dalla
dimostrazione nel caso polinomiale presentata da Mazza [19], che tale sistema
di calcolo è elementare.
6.1
Logica lineare elementare
Frammenti della logica lineare possono essere visti come linguaggi di programmazione in grado di rappresentare tutte e sole le funzioni di una data
classe di complessità. Chiedersi se esiste un limite alla complessità delle funzioni definibili tramite la logica equivale ad analizzare la complessità della
procedura di cut-elimination. Infatti, l’esecuzione di un programma nella
logica non è altro che l’eliminazione delle regole del cut della derivazione.
La logica lineare elementare (ELL) è un sottosistema della logica lineare
che permette di descivere esattamente la classe delle funzioni elementari. La
classe delle funzioni elementari, introdotte da Kalmàr [16], è il più piccolo insieme E contenente le funzioni di base (costanti, proiezione, addizione,
68
CAPITOLO 6. IL λ-CALCOLO INFINITARIO È ELEMENTARE
69
moltiplicazione e sottrazione) e chiuso per composizione, prodotti e somme
limitati. Le funzioni elementari non sono altro che le funzioni che si possono
implementare in tempo elementare, cioè la classe di funzioni calcolabili da
una macchina di Turing in un numero di passi limitato da una qualche funzione elementare.
Si considera la variante intuizionista anche per ELL, che si indica con IELL.
Il sistema di regole di IELL è il seguente:
A$A
pidq
Γ$A
∆, A $ B
Γ, ∆ $ B
Γ, A $ B
Γ$A(B
pcutq
p( Rq
Γ$A
∆, B $ C
Γ, ∆, A ( B $ C
p( Lq
Γ$A
p!q
!Γ $!A
Γ$A
Γ $ @X.A
p@Rq
Γ, ArB {X s $ C
Γ, @X.A $ C
Γ$B
Γ, !A $ B
p@Lq
pwq
!A, !A, Γ $ A
pcq
!A, Γ $ A
In particolare un λ-termine M è tipabile in IELL con tipo Γ $ M : A, in cui
il contesto Γ è un’applicazione da variabili a formule ed è definito su tutte le
variabili libere di M , se esiste una derivazione nel sistema:
x:A$x:A
pidq
Γ $ M1 : A
∆, x : A $ M2 : B
Γ, ∆ $ M1 rM2 {xs : B
pcutq
CAPITOLO 6. IL λ-CALCOLO INFINITARIO È ELEMENTARE
Γ, x : A $ M : B
Γ $ λx.M : A ( B
70
p( Rq
Γ$x:A
∆, M1 : B $ M2 : C
Γ, ∆, λy.N : A ( B $ M2 rpN qx{M1 s : C
p( Lq
Γ$M :A
p!q
!Γ $!M :!A
Γ$M :A
Γ $ M : @X.A
p@Rq
Γ, x : ArB {X s $ M : C
Γ, x : @X.A $ M : C
Γ$M :B
Γ, x :!A $ M : B
p@Lq
pwq
x :!A, y :!A, ∆ $ M : B
z :!A, ∆ $ M rz {x, z {y s : B
pcq
Dal momento che l’insieme delle funzioni elementari E è chiuso per composizione, per ogni m l’iterazione m volte di un esponenziale 2m
n è in E,
dove
"
n
se m 0
m 1
m
2n 22n se m ¡ 0
In particolare, si ha il seguente risultato:
Proposizione 6.1 Se f
P E allora esiste m P N tale che per ogni x
f pxq ¤ 2m
n
con n dimensione di x.
In ELL si ha che la procedura di cut-elimination è limitata da 2m
n per
qualche m, dove n è legato alla grandezza dell’input.
CAPITOLO 6. IL λ-CALCOLO INFINITARIO È ELEMENTARE
6.2
71
λ-calcolo infinitario lineare
Si definisce un λ-calcolo infinitario lineare, un calcolo infinitario a partire da
quello descritto nel Capitolo 5, in cui però si distinguono due tipi di variabili: le variabili lineari e le variabili non-lineari, quest’ultime con occorrenze
distinte tramite indici (x1 , x2 , . . .). Ogni occorrenza di variabile compare al
massimo una volta in un termine. L’utilità delle variabili non-lineari è quello
di riuscire a descrivere formule di tipo !A.
Definizione 6.2 (Termini) Dati due insiemi disgiunti di variabili lineari,
ta, b, c, . . .u, e variabili non-lineari, tx, y, z, . . .u, si definiscono i pre-termini
come segue.
t, u : K
|
dove i P N e
a
|
|
xi
p, q : a
λp.t
|
x
| ptqu |
|
tbu
|
u
pbq
x indica la variabile x di occorrenze xi e u una sequenza finita di termini,
xup0q, . . . , upn 1qy con upiq K per ogni i ¥ n. u si dice box.
Le occorrenze di ogni variabile (lineare e non-lineare) compare al massimo
una volta in un termine. Se x(risp. a) appare in p, si scrive che x P p(risp.
a P p). In particolare x P p indica che tutte le occorrenze xi di x sono legate
in λp.t (usando la stessa definizione data precedentemente di variabili libere
e legate). Le variabili libere di u sono non-lineari.
f
L’insieme dei termini ottenuti si indica con lΛaf
p .
Definizione 6.3 (Sostituzione) Data la relazione , definita nel modo seguente:
. t
a per ogni t;
. t
x se t u;
. da t
peu
q segue che t b u
Allora si definisce tru{ps se u
p b q.
p e si ha che:
. tru{as è la sostituzione usuale;
. tru{xs è il termine t in cui ogni occorrenza xi viene sostituita con upiq;
. tru1 b u1 {p1 b p2 s tru1 {p1 sru2 {p2 s.
CAPITOLO 6. IL λ-CALCOLO INFINITARIO È ELEMENTARE
72
f
Definizione 6.4 (Contesto) Dato un termine t P lΛaf
si definisce il conp
testo debole S di t
S : |
λp.S
| pS qu |
Sbu
|
ubS
dove indica il contesto vuoto nel caso in cui il termine sia una variabile
(lineare o non-lineare).
Il contesto di t è dato da:
C : S
| xup0q, . . . , C, . . . upn 1qy
Osservazione: Un termine u è sottotermine di t (u „ t) se esiste un contesto
C tale che t C rus, dove C rus è il termine ottenuto sostituendo u a nel
contesto C.
Definizione 6.5 (Riduzione) La riduzione di un termine t si indica con
Ñ ed è l’unione di due operazioni Ñs , riduzione debole, e ù, riduzione
nella box, definite nel modo seguente:
. pλp.tqu Ñs tru{ps se e solo se u
p;
. t Ñs t1 allora S rts Ñs S rt1 s;
. u ù up0q.
Il termine della forma pλp.tqu u p con si dice redesso. Ogni passo di riduzione Ñs è chiaramente associato a un redesso che è detto focalizzato dal
passo di riduzione.
Si indica con Ñ la chiusura riflessiva-transitiva di Ñ e con Ñl la composizione di esattamente l P N passi di Ñ.
Le definizioni di distanza e uniformità defnite nel Capitolo 5 si estendono
f
a lΛaf
considerando come variabili anche quelle lineari e indicando l’astrap
f
zione con λp invece di λx. Analogamente si indica con lΛaf
8 il completamento
af f
metrico di lΛp rispetto alla metrica d.
Usando la Proposizione 6.1, si vuole dimostrare che lΛ8 { è elementare.
Per arrivare a questa conclusione è necessario introdurre il concetto di stratif
ficazione che permette di analizzare i termini di lΛaf
8 in base alla profondità
nell’albero che li rappresenta delle box, da cui si può dedurre il risultato
cercato.
f
Definizione 6.6 (Box-profondità) Dato un termine t P lΛaf
8 si definisce
box-profondità :
CAPITOLO 6. IL λ-CALCOLO INFINITARIO È ELEMENTARE
73
- di una specifica occorrenza di un sottotermine u di t, denotata con du ptq,
il numero delle box nidificate di t che contengono u;
- di t, denotata con dptq, il Suppdu ptqq con u sottotermine di t;
- relativa di un’occorrenza xi che appare (libera o legata) in t, denotata con
rdxi ptq, nel modo seguente:
• rdxi ptq dxi ptq se xi è libera in t;
• rdxi ptq dxi ptq dλp.u ptq se xi è legata in t e quindi esiste un
sottotermine λp.u di t tale che x P p e xi appare in u.
Definizione 6.7 (Termine stratificato) Un termine t è stratificato se,
per ogni xi „ t, rdxi ptq 1.
L’insieme dei termini stratificati si indica con lΛs8 e lΛs0
8 l’insieme dei termini stratificati che non hanno variabili libere non-lineari.
Osservazione: I sottotermini di termini stratificati non sono necessariamente
stratificati. Per esempio: xx0 y P lΛs8 ma x0 R lΛs8 .
Lemma 6.8 Siano t, u P lΛs8 e u p. Si suppone che x P p e x libera in t
implica che dxi ptq 1 per ogni i P N. Allora, per ogni v „ u
dv ptru{psq dv puq (con v che non viene cancellata dalla sostituzione).
Proposizione 6.9 (La riduzione preserva la stratificazione) Se t P lΛs8
1
1
s0
e t Ñs t1 , allora t1 P lΛs8 . Inoltre, Se t P lΛs0
8 e t ù t , allora t P lΛ8 .
Dimostrazione:
Sia xi „ t1 , è sufficiente mostrare che rdxi pt1 q 1. Dal momento che
con la riduzione non si crea alcuna occorrenza di varibile, si ha xi „ t
e per ipotesi rdxi ptq 1.
Sia t S rpλp.uqv s e t1 S rurv {pss
– se xi ı̀n S, segue automaticamente il risultato.
– se xi
R p, si hanno due casi
1. xi „ u, il lemma segue a prescindere dalla stratificazione;
2. xi „ v, allora per la stratificazione e per il Lemma 6.8 si
ottiene
dxi purv {psq dxi pv q
Nel caso in cui x sia libera in v, si conclude la tesi; altrimenti
si ha che λq.v „ v lega x, applicando il Lemma 6.8 si ha
dλq.v purv {psq dλq.v pv q
CAPITOLO 6. IL λ-CALCOLO INFINITARIO È ELEMENTARE
74
Si conclude la tesi per definizione di box-profondità relativa.
Definizione 6.10 (Grandezza) Dato t P lΛ8 , si definisce la grandezza di
t, denotata con |t| nel modo seguente:
|K| : |a| : |u| : 1 |xi| : 1 i
|λp.t| : 1 |p|0 |t| |ptqu| : |t b u| : 1 |t| |u|
con |a|0 : |x|0 : 1 e |p b q |0 : 1 |p|0 |q |0 .
Lemma 6.11 Sia t P lΛs8 di altezza finita e t Ñs t1 . Allora
1. dpt1 q ¤ dptq;
2. |t1 | |t|.
Dimostrazione:
1. Sia t S rpλp.uqv s e t1 S rurv {pss, si assume che dpt1 q ¡ 0 (nel
caso in cui dpt1 q 0 è banale).
Dalla definizione di box-profondità si ha allora che esiste un’occorrenza xi „ t1 tale che dxi pt1 q è massimale con x R p. Poichè
allora xi appare in S o in u, si conclude per il Lemma 6.8.
2. Procedendo per induzione su p si dimostra che |urv {ps| ¤ |u| |v |.
Il caso piè rilevante è con p x e v v. Per stratificazione si ha
che dxi puq 1 per ogni i P N, segue che i vpiq vengono sostituiti
a profondità 1 e la loro grandezza non è rilevante. Quindi
|urv{ps| |pλp.uqv|.
Il risultato segue per induzione su S. Proposizione 6.12 (Terminazione) Ogni t
temente normalizzabile.
P lΛs08 di altezza finita è for-
Dimostrazione: Si procede per induzione su pdptq, |t|q usando il Lemma 6.11. Definizione 6.13 (Grandezza nella box) Sia t P lΛ8 si definisce la grandezza di t nella box a profondità j, denotata con |t|j per ogni 0 ¤ j ¤ dptq,
nel modo seguente:
CAPITOLO 6. IL λ-CALCOLO INFINITARIO È ELEMENTARE
|K|j |a|j | xi | j "
1
0
"
"
75
1 se j 0
0 altrimenti
j se j 0
altrimenti
|λp.t|j ||pt||j |q|j
"
se j 0
altrimenti
|ptqu|j |t b u| ||tt||jj ||uu||jj 1
"
se j 0
|u| 1°8 |upiq|j1 altrimenti
j 0
Inoltre si ha
|t| se j 0
altrimenti
pq
¸
d t
|t|j.
j 0
Osservazione: In ogni box le occorrenze delle variabili lineari sono in numero
finito, anche se x indica l’insieme di tutte le occorrenze senza porre un limite.
La grandezza
°8 di u è potenzialmente infinita, ma quanto detto garantisce che
la serie j 0 |upiq|j 1 non può divergere.
Definizione 6.14 (Lista di sostituzioni) Data una variabile x non-lineare
e u una box, una sostituzione esplicita è della forma rx : us. Si indica con
σ un elemento dell’insieme delle liste finite di sostituzioni esplicite, dette liste di sostituzione.
Si denota con σσ 1 la concatenazione di tali liste e con la lista vuota.
Si definiscono allora
σ ru{ps:
- ru{ps : ;
prx : usσ1qru{ps : rx : uru{pssσ1ru{ps.
tru{pl s con t, u pre-termini e u p:
- tru{al s : tru{as;
- tru{xl s t;
- tru1 b u2 {pp1 b p2 ql s tru1 {pl1 sru2 {pl2 s.
la lista di sostituzioni rrp : uss con p u:
-
CAPITOLO 6. IL λ-CALCOLO INFINITARIO È ELEMENTARE
-
76
rra : uss : ;
rrx : uss rx : us;
rrp1 b p2 : u1 b u2ss rrp2 : u2ssrrp1 : u1ss.
Definizione 6.15 (Configurazione) Dato un termine t P lΛ8 e σ una lista di sostituzioni, la coppia pt, σ q è detta configurazione. Una configurazione
si denota con c.
Su ogni configurazione si hanno le seguenti regole di riscrittura:
- pS rpλp.tqus, σσ 1 q Ñm pS rtru{pl ss, σ rrp : ussσ 1 q dove u
variabile non-lineare di p compare in σ 1 ;
- pt, σ rx : usσ 1 q Ñe
p e nessuna
prtru{xss, σru{xsσ1q.
dove S è un contesto debole.
Quindi, quando un redesso è focalizzato (Definizione 6.5), la parte lineare delle sostituzioni è eseguita immediatamente, mentre la parte non-lineare viene
mantenuta nella lista di sostituzione ed eseguita successivamente. Infatti, si
ha che t Ñs t1 implica pt, σ q Ñm Ñe pt1 , σ 1 q per ogni σ con σ 1 ottenuta da σ
come visto.
Si denota con Ñc :Ñm Y Ñe .
Definizione 6.16 (Sequenza di riduzioni normale) Una sequenza di riduzione c Ñ c1 è normale se si può decomporre in c Ñm Ñe c1
Si verifica facilmente che in lΛs8 , i passi di riduzione Ñe possono sempre
essere postposti: ovvero se t P lΛs8 e pt, σ q Ñe c1 Ñm c1 , allora esiste c2 tale
che pt, σ q Ñm c2 Ñe c1 .
D’ora in avanti si assume che tutte le occorrenze di λ alla profondità 0 in
un termine t legano variabili distinte. Dal momento che il calcolo è affine tale
caratteristica si mantiene anche dopo ogni passo di riduzione Ñs . Questo ci
da un modo implicito per tenere traccia dei residui durante una riduzione:
un’occorrenza xi in t1 è necessariamente il residuo (unico) di xi in t, se t Ñs t1 .
Definizione 6.17 (Arità) Sia x una variabile legata alla box-profondità 0
di t P lΛs0
8 , cioè esiste λp.u „ t tale che x P p e dλp.u ptq 0.
Sia X ti P N|xi è libera in uu. L’ arità di x in t, denotata con ∇t pxq, è
definita come segue:
• se X è finito, allora ∇t pxq : maxpX q
• se X è infinito, allora esiste un’unica box u „ u che contiene tutte le
occorrenze di x ma in numero finito, più precisamente esiste h P N tale
che xi è contenuta in u per ogni i ¤ k, dunque si ha ∇t pxq : k.
CAPITOLO 6. IL λ-CALCOLO INFINITARIO È ELEMENTARE
77
Definizione 6.18 (Grandezza potenziale di c) Date due variabili x e y
tali che σ σ1 ry : vsσ2 rx : usσ3 ed esistono infinite occorrenze
° di x in
v, si indica con x œσ y. Data c : pt, σ q, si definisce µc pxq : xœσ y ∇t py q.
Sia σ rx1 : u1 s . . . rxn : un s. Allora la grandezza potenziale di c a
profondità j, con j ¥ 1 è definita come segue
n
¸
rcsj : |t|j
µc pxk q|uk |j .
k 1
Lemma 6.19 Sia t P lΛs0
8 e t Ñs t1 , allora
per ogni 1 ¤ j
¤ dptq.
|t1|j ¤ |t|j |t|1|t|
0
Dimostrazione:
Si considera una sequenza normale pt, σ q Ñm pt1 , σ1 q Ñe pt1 , σ 1 q e si
ottiene che |t1 | ¤ |t|. Dunque si osserva che rpt1 , σ 1 qsj |t1 |j . In
particolare si può mostrare che c1 Ñe c2 implica rc1 sj ¤ rc2 sj . Dunque
la grandezza potenziale di pt1 , σ1 q limita la grandezza alla fine della
riduzione. Si conclude osservando che la grandezza potenziale verifica
il limite del lemma. l 1
Teorema 6.20 Sia t P lΛs0
8 e t Ñ t con l P N, allora
|t1| ¤ 2d|tp|tq #
|t| p q
d t
2|t|
2
se d(t)=0
1
altrimenti
ovvero il λ-calcolo infinitario stratificato è elementare.
Dimostrazione:
Si procede per induzione sul numero dei passi di riduzione ù.
t Ñls1 t1 si possono avere due casi:
1. t1 t1 : per il Lemma 6.19 si ha |t1 |j
|t|
segue che |t1 | ¤ |t||t|1 0 ;
¤ |t|j |t|1|t|
0
per ogni j
2. t1 u: si ha quindi che t1 ù t2 Ñl2 t1 con l 1
applicando l’ipotesi induttiva sulla riduzione di t2 si ha
l1
¡ 0,
l2 ,
|t1| ¤ 2d|tpt| q
per il Lemma 6.11 si ha dpt2 q dpt1 q 1 ¤ dptq 1.
Più in generale, |t2 |j |t1 |j 1 per ogni j, quindi si ha che |t2 | °dpt q
j 0 |t1 |j 1 ¤ |t1 | ¤ |t|, quindi si ha la tesi. 2
2
1
Appendice A
Spazi Metrici
Definizione A.1 (Metrica) Dato un insieme X, si dice metrica (o distanza) in X una funzione d che ad ogni coppia di punti x, y diX associa un
numero dpx, y q con le seguenti proprietà:
1. dpx, y q ¥ 0, in particolare dpx, y q 0 se e solo se x y
2. dpx, y q dpy, xq
3. dpx, y q ¤ dpx, z q
lare)
dpz, y q per ogni x, y, z
P X ( disuguaglianza triango-
La coppia pX, dq si chiama spazio metrico.
Osservazione: In un insieme si possono definire più metriche e in generale
metriche diverse definite nello stesso spazio X identificano spazi metrici diversi.
Su un insieme X è sempre possibile introdurre una distanza discreta
dpx, y q "
0 se x y
1 se x y
Tramite la distanza, in uno spazio metrico si possono definire dischi aperti.
Definizione A.2 (Disco Aperto) Dato un punto x0
0,
si dice disco aperto di centro x0 e raggio r l’insieme
P X e un intero r ¡
Dpx0 , rq tx P X : dpx, x0 qxru
Definizione A.3 (Insieme Aperto) Un sottoinsieme di X si dice aperto
(rispetto alla distanza d) se è unione di dischi aperti.
78
APPENDICE A. SPAZI METRICI
79
X e i suoi dischi aperti sono particolari aperti di X.
Definizione A.4 (Distanza Ultrametrica) Si definisce distanza ultrametrica una distanza ottenuta sostituendo la disuguaglianza triangolare con la
seguente
dpx, y q ¤ maxtdpx, z q
dpz, y qu se per ogni x, y, z
PX
detta disuguaglianza ultrametrica. In questo caso la coppia pX, dq costituisce
uno Spazio Ultrametrico.
È facile vedere come la disuguaglianza ultrametrica implichi quella triangolare, ma non viceversa.
Definizione A.5 (Distanze Topologicamente Equivalenti) Due distanze d1 , d2 definite sullo stesso insieme X si definiscono topologicamente equivalenti se definiscono gli stessi insiemi aperti.
Dato uno spazio metrico pX, dq e un intero r ¡ 0 si può definire, per esempio,
una nuova distanza a partire da d topologicamente equivalente:
dr px, y q : rdpx, y q. Per r 1 le due distanze sono diverse e identificano gli
stessi aperti.
Con la distanza di uno spazio metrico si possono dare nuove definizioni
di contiunuità, convergenza etc . . .
Definizione A.6 (Chiusura di un insieme) In uno spazio metrico
” X si
defisce la chiusura di un insieme E „ X come l’insieme E E δE, o
equivalentemente come l’intersezione degli insiemi chiusi che contengono E.
Teorema A.1 Un punto x appartiene a E se e solo se è limite di una
successione xn di punti di E.
Un particolare interesse hanno gli insiemi densi, cioè gli insiemi E la cui
chiusura è tutto lo spazio X.
Definizione A.7 (Successione Convergente) Sia X uno spazio metrico
e xn una successioni di valori in X. Si dirà che xn converge a x0 se per ogni
¡ 0 esiste un ν tale che per ogni n ¡ ν si ha dpxn , x0 q .
Definizione A.8 (Successione di Cauchy) Sia X uno spazio metrico e
xn una successioni di valori in X. Si dirà che xn è di Cauchy se per ogni
¡ 0 esiste un ν tale che per ogni n, m ¡ ν si ha dpxn , xm q .
APPENDICE A. SPAZI METRICI
80
Utilizzando la disuguaglianza triangolare, si vede facilmente che ogni successione convergente è di Cauchy. Il viceversa in generale non è vero, ma
dipende dallo spazio metrico.
Definizione A.9 (Spazio Completo) Uno spazio metrico X si dice completo se ogni successione di Cauchy in X è convergente.
Teorema A.2 Uno spazio metrico X è completo se e solo se l’intersezione
di una qualsiasi successione C1  C2  . . .  Cn  . . . di insiemi chiusi non
vuoti, con diametro che tende a zero, è costituita da un solo punto.
Definizione A.10 (Funzione Continua) Sia f : X Ñ Y un’applicazione
tra due spazi metrici con distanze rispettivamente dX e dY , f si dice continua
in x P X se
per ogni ¡ 0 esiste δ
¡ 0 : dY pf pxq, f pyqq per ogni y P Y tale che dX px, y q δ .
In particolare, f si dice continua se lo è per ogni x P X
Definizione A.11 (Omeomorfismo) Sia f : X Ñ Y un’applicazione biettiva tra spazi metrici, allora f si dice omeomorfismo se è continua e anche
la sua inversa lo è.
Due spazi metrici X, Y si dicono omeomorfi se esiste un omeomorfismo di
uno sull’altro.
In particolare, l’omeomorfismo definisce una relazione di equivalenza tra spazi
metrici.
Appendice B
Spazi Topologici
Definizione B.1 (Struttura Topologica) Si definisce una struttura topologica o topologia su X, con X ∅, una famiglia non vuota τ di sottoinsiemi di X, detti insiemi aperti della topologia, tali che:
1. ∅, X sono aperti
2. l’unione di una qualsiasi famiglia di insiemi aperti è un aperto
3. l’intersezione di due insiemi aperti è un aperto
La coppia pX, τ q è detta spazio topologico e i suoi elementi punti. L’insieme
X si dice supporto dello spazio topologico pX, τ q.
Dato uno spazio metrico pX, dq si può sempre costruire una topologia
su X considerando la famiglia di aperti rispetto a d, tale topologia si dice
topologia indotta da d.
La famiglia B tX, ∅u è una topologia per ogni X ∅, è detta topologia
banale e pX, B q spazio topologico banale.
Considerando aperto ogni sottoinsieme di X e prendendo τ P pX q si ottine
la topologia discreta e pX, P pX qq è lo spazio topologico discreto.
Definizione B.2 (Spazio Topologico Metrizzabile) Uno spazio topologico pX, τ q è metrizzabile se esiste una distanza su X che induce τ .
Se uno spazio topologico è metrizzabile, la distanza che induce la topologia
non è univocamente determinata.
Osservazione: Non tutti gli spazi topogici sono metrizzabili: per esempio
quelli a supporto finito e non discreto, in quanto ogni spazio metrizzabile finito è discreto.
81
APPENDICE B. SPAZI TOPOLOGICI
82
Definizione B.3 (Topologia Indotta) Sia X uno spazio metrizzabile da
dX , Y „ X con dY restrizione di dX a Y , allora la topologia indotta da dY
su Y è detta topologia indotta da X su Y .
Definizione B.4 (Base di una topologia) Sia τ una topologia su un insieme non vuoto X. Una base di τ è una famiglia di aperti B „ τ tali che
ogni aperto di τ sia un unione di aperti di B, ovvero
per ogni aperto A di X e per ogni punto x P A esiste B
x P B „ A.
P B tale che
Se B è una base per τ , dati due insiemi qualsiasi A, B P B la loro intersezione
è un aperto ed è quindi unione di elementi di B. Anche X essendo aperto è
unione di elementi di B.
Definizione B.5 (Topologia Prodotto) Dati due spazi X1 , X2 con topologia rispettivamente τ1 , τ2 . Si considera il prodotto cartesiano X X1 xX2
e la famiglia di sottoinsiemi
B
tA1xA2 : A1 P τ1, A2 P τ2u
con
A1 , A2
aperti
che è sia un ricoprimento per X ma, si vede facilmente, è anche base di
un’unica topologia τ su X per la prop1osizione.
Allora τ è detta topologia prodotto su X.
pX, τ q si chiama spazio topologico prodotto di X1 per X2.
Si consideri una famiglia qualsiasi tXs usPS di spazi topologici con topologie
rispettivamente τs , s P S, e il prodotto cartesiano
X
¹
P
Xs
tf : S Ñ
s S
¤
P
Xs |f psq P Xs , s P S u
s S
Si definisce la t-esima proiezione l’applicazione
pt : X
Ñ Xt
con pt pf q f ptq
Definizione B.6 (Topologia della Convergenza Puntuale) Considerando
S pa, bq un intervallo aperto di R e Y R. Allora X Rpa,bq è l’insieme
delle funzioni a valori reali definite in pa, bq. La topologia prodotto in R si
chiama topologia della convergenza puntuale, in quanto è una topologia per
cui si ha:
esiste il limite della successione tfn unPN
„ X in τ ðñ
per ogni x P pa, bq la successione tfn pxqunPN ha un limite.
APPENDICE B. SPAZI TOPOLOGICI
83
Definizione B.7 (Filtro) Sia X un insieme, una famiglia F di parti di X
si dice filtro se soddisfa le seguenti prop1rietà:
(i) per ogni U
(ii) se U
(iii)
PF
PF
e U1
… U si ha W P F
allora anche U X U 1 P F
eW
PF
HRF
Definizione B.8 (Uniformità diagonale) Si definisce uniformità diagonale ∆ su X un filtro U di XxX tale che
(i) ∆ tpx, xq|x P X u „ U per ogni U
(ii) se U
PU
PU
P U , dove U 1 tpy, xq|px, yq P U u
P U tale che V 2 tpx, yq| esiste z P X
allora anche U 1
(iii) per ogni U P U esiste V
px, zq, pz, yq P V u „ U
:
Ogni elemento di U è detto entourage.
Definizione B.9 (Spazio Uniforme) Uno spazio definito da una base di
entourages si dice uniforme se è chiuso rispetto all’unione e all’intersezione.
Ogni spazio uniforme si può dotare di una topologia, definendo come aperto
qualunque sottoinsieme A tale che per ogni x P A esiste un entourage U P U
per cui
U rxs ty |px, y q P U u „ A
Definizione B.10 (Uniformità Metrica) Dato uno spazio metrico pX, dq,
si definisce la sua uniformità metrica il filtro generato da
Ur
tpx, yq P XxX |dpx, yq ru
Definizione B.11 (Insieme Denso) Unn sottoinsieme D di uno spazio
topologico X si dice denso nello spazio se ogni elemento dello spazio appartiene all’insieme o ne è punto di accumulazione, in particolare se D X.
Appendice C
Topologia di Scott
Originariamente Scott definı̀ la sua topologia su reticoli completi. Questa
definizione generalizza immediatamente gli ordini parziali completi.
Definizione C.1 Sia pD, „q un poset (insieme parzialmente ordinato) con
„ riflessiva, allora si definisce:
(i) un sottoinsieme X
– X
H
– per ogni x, y
„ D è diretto se
P X esiste z P X tale che x „ z, y „ z
(ii) D è un cpo (ordine parziale completo) se
– esiste un elemento minimo
K < x. K si dice bottom
– per ogni X
K P D, cioè tale che per ogni x P D
„ D diretto esiste il massimo — X P D
Definizione C.2 (Reticolo Completo) Un reticolo completo è un poset
in cui ogni X „ D ha un massimo.
Osservazione: Ogni reticolo completo è un cpo, dal momento che
K —H
Definizione C.3 (Topologia di Scott) Sia pD, „q un cpo, la topologia di
Scott su D è definita come segue:
un insieme O „ D è aperto se
• x P O e x < y implica y
•
—
X
PO
P O, con X „ D diretto implica X X O H
84
APPENDICE C. TOPOLOGIA DI SCOTT
85
La caratterizzazione delle funzioni continue è la principale ragione per cui si
introduce la topologia di Scott.
1 una mappa, con pD, <q, pD1 , <1 q cpo.
Proposizione C.1 Sia f : D Ñ D—
—
Allora f è continua se e solo se f p X q f pX q per ogni X „ D diretto,
dove f pX q tf pxq|x P X u.
Proposizione C.2 Dati pD, <q, pD1 , <1 q cpo. Sia DxD1 il prodotto cartesiano parzialmente ordinato da
xx, x1y < xy, y1y se e solo se x < y, x1 < y1
1
Allora
— DxD
— è un cpo dove, per un sottoinsieme diretto X
x X0, X1y in cui
X0
tx P D| esiste x1 P D1, xx, x1y P X u,
X1
„ DxD1, — X tx1 P D1| esiste x P D, xx, x1y P X u.
In generale, la topologia su DxD1 non è il prodotto delle topologia su D e
D1 .
Definizione C.4 Siano dati pD, <q, pD1 , <1 q cpo. Si definisce
rD Ñ D1s tf : D Ñ D1|f è continuau
Tale insieme può essere ordinato parzialmente puntualmente:
f < g se e solo se per ogni x P D
Si ottiene quindi che rD
particolare:
f pxq <1 g pxq
Ñ D1s è un poset per ogni pD, <q, pD1, <1q cpo.
In
Proposizione C.3 rD Ñ D1 s è un cpo con il massimo un insieme diretto
F „ rD Ñ D1 s definito da
§
p
F qpxq §
tf pxq|f P F u
Proposizione C.4 (Continuità dell’applicazione) Ap : rDxD1 sxD
D con Appf, xq f pxq è continua.
Ñ
Proposizione C.5 (Continuità dell’astrazione) Sia fppxq λy.f px, y q P
D1 con f P rDxD1 Ñ D2 s, allora
(i) fp è continua, cioè fp P rD
(ii)
Ñ rD1 Ñ D2ss
λf.fp : rDxD1 Ñ D2 s Ñ rD Ñ rD1 Ñ D2 ss è continua.
Bibliografia
[1] Appunti del corso di ”Tipi e logica lineare” tenuto dal professor Abrusci
nell’anno accademico 20012/2013.
[2] Arnold A., Nivat M.: The Metric Space of infinite trees. Algebraic and
topological proprerties, Fundation Information 3(4), (445-476), 1980.
[3] Baillot P., Terui K.: A feasible algorithm for typing in Elementary Affine
Logic, Lecture Notes in Computer Science Volume 3461, pp 55-70, 2005
[4] Barendregt H. P.: The Lambda Calculus, North Holland, 1984.
[5] Church, A.: A set of postulates for fondation of logic, Annals of
Mathematics, 1932
[6] Church A.: A Formulation of the Simple Theory of Types, JSL 5, 1940
[7] Curry H.B., Feys R.: Combinatory Logic, volume 1, Olanda, 1958
[8] De Bruijn N.G.: Lambda calculus notation with nameless dummies,
Indagat. Math.34, (95-169), 1972.
[9] Girard J.Y.: Proof and types, Cambridge, Cambridge University Press,
1989
[10] Girard J.Y.: From foundation to ludics, Bulletin of Symbolic Logic, 9(2),
2003
[11] Girard J. Y.: The Blind Spot, Zurigo, European Mathematicall Society,
2011
[12] Giusti E.: Analisi Matematica 1, Bollati Boringhieri, 1985
[13] Giusti E.: Analisi Matematica 2, Bollati Boringhieri, 1985
[14] Harrison J.: Introduction to Functional Programming, 1997
86
BIBLIOGRAFIA
87
[15] Howard W. A.: The formulae-as-types notion of construction in To H. B.
Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism,
J. P. Seldin and J. R. Hindley (ed), pp. 479-490, Academic Press, 1980
[16] Kalmàr L.: Ein einfaches Beispiel für ein unentscheidbares arithmetisches Problem, Mat. Fiz. Lapok, 50:1-23, 1943
[17] Krivine J.L.:Lambda-calcul, types et modles, Masson, Paris, 1990
[18] Mazza D.: An Infinitary Affine Lambda-Calculus Isomorphic to the
Full Lambda-Calculus, Proceedings of the 27th Annual ACM/IEEE
Symposium on Logic In Computer Science, LICS, 2012
[19] Mazza D.:Non-Uniform Polytime Computation in the Infinitary Affine
Lambda-Calculus, Proceedings of ICALP, 2014
[20]
[21] Sernesi E.: Geometria 2, Bollati Boringhieri, 1994
[22] Terui K.: Computational ludics, Theoretical Computer Science, 412(20),
(2048-2071), 2011