de carvalho-these

Informations

• Publié par: Vufuk
• Nombre de lectures: 33
• Langue: Français

Extrait

UNIVERSITÉ DE LA MÉDITERRANÉE Aix Marseille II
ÉCOLE DOCTORALE DE MATHÉMATIQUES ET INFORMATIQUE E.D. 184
THÈSE
présentée pour obtenir le grade de
D  ’U´   M´ ´
Spécialité : Mathématiques
par
Daniel DE CARVALHO
Titre :
Sémantiques de la logique linéaire
et temps de calcul
soutenue publiquement le 4 septembre 2007
JURY
M. Patrick BAILLOT
M. Pierre Louis CURIEN
M. Thomas EHRHARD
M. Martin HYLAND Rapporteur
M. François LAMARCHE
M. Kazushige TERUI
M. Lorenzo TORTORA DE FALCO RapporteurKateTable des matières
Remerciements 9
Introduction 11
Préliminaires 15
1 Préliminaires catégoriques 17
1.1 Catégories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
1.2 enrichies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2 La logique linéaire 23
2.1 Les formules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
2.1.1 Le fragment intuitionniste . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
2.1.2 La logique linéaire classique . . . . . . . . . . . . . . . . . . . . . . . . . . 23
2.2 Le calcul des séquents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
2.2.1 Le fragment intuitionniste . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
2.2.2 La logique linéaire classique . . . . . . . . . . . . . . . . . . . . . . . . . . 24
2.3 Les réseaux . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
2.3.1 Les structures de preuve de MELL . . . . . . . . . . . . . . . . . . . . . . . 25
2.3.2 Séquentialisation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
I Sémantiques de la logique linéaire et réseaux différentiels 27
3 Qu’est ce qu’un modèle catégorique de la logique linéaire ? 31
3.1 Le deuxième sous sol . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
3.2 Monades faibles (monoïdales) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
3.2.1 Semi monades . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
3.2.2 Monades faibles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
3.2.3 Semi adjonctions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
3.2.4 Algèbres pour une monade faible . . . . . . . . . . . . . . . . . . . . . . . 46
3.2.5 Semi foncteurs monoïdaux et monades faibles monoïdales . . . . . . . . . . 49
3.3 Interpréter la logique linéaire et le lambda calcul . . . . . . . . . . . . . . . . . . . 54
3.3.1 Le fragment multiplicatif exponentiel . . . . . . . . . . . . . . . . . . . . . 54
3.3.2 Une interprétation du lambda calcul simplement typé . . . . . . . . . . . . . 56
3.3.3 Avec les additifs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 81
56 TABLEDESMATIÈRES
3.3.4 Une autre interprétation du lambda calcul . . . . . . . . . . . . . . . . . . . 87
4 Qu’est ce qu’un modèle des réseaux différentiels ? 93
4.1 Bigèbres . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93
4.2 Interpréter les réseaux différentiels . . . . . . . . . . . . . . . . . . . . . . . . . . . 99
5 Des réseaux différentiels à la logique linéaire 101
5.1 Préliminaires (semi )algébriques . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101
5.1.1 Monoïdes et semi anneaux dénombrablement complets . . . . . . . . . . . . 101
5.1.2 Semi modules dénombrablement complets . . . . . . . . . . . . . . . . . . 102
5.2 Construction du modèle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104
5.2.1 Réseaux différentiels avec sommes infinies et coefficients réels positifs . . . 104
5.2.2 Traduire la logique linéaire dans les réseaux différentiels . . . . . . . . . . . 106
6 Deux modèles relationnels 129
6.1 L’interprétation relationnelle de MALL . . . . . . . . . . . . . . . . . . . . . . . . 129
6.2 Le modèle relationnel des multiensembles finis . . . . . . . . . . . . . . . . . . . . 130
6.3 Une sémantique non uniforme du lambda calcul pur . . . . . . . . . . . . . . . . . 131
6.3.1 Interpréter les lambda termes . . . . . . . . . . . . . . . . . . . . . . . . . 131
6.3.2 Une sémantique non uniforme . . . . . . . . . . . . . . . . . . . . . . . . . 133
6.3.3 Des types avec intersection non idempotente . . . . . . . . . . . . . . . . . 133
6.3.4 Propriétés de normalisation . . . . . . . . . . . . . . . . . . . . . . . . . . . 137
6.4 Le modèle relationnel des suites finies . . . . . . . . . . . . . . . . . . . . . . . . . 138
6.5 Une cocontraction non commutative . . . . . . . . . . . . . . . . . . . . . . . . . . 141
6.6 Une sémantique non extensionnelle du lambda calcul typé . . . . . . . . . . . . . . 142
7 Hic salta ! 143
7.1 A propos de l’extensionnalité . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 145
7.2 Une contraction non cocommutative ? . . . . . . . . . . . . . . . . . . . . . . . . . 146
II Temps de calcul via sémantique et types avec intersection 149
8 La machine de Krivine 153
8.1 Une machine calculant la forme normale de tête principale . . . . . . . . . . . . . . 153
8.1.1 Etats de la machine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 153
8.1.2 Exécution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 154
8.1.3 Des dérivations de type pour les états . . . . . . . . . . . . . . . . . . . . . 157
8.1.4 Relier la taille des dérivations et le temps d’exécution . . . . . . . . . . . . . 160
8.1.5 Relier la sémantique et le temps d’exécution . . . . . . . . . . . . . . . . . 164
8.2 Une machine calculant la formeβ normale . . . . . . . . . . . . . . . . . . . . . . . 166
8.2.1 Typages principaux et 1 typages . . . . . . . . . . . . . . . . . . . . . . . . 167
8.2.2 Relier la taille des dérivations et le temps d’exécution . . . . . . . . . . . . . 168
8.2.3 Relier la sémantique et le temps d’exécution . . . . . . . . . . . . . . . . . 170
8.3 Travail ultérieur . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 171TABLEDESMATIÈRES 7
9 Des types avec intersection pour le lambda calcul léger 173
9.1 Le lambda calcul affine léger . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 174
9.2 Le système d’assignation de types ILAL . . . . . . . . . . . . . . . . . . . . . . . 176N
9.3 Les vrais termes, les termes sûrs et les termes raisonnables . . . . . . . . . . . . . . 177
9.4 Le système de types avec intersection légère (LI) . . . . . . . . . . . . 180
9.4.1 “Subject Reduction” . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 181
9.4.2 Pseudo termes typables et termes raisonnables . . . . . . . . . . . . . . . . 181
9.4.3 Les termes raisonnables sont typables . . . . . . . . . . . . . . . . . . . . . 181
9.4.4 Le gommage d’un terme raisonnable est fortement normalisable . . . . . . . 184
9.5 Le système relâché avec intersection légère (RLI) . . . . . . . . . . . . . . . . . . . 186
9.5.1 “Subject Reduction” . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 186
9.5.2 Propriété de la sous formule . . . . . . . . . . . . . . . . . . . . . . . . . . 187
9.5.3 Les pseudo termes typables sont des termes sûrs . . . . . . . . . . . . . . . 187
9.5.4 Les termes sûrs sont des termes typables . . . . . . . . . . . . . . . . . . . . 187
9.6 Une sémantique du second ordre . . . . . . . . . . . . . . . . . . . . . . . . . . . . 188
Pour prendre congé 195
A Quelques calculs 199
Bibliographie 2098 TABLEDESMATIÈRESRemerciements
Tout d’abord, merci à Patrick Baillot pour m’avoir initié à la recherche en acceptant de diriger
mon stage de DEA sur la logique linéaire légère et la théorie des ensembles naïve, puis pour avoir
continué tout au long de ma thèse à me prodiguer des conseils et d’avoir eu la patience de lire des
versions préliminaires de mes travaux. J’ai tiré un grand profit des très nombreuses discussions que
j’ai eues avec lui.
Merci à Thomas Ehrhard pour sa grande générosité dans la transmission de sa compréhension de
la logique, je lui dois beaucoup et lui en suis très reconnaissant. Il a su diriger ma thèse en me laissant
une grande liberté, tout en restant très exigeant.
Merci à Damiano Mazza et à Lionel Vaux pour leur amitié et pour notre collaboration : grâce à
eux, j’ai mieux compris les réseaux de la logique linéaire et les réseaux différentiels.
Merci aux membres de l’équipe de de l’IML pour leur accueil, en particulier à Pierre
Boudes, Marie Renée Donnadieu, Yves Lafont, Myriam Quatrini, Laurent Régnier et Paul Ruet.
Merci aussi à Etienne Duchesne, Marc de Falco, Yves Guiraud et Pierre Hyvernat pour avoir
contribué à créer une ambiance favorable au sein de l’&