these-duchesne
116 pages
Français
Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres

Description

Universite de la Mediterranee, Aix-Marseille 2U.F.R. de MathematiquesTHESEpour obtenir le grade deDOCTEUR DE L’UNIVERSITE AIX-MARSEILLE 2Specialite : Mathematiquespresentee et soutenue publiquement parEtienne Duchesnele 26 octobre 2009Titre :La Localisation en Logique :Geometrie de l’Interaction et SemantiqueDenotationnelleDirecteur de these : Laurent RegnierRapporteurs : Martin HylandPhilip ScottJury : Patrick BaillotJean-Yves GirardMartin HylandSimone MartiniLaurent RegnierKazushige Terui2RemerciementsMerci a Laurent Regnier pour l’attention qu’il m’a portee durant cette these. Je lui suistres reconnaissant pour la patience et la bienveillance dont il a fait preuve, ainsi que pour lagenerosite avec laquelle il partage ses connaissances.Merci a Martin Hyland et a Phil Scott d’avoir accepte de rapporter cette these dans un delaiparticulierement court.Merci a Patrick Baillot, Jean-Yves Girard, Martin Hyland, Simone Martini et KazushigeTerui d’avoir accepte de faire partie du jury. La presence de chacun d’entre eux est un reelhonneur.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 discussionsenrichissantes que j’ai pu avoir avec eux.Merci a tous les membres de l’equipe de logique et plus generalement de l’IML pour leuraccueil chaleureux. Merci aux autres ...

Sujets

Informations

Publié par
Nombre de lectures 34
Langue Français

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
La logique de la programmation s’interesse aux liens existants entre les preuves formelles
et la programmation fonctionnelle. Enoncee en premier lieu pour la logique intuitionniste et le
-calcul avec le celebre isomorphisme de Curry-Howard dans les annees soixante, la correspon-
dance entre preuves et programmes repose sur l’elimination des coupures.
La coupure est une regle logique permettant de deduire l’enonce B a partir d’une preuve de
A et d’une preuve de A)B. Cette regle est en realite redondante et, plus interessant encore
que le fait que l’on puisse s’en passer, il est possible de reecrire les preuves s’en servant jusqu’ a
obtenir des preuves sans coupure { leur forme normale. Le lien entre preuves et programmes
est alors le suivant : une preuve de A) B est un programme qui a une preuve de A associe
une preuve de B, et l’execution de ce programme est donnee par la procedure d’elimination
des coupures. La logique de nit en ce sens un langage de programmation abstrait et on peut
donc considerer ses objets de deux fa cons equivalentes : preuves et enonces logiques d’une part,
programmes et types d’autre part. L’analyse de leur structure particuliere permet alors de
garantir des proprietes sur les programmes s’ecrivant dans ce langage.
C’est dans ce cadre que la semantique des preuves permet d’etudier le sens calculatoire des
demonstrations. Plut^ ot que d’etudier directement les systemes de preuves ou la syntaxe fait
souvent obstacle a une manipulation aisee et alourdit les raisonnements, on interprete les objets
de la logique { enonces et preuves { dans des structures mathematiques adaptees aux proprietes
du calcul etudiees. C’est ainsi que la semantique coherente a permis a J.-Y. Girard d’introduire
la logique lineaire [Gir87a], ou les proprietes liees aux regles structurelles (duplication et ajout
d’hypotheses) observees dans la semantique sont prises en compte dans la syntaxe et aboutissent
a une de nition plus ne des objets. En particulier l’implication intuitionniste A ) B est
decomposee en !A(B formee d’une implication lineaire( { typant un programme utilisant
exactement une fois son argument { et une modalite ! { exprimant la possibilite de dupliquer
un argument. Ce ra nement de la logique intuitionniste fut particulierement fructueux pour
l’analyse de la programmation fonctionnelle. L’implication lineaire etablit une symetrie entre
hypotheses et conclusions et la negation lineaire lui correspondant est involutive. Les preuves
bene cient d’une syntaxe synthetique sous forme de graphes (les reseaux de preuves), eliminant
les informations super ues de sequentialisation et permettant ainsi de decomposer l’elimination
des coupures en etapes elementaires et locales. La dynamique de l’elimination des coupures {
910 CHAPITRE 1. INTRODUCTION
symetrique et locale { est celle d’une interaction entre preuves.
Semantique et localisation
Une part importante des semantiques s’attache a interpreter les preuves par la fonction
qu’elles implementent, la regle de coupure etant alors interpretee par la composition de fonctions.
Bien que la notion de \fonction calculee" varie fortement d’une semantique a l’autre, une preuve
de A ( B calcule la m^eme fonction que cette preuve soit en forme normale ou non. Ces
semantiques { les semantiques denotationnelles { interpretent donc les preuves par un invariant
de la reduction. Cette approche a ete generalisee et abstraite jusqu’ a aboutir a une de