La lecture en ligne est gratuite
Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres

Partagez cette publication

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