mpri-mellies-cours-3

Master Parisien de Recherche en InformatiqueCours 2.2`Modele des langages de programmationDomaines, Categories,´ Jeux` ´Derniere seanceExponentielle;Construction de Kleisli1Seance´ prec´ edente:´ la categorie´ Ens comme ccc— Une categor´ ie cartesienne´ est une categor´ ieC ou` sont specifi´ es:´• pour chaque couple d’objets A,B, un produit cartesien´ A× B et ses projectionsA×B−→A etA×B−→B,• un objet terminal1.— Une categor´ ie cartesienne´ close est une categor´ ie cartesienne´ ou` sont specifi´ es´ , pourchaque objetB,• un foncteurop(−⇒−):C ×C−→C,• une famille de bijections(φ ) indexee´ par des objetsA,B,C:A,B,C A,Cφ :Hom(A×B,C)−→Hom(B,A⇒C)A,B,Cnaturelle enA,B etC.2I. Espaces de coherence´ .3Espace de coherence´` ` ´Ce modele est a l’origine de la logique lineaire (1986).´ ´ `Decomposition lineaire du modele des dI domaines et fonctions stables.Depuis, d’autres telles linear´ isations ont et´ e´ oper´ ee:´StructuresJeuxde donnees´ concretes` ⇒Lamarche 1992Berry Curien 1985dI domaines avec coherence´ Espaceet fonctions fortement stables ⇒ d’hypercoherence´Bucciarelli Ehrhard 1991 Ehrhard 1993Bidomaines Bistructures⇒Berry 1979 Curien Plotkin Winskel 199646Espace de coherence´_´ ´On appelle espace de coherence un coupleA=(|A|, ) forme^A´— d’un ensemble|A| appele la trame deA_´ ´ ´— d’une relation reflexive symetrique ⊂|A|×|A| appelee coherence.^AEspace de coherence´ est une maniere` pedante´ de dire graphe.Notation: on ecr´ it0 ...