mpri-mellies-cours-3

Publié par

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 ...
Publié le : samedi 24 septembre 2011
Lecture(s) : 26
Nombre de pages : 66
Voir plus Voir moins
Master Parisien de Recherche en Informatique Cours 2.2
Modeledeslangagesdeprogrammation Domaines,Cat´egories,Jeux
Dernierese´ance
Exponentielle;
Construction de Kleisli
1
S´ear´ec´edente:lacate´gorieEnscommeccc nce p —Unecat´egoriecarte´ sienneest une categorieCousontsp´eci´es: ´
pour chaque couple d’objetsA, B sien, un produit carte´A×Bet ses projections A×B−→AetA×B−→B,
un objet terminal1.
—Unecat´egorie closecarte´ sienneecat´egoestunes´ci´espntsouoenneise´traceirrp,uo chaque objetB,
un foncteur
(− ⇒ −) :Cop×CC,
une famille de bijections(φA,B,C)A,C par des objetsindexe´ eA, B, C: φA,B,C:Hom(A×B, C)−→Hom(B, AC) naturelle enA,BetC.
2
I.
Espaces
de
coherence. ´
3
Espacedecoh´erence Cemodeleestaloriginedelalogiquelin´eaire(1986). De´compositionlin´eairedumodeledesdI-domainesetfonctionsstables. Depuis,dautrestelleslin´earisationsonte´te´ope´r´ee:
Structures dedonn´eesconcretes Berry-Curien 1985
dI-domainesaveccoh´erence et fonctions fortement stables Bucciarelli-Ehrhard 1991
Bidomaines Berry 1979
Jeux Lamarche 1992
Espace dhypercoh´erence Ehrhard 1993
Bistructures Curien-Plotkin-Winskel 1996
4
Espacedecohe´rence On appelleenceh´erdeecsopaceun coupleA= (|A|_,^A)em´orf — d’un ensemble|A|appele´ latramedeA —dunerelationreexivesym´etrique_^A⊂ |A| × |A|´lepeepaneec´ohcre. Espacedecoh´erencereinametnade´peeirededstunegephra. Notation:on´ecrit —a _Aa0sia_^Aaeta6=a. —^a_Aa0si¬(^a_Aa0)oua=a0. Exemple 1. les espaces de cohe´ rence0 =>de trame vide et1 =de trame singleton. Exemple 2. pour tout ensembleX”dsircteh´erencepacedeco,sel(X,=). En particulier, B= ({V, F},=)etN= (N,=).
00
5
Interaction
Uneueiqcludans un grapheAest un sous-ensemble de|A|tel que (a, a0)ua,^_Aa0 Uneueiqcltinavdans un grapheAest un sous-ensemble de|A|tel que (a, a0)a,_^vAa0
Nousallonsinterpr´eter
— les types simples duλ-calcul comme des graphes,
— les programmesude typeAcomme des cliques deA,
— les contre-programmesvde typeAcomme des anti cliques deA, -
— l’interaction entreuetvcomme l’intersectionuv.
Remarque:uvtnemel=(se´ratlutaenluupn´su´eelcnoit!t.)
6
La ne´ gation
SoitA´O.dnneec´hreitcodecepaesunnation´egsaAcomme le graphe dual deA: e n
—|A|=|A| —a_^Aa0ssi^a_Aa0. Remarque: une anti-clique deAest une clique deA. On fait donc interagir une clique deAcontre une clique deA. Dualite´ Joueur vs. Opposant.
Proprie´te´fondamentale:
A= (A)
7
La somme (plus)
SoientAetB rence. On de´ nitdeux espaces de cohe´la sommeABcomme la somme des graphesAetB
—|AB|=|A|+|B| —a^_ABa0ssia_^Aa0, —^b_ABb0ssi^_bBb0, —_^aABb.ismaja
exo. montrer que les graphesA0etAsont isomorphes.
8
Le produit (avec)
SoientAetBdeux espaces de cohe´ On rence. nit de´le produitA&Bcomme une somme “alternative” des graphesAetB.
—|A&B|=|A|+|B| —a^_A&Ba0ssi_a^Aa0, —b _&Bb0ssi_^bBb0, ^A —a_^A&Bbsr.juuoto
exo. montrer que
A&B= (AB)
9
Tenseur
SoientAetBn´end.Oceenerh´tiedoccaseexpsduele tenseurABcomme le produit des deux graphesAetB:
—|AB|=|A| × |B|
00
—(a, b)_^AB(a0, b0)ssi^_aAaet^_bBb.
exo. montrer que les graphesA1etAsont isomorphes.
10
Par
SoientAetB rence.deux espaces de cohe´ de´ On nitle par-produitA.Bcomme un produit “alternatif” des deux graphesAetB:
.
—|A B|=|A| × |B|
—(a, b)_A.B(a0, b0)ssia _Aa0oub _Bb0.
exo. montrer que
A.B= (AB)
11
Soyez le premier à déposer un commentaire !

17/1000 caractères maximum.