HYPERCOHÉRENCES ET JEUX

Sujets

• Agent contractuel
• Protocole de cohérence de cache
• Strictement personnel
• Ensemble fini
• Finien de Clonard
• Règles d'Acquisition ferengies

Informations

• Publié par: Sion
• Nombre de lectures: 100
• Langue: Français
• Poids de l'ouvrage: 1 Mo

Extrait

UNIVERSITÉ DE LA MÉDITERRANÉE - AIX-MARSEILLE II U.F.R. DE SCIENCES Numéro attribué par la bibliothèque : THÈSE pour obtenir le grade de DOCTEUR DE L’UNIVERSITÉ DE LA MÉDITERRANÉE Spécialité : MATHÉMATIQUES DISCRÈTES ET FONDEMENTS DE L’INFORMATIQUE présentée et soutenue publiquement par Pierre BOUDES le 20/12/2002 TITRE : HYPERCOHÉRENCES ET JEUX Directeur de thèse : Thomas EHRHARD Rapporteurs : MM. Pierre-Louis CURIEN Glynn WINSKEL Jury : MM. Patrick BAILLOT Pierre-Louis CURIEN Thomas EHRHARD Jean-Yves GIRARD James LAIRD Glynn WINSKEL2Hypercohérences et Jeux Pierre BOUDES Institut de Mathématiques de Luminy 13 janvier 200421 Introduction 7 2 Préliminaires mathématiques 13 2.0.1 Notations, conventions . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.0.2 Logique linéaire, logique linéaire polarisée . . . . . . . . . . . . . . . 15 2.0.3 Les sémantiques dénotationnelles . . . . . . . . . . . . . . . . . . . . 18 2.0.4 La sémantique relationnelle . . . . . . . . . . . . . . . . . . . . . . . 19 2.0.5 Collapse extensionnel . . . . . . . . . . . . . . . . . . . . . . . . . . 20 I Du statique au dynamique : retrouver le temps 23 3 Déploiement d’hypercohérences 25 3.1 Structure de jeux des hypercohérences . . . . . . . . . . . . . . . . . . . . . . 25 3.1.1 Infinie cohérence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 3.1.2 Le déploiement en tours . . . . . . . . . . . . . . . . . . . . . . . . . 31 3.2 Comportement logique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 3.2.1 Additifs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 3.2.2 Multiplicatifs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 3.2.3 Exponentielles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 4 Jeux polarisés à bord 55 4.1 Jeux polarisés . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 4.2 Un modèle de MALLP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75 4.2.1 Correction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 4.2.2 Réversibilité . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 4.2.3 Écrasement sur le modèle relationnel . . . . . . . . . . . . . . . . . . 82 4.3 Vers un modèle intégrant les exponentielles . . . . . . . . . . . . . . . . . . . 84 4.3.1 Interprétation des exponentielles . . . . . . . . . . . . . . . . . . . . . 85 5 Exponentielle pour les jeux à bords 93 5.1 Construction exponentielle . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94 5.2 Non exponentielle des algorithmes séquentiels . . . . . . . . . . . . . . . . . . 100 5.3 Structure de nouvelle catégorie de Seely . . . . . . . . . . . . . . . . . . . . . 103 34 TABLE DES MATIÈRES II Simple et multiple 115 6 Uniformité et lieux de l’interaction 117 6.1 Espace deP -cohérence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121 6.2 Uniformité destructive, le modèle relationnel bipartite . . . . . . . . . . . . . . 122 6.2.1 Le modèle bipartite uniforme . . . . . . . . . . . . . . . . . . . . . . . 123 6.3 La sémantiqueK-cohérente de la logique linéaire . . . . . . . . . . . . . . . . 125 6.3.1 Interprétation de MALL... rien de nouveau . . . . . . . . . . . . . . . 126 6.3.2 Exponentielles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 127 6.3.3 Le bien sûr est le⊗-comonoïde libre . . . . . . . . . . . . . . . . . . 131 6.4 Sémantiques non-uniformes et sémantiques uniformes . . . . . . . . . . . . . 134 6.4.1 Hypercohérences non-uniformes . . . . . . . . . . . . . . . . . . . . . 138 6.4.2 Collapses extensionnels . . . . . . . . . . . . . . . . . . . . . . . . . 140 6.4.3 Séquentialité d’ordre supérieur . . . . . . . . . . . . . . . . . . . . . . 140 7 Conclusion et Perspectives 143Mes plus vifs remerciements vont à Thomas Ehrhard, pour la qualité exceptionnelle de son encadrement et pour l’attention sans faille qu’il a su porter à cette thèse au cours de son élabo- ration, toujours avec une grande humanité. Je dois beaucoup à Jean-Yves Girard, dont les travaux sont une source d’inspiration toujours renouvelée, ayant largement participé à mon éveil scientifique, dans une équipe de recherche d’un dynamisme très stimulant. Je tiens ici à l’en remercier. Merci à Pierre-Louis Curien pour la qualité de ses suggestions et de son écoute, lors des quelques discussions scientifiques que nous avons pu avoir, en particulier, lors de sa relecture de cette thèse. Je tiens à remercier Glynn Winskel pour avoir mené à bien la relecture de cette thèse, avec un regard extérieur, et malgré la difficulté due à la langue. Merci à Martin Hyland pour l’intérêt qu’il a porté à mon travail sur la non-uniformité, lors de ses passages à Marseille, et pour m’avoir aiguillé vers la conjecture de Longley. Les travaux de James Laird, d’une richesse étonnante, ont suscité mon intérêt et m’ouvrent de nouvelles pistes de recherche en connexion avec cette thèse, ce dont je le remercie. Merci à Patrick Baillot et à Olivier Laurent, pour toutes ces discussions que nous avons eu, notamment lorsque nous partagions le même bureau, et qui m’ont beaucoup apporté d’un point de vue scientifique. Merci à Alexandra Bruasse-Bac avec qui j’ai pu partager de nombreuses fois mon intérêt pour les travaux de Thomas Ehrhard. Merci à Samuel Tronçon dont le regard neuf sur les travaux de Jean-Yves Girard a donné matière à de nombreuses et intéressantes discussions. L’équipe Logique de la Programmation a su m’accueillir dans une véritable dynamique de recherche. Je tiens à remercier particuliérement Marie-Renée Fleury-Donnadieu, Myriam Qua- trini et Laurent Regnier pour la qualité de cet accueil. Merci à Pierre Barthelémy, France Bodin, Jeanine Brohan, Jean-Bruno Erismann et à Aurélia et Éric Lozingot pour leur efficacité à faire fonctionner le laboratoire. Parmi les thésards de l’équipe, je remercie aussi Sylvain Lippi et Virgile Mogbil ainsi que Christophe Gaubert, Pierre Hyvernat et Alaeddine Benrhouma pour avoir participé à un climat chaleureux, propice à la recherche. Mes remerciements vont encore à Cédric Lhoussaine avec qui j’ai découvert le monde de la recherche, en bonne amitié, et pour son soutien. Merci aussi à Lorenzo Tortora de Falco, pour m’avoir permi de séjourner à Rome et avoir su m’y faire partager son intérêt scientifique. Je tiens à remercier ma famille et, en premier lieu, mes parents, Alix et Antoine, ainsi que Cécile Clozel pour leur soutien et pour avoir éveillé en moi le goût du travail intellectuel. Un grand merci à ma compagne, Hélène Tennéroni, pour son soutien indéfectible et pour tout le reste.6 TABLE DES MATIÈRES Cette thèse porte sur les propriétés mathématiques du Calcul. Ce que nous entendons ici par Calcul est, au sens large, l’activité qui consiste à transformer des ingrédients selon des direc- tives simples pour produire un résultat. Plus précisément, nous nous intéressons à la part ma- thématisable de cette activité. Aussi cette thèse ne porte-t-elle pas sur la cuisine, les procédures juridiques ou le jiu-jitsu (« règles procédurales de la souplesse »). Nous distinguons, traditionnellement, deux niveaux de mathématisation dans l’étude des propriétés mathématiques du Calcul. Au premier niveau, il s’agit de représenter le Calcul dans les mathématiques, c’est le niveau de la Syntaxe. Se rattachent à ce niveau : la part mécanique des mathématiques (le calcul arithmétique tel qu’enseigné à l’école, par exemple), les machines abstraites, les automates, la machine de Turing, les circuits booléens (à l’œuvre dans les calcu- lettes, les ordinateurs,...), les langages de programmation. La preuve formelle en logique mathé- matique, en partie née du désir de mécaniser le raisonnement, appartient aussi à ce niveau. Pour le calcul sur des entiers, le contenu opératoire des différentes syntaxes (ce qui est calculable) est équivalent. On peut alors parler du Calcul sur les entiers. Au second niveau, nous devons donner une définition mathématique de certaines propriétés du Calcul. Il s’agit d’interpréter le Calcul par des notions mathématiques qui fassent sens. C’est le niveau de la Sémantique, sur lequel se situe cette thèse. Nous nous intéressons, plus précisément, à la sémantique en ce qu’elle offre un point de vue distant, potentiellement porteur d’intuitions nouvelles sur le Calcul. Les objets qui agissent au sein du Calcul, ses agents, sont les algorithmes. Une donnée pour un calcul peut toujours être considérée comme le résultat fourni par un algorithme qui n’attend pas d’entrée. Dans notre cadre, les agents sont typés. Les types définissent quels agents agissent sur quels autres agents. Un agent de typeA→B s’applique à un agent de typeA pour donner un agent de type B. La notion importante est celle d’exécution. L’exécution du calcul est représentée par une procédure de réécriture sur les agents. La procédure de réécriture met les agents sous forme normale. La forme normale d’un agent de typeB obtenu en appliquant un agent de typeA → B à un agent de typeA, est le résultat de cette l’application. L’application 2de la fonction carré, de typeN → N, à l’entier naturel 2 donne l’entier 2 qui se réécrit sous forme normale en l’entier4. Une preuve formelle est une succession finie d’opérations sur des formules logiques produi- sant une formule conclusion. Si on a une preuve de la formuleA et une preuve de la formuleA impliqueB, alors l’opération de modus ponens nous permet de former une preuve deB. Cette preuve deB utilise un lemme qui est la preuve deA impliqueB. En Déduction Naturelle on a une procédure de réécriture des preuves qui élimine l’usage des lemmes. Il existe une correspondance entre les preuves en Déduction Naturelle et les algorithmes, 78 CHAPITRE 1. INTRODUCTION exprimés en λ-calcul typé, pour laquelle la procédure d’élimination des lemmes coïncide avec la procédure d’exécution des algorithmes (la β-réduction des termes). Cette correspondance est appelée correspondance de Curry-Howard. El