these-duchesne

Informations

• Publié par: Nasheg
• Nombre de lectures: 49
• Langue: Français

Extrait

Universite de la Mediterranee, Aix-Marseille 2
U.F.R. de Mathematiques
THESE
pour obtenir le grade de
DOCTEUR DE L’UNIVERSITE AIX-MARSEILLE 2
Specialite : Mathematiques
presentee et soutenue publiquement par
Etienne Duchesne
le 26 octobre 2009
Titre :
La Localisation en Logique :
Geometrie de l’Interaction et Semantique
Denotationnelle
Directeur de these : Laurent Regnier
Rapporteurs : Martin Hyland
Philip Scott
Jury : Patrick Baillot
Jean-Yves Girard
Martin Hyland
Simone Martini
Laurent Regnier
Kazushige Terui2Remerciements
Merci a Laurent Regnier pour l’attention qu’il m’a portee durant cette these. Je lui suis
tres reconnaissant pour la patience et la bienveillance dont il a fait preuve, ainsi que pour la
generosite avec laquelle il partage ses connaissances.
Merci a Martin Hyland et a Phil Scott d’avoir accepte de rapporter cette these dans un delai
particulierement court.
Merci a Patrick Baillot, Jean-Yves Girard, Martin Hyland, Simone Martini et Kazushige
Terui d’avoir accepte de faire partie du jury. La presence de chacun d’entre eux est un reel
honneur.
Au cours de visites regulieres a Paris ou a Lyon, Thomas Ehrhard et Olivier Laurent ont tou-
jours repondu a mes sollicitations. Je les remercie pour leur disponibilite et pour les discussions
enrichissantes que j’ai pu avoir avec eux.
Merci a tous les membres de l’equipe de logique et plus generalement de l’IML pour leur
accueil chaleureux. Merci aux autres thesards et postdocs, presents ou passes, pour avoir fait
de ce laboratoire un lieu d’echange de points de vues, scienti ques ou non. En particulier merci
a Marc de Falco et Thomas Seiller pour nos discussions de GdI, ce dernier a notamment relu
certaines parties de ce memoire ; a Pierre Hyvernat et Lionel Vaux pour avoir si souvent repondu
a mes questions ; a Anne Crumiere et Mathieu Sablik pour leur amitie ; et dans le desordre merci
egalement a Elise, Je , Vincent, Thierry, Nicolas, Yann, Marie-Claire, Tammam, Yves, Daniel,
Manu, Pierre, Paolo et a tous ceux que j’oublie encore.
Merci a Myriam Quatrini pour m’avoir suggere d’ecrire a Kaz.
Merci a Roberta, Anne, Papelucho, Melissa, Florent, Valentina, Boris, Mila, Ely, Charlotte
et aux autres marseillais pour avoir rendu mon sejour inoubliable. Merci a Satti, Celine, David,
Kathrin, Caroline, Claudia, Camille et a tous ceux d’ailleurs pour leur amitie.
Merci a toute ma famille pour leur soutien et pour le bonheur partage a chaque fois qu’elle
s’est elargie.
Merci a Helene pour sa patience, pour m’avoir soutenu pendant les moments les plus penibles
de cette these et pour tout le reste.
34Table des matieres
1 Introduction 9
2 Preliminaires 13
2.1 La logique lineaire classique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.1.1 Formules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
2.1.2 Calcul des sequents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
2.1.3 Structures et reseaux de preuve . . . . . . . . . . . . . . . . . . . . . . . . 15
2.2 La semantique relationnelle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.2.1 Interpretations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
2.2.2 Experiences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
3 Semantique relationnelle localisee 19
3.1 De nitions et notations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
3.2 Le modele . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
3.2.1 Interpretation de LL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
3.2.1.1 Formules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
3.2.1.2 Preuves . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
3.2.2 Oubli de l’indexation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
3.2.3 Digression categorique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
3.2.3.1 Modele categorique de LL . . . . . . . . . . . . . . . . . . . . . . 26
3.2.3.2 Modele faible . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
3.3 Experiences pour RelLoc . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
3.4 RelLoc et LL(I) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
3.4.1 Familles de points et formules de LL(I) . . . . . . . . . . . . . . . . . . . 33
3.4.1.1 Notations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
3.4.1.2 Formules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
3.4.1.3 Projection d’une formule et representation d’une famille . . . . . 34
3.4.1.4 Restriction et re-indexation . . . . . . . . . . . . . . . . . . . . . 35
56 TABLE DES MATIERES
3.4.2 Experiences et calcul des sequents . . . . . . . . . . . . . . . . . . . . . . 37
3.4.2.1 Reformulation des experiences . . . . . . . . . . . . . . . . . . . 37
3.4.2.2 Sequentialisation . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
4 Geometrie de l’interaction de MALL 41
4.1 Preliminaires . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
4.1.1 Motivations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
4.1.2 Ensembles et permutations partielles . . . . . . . . . . . . . . . . . . . . . 42
4.1.3 Interaction et execution . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
4.2 Un cas simple : MLL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
4.2.1 MPI . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
4.2.2 Interpreter les preuves . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
4.2.2.1 Objet dualisant et objet re exif . . . . . . . . . . . . . . . . . . 48
4.2.2.2 Interpretation des formules . . . . . . . . . . . . . . . . . . . . . 49
4.2.2.3 Interpretation des preuves . . . . . . . . . . . . . . . . . . . . . 50
4.3 Les additifs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52
4.3.1 Bool . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
4.3.2 Combinaisons booleennes . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
4.3.2.1 De nitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
4.3.2.2 Operations usuelles . . . . . . . . . . . . . . . . . . . . . . . . . 56
4.3.2.3 Quotient . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
4.3.3 MAPI . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
4.3.4 Interpreter les preuves . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59
4.3.4.1 Objet dualisant et objet re exif . . . . . . . . . . . . . . . . . . 59
4.3.4.2 Interpretation des formules . . . . . . . . . . . . . . . . . . . . . 60
4.3.4.3 Interpretation des preuves . . . . . . . . . . . . . . . . . . . . . 62
5 Les exponentielles 65
5.1 Motivations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
5.1.1 Le principe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
re5.1.2 1 objection : le quotient . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
e5.1.3 2 objection : l’application . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
5.1.4 Une solution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
5.2 Le plongement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
5.2.1 Sur les objets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68
5.2.2 Dereliction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69
5.2.3 Enfouissement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70TABLE DES MATIERES 7
5.3 La promotion fonctorielle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71
5.4 Proprietes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
5.4.1 Naturalite et comonade . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
5.4.1.1 Naturalite . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
5.4.1.2 Comonade faible . . . . . . . . . . . . . . . . . . . . . . . . . . . 77
5.4.2 Contraction et a aiblissement . . . . . . . . . . . . . . . . . . . . . . . . . 80
5.4.3 Mono dalite . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84
5.4.4 & et exponentielles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87
5.5 Interpreter les preuves . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88
5.5.1 Objet re exif . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89
5.5.2 Interpretation des formules . . . . . . . . . . . . . . . . . . . . . . . . . . 91
5.5.3 Interpretation des preuves . . . . . . . . . . . . . . . . . . . . . . . . . . . 91
6 Action de la GdI sur la semantique denotationnelle 93
6.1 Adresses et point xe . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94
6.2 Formes normales . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95
6.3 Dynamique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99
6.4 GdI de MALL et elimination des coupures . . . . . . . . . . . . . . . . . . . . . . 108
7 Perspectives 1098 TABLE DES MATIERESChapitre 1
Introduction
Logique et calcul