HYPERCOHÉRENCES ET JEUX
154 pages
Français

HYPERCOHÉRENCES ET JEUX

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

Description

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 . . . . . . . . . . . . . . ...

Sujets

Informations

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

Exrait

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. Elle nous permet de voir les preuves formelles comme des algorithmes. La Logique Linéaire, introduite par J.-Y. Girard ([Gir87]), est une syntaxe ayant de nom- breuses bonnes propriétés. Une des caractéristiques importantes de la logique linéaire est qu’elle représente un calcul sensible aux ressources. La notion de ressource remplace ici celle de don- née. AinsiA flèche linéaireB est une formule qui signifie que si on a exactement une ressource de type A, alors on peut produire une ressource de type B, en consommant cette ressource de type A. La ressource A flèche linéaire B est elle aussi consommée. Bien entendu, il est aussi possible de représenter des ressources indéfiniment disponibles. C’est le rôle des modalités ex- ponentielles. Ainsi, bien sûr A, noté!A, signifie qu’une ressource de typeA est disponible autant de fois que nécessaire. La logique linéaire a un grand pouvoir expressif. On peut, par exemple, traduire la Déduction Naturelle en logique linéaire. La formuleA implique B se traduit en !A flèche linéaire B. C’est ce qu’on appelle la décomposition linéaire de la flèche intuitionniste. La notion d’exécution, en logique linéaire, est représentée par l’élimination des coupures (une forme d’élimination des lemmes, due à Gentzen). Dans cette thèse nous ne nous intéressons pas vraiment à la nature des résultats d’un algo- rithme, au temps de calcul qu’il nécessite ou à ce qui est calculable et à ce qui ne l’est pas. Nous nous intéressons plutôt à la nature du Calcul et plus précisément à certaines des ses propriétés intrinsèques. Ces propriétés sont notamment : Le déterminisme. Sur une même entrée, nous avons un même résultat. La séquentialité. Un calcul s’exécute étape par étape. La convergence ou la terminaison. les calculs terminent, autrement dit, on obtient toujours un résultat, et ce, en un nombre fini d’étapes. Nous interprétons les agents du Calcul par des objets invariants par exécution. L’interpré- tation obtenue est ce qu’on appelle une sémantique dénotationnelle. La dénotation d’un agent est l’agent en lequel il se réécrit, sa forme normale. Ainsi la dénotation de 2 + 1 est 3, et en sémantique dénotationnelle 2 + 1 et 3 doivent avoir la même interprétation. La donnée d’une fonction d’interprétation des agents est ce qu’on appelle un modèle dénotationnel. La logique linéaire est très liée à l’activité en sémantique dénotationnelle. Une part de la découverte de la logique linéaire peut d’ailleurs être attribuée à cette activité. En effet, l’inter- prétation de la Déduction Naturelle dans les espaces cohérents a, la première, révélé la décom- position linéaire de la flèche intuitionniste. Dans cette thèse, nous travaillons principalement avec la logique linéaire comme syntaxe du Calcul. Une interprétation dénotationnelle standard associe aux algorithmes les fonctions qu’ils cal- culent. Le modèle obtenu est alors dit extensionnel. Le fait qu’une fonction associe à une entrée un unique résultat correspond au déterminisme. La convergence est le fait que la fonction asso- ciée à un algorithme est totale. La convergence en un nombre fini d’étapes correspond au fait que, pour calculer un résultat fini, la fonction associée à un algorithme n’utilise qu’une part finie des données. Dans le modèle des espaces cohérents, les agents sont interprétés par des fonctions stables. La stabilité assure que, pour chaque atome de résultat calculé par une fonction sur une donnée, il existe une part minimale de la donnée qui permet de calculer cet atome de résultat. La séquentialité est plus mystérieuse au niveau des fonctions. On peut l’exprimer pour des agents simples calculant des résultats atomiques sur des données atomiques. Mais la généralisation na- turelle de cette définition de la séquentialité ne permet pas de définir un modèle dénotationnel dans un cadre extensionnel ([Ehr99]). La stabilité forte a été introduite par A. Bucciarelli et T. Ehrhard ([BE94]). Dans une cer- taine mesure, elle permet d’exprimer la séquentialité dans un cadre extensionnel ([Ehr99]). Les hypercohérences forment un modèle de la logique linéaire, introduit par T. Ehrhard ([Ehr93]), donnant une présentation simplifiée de la stabilité forte sous forme de cliques, représentant les agents, dans des hypergraphes, représentant les formules.
  • Accueil Accueil
  • Univers Univers
  • Ebooks Ebooks
  • Livres audio Livres audio
  • Presse Presse
  • BD BD
  • Documents Documents