Universite de la Mediterranee Aix Marseille U F R de Mathematiques
116 pages
Français

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Universite de la Mediterranee Aix Marseille U F R de Mathematiques

-

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris
Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus
116 pages
Français
Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus

Description

Niveau: Supérieur, Doctorat, Bac+8

  • cours - matière potentielle : visites regulieres


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 Terui

  • logique lineaire

  • merci

  • digression categorique

  • universite aix-marseille

  • localisation en logique

  • membres de l'equipe de logique

  • discussions de gdi


Sujets

Informations

Publié par
Publié le 01 octobre 2009
Nombre de lectures 84
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

  • Univers Univers
  • Ebooks Ebooks
  • Livres audio Livres audio
  • Presse Presse
  • Podcasts Podcasts
  • BD BD
  • Documents Documents