mpri-mellies-cours-3

Description

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

Informations

• Publié par: Enyo
• Nombre de lectures: 14
• Langue: Français

Extrait

Master Parisien de Recherche en Informatique Cours 2.2

Mode  ledeslangagesdeprogrammation Domaines,Cat ´ egories,Jeux

Dernie  rese ´ ance

Exponentielle;

Construction de Kleisli

1

S ´ ear ´ ec ´ edente:lacate ´ gorieEnscommeccc nce p —Unecat ´ egorie carte´ sienne est 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 close carte´ sienne ecat ´ egoestunes ´ ci ´ espntsouoenneise ´ traceirrp,uo chaque objetB,

•un foncteur

(− ⇒ −) :C op ×C−→C,

•une famille de bijections(φ A,B,C ) A,C  par des objets indexe´ e A, B, C: φ A,B,C :Hom(A×B, C)−→Hom(B, A⇒C) naturelle enA,BetC.

2

I.

Espaces

de

coherence. ´

3

Espacedecoh ´ erence Cemode  leesta  l’originedelalogiquelin ´ eaire(1986). De ´ compositionlin ´ eairedumode  ledesdI-domainesetfonctionsstables. Depuis,d’autrestelleslin ´ earisationsonte ´ te ´ ope ´ r ´ ee:

Structures dedonn ´ eesconcre  tes Berry-Curien 1985

dI-domainesaveccoh ´ erence et fonctions fortement stables Bucciarelli-Ehrhard 1991

Bidomaines Berry 1979

⇒

⇒

⇒

Jeux Lamarche 1992

Espace d’hypercoh ´ erence Ehrhard 1993

Bistructures Curien-Plotkin-Winskel 1996

4

Espacedecohe ´ rence On appelleenceh ´ erdeecsopaceun coupleA= (|A| _ , ^ A )em ´ orf — d’un ensemble|A| appele´ la tramedeA —d’unerelationreexivesym ´ etrique _ ^ A ⊂ |A| × |A| ´ lepeepaneec ´ ohcre. Espacedecoh ´ erencere  inametnade ´ peeirededstunegephra. Notation:on ´ ecrit —a _ A a 0 sia _ ^ A aeta6=a. — ^ a _ A a 0 si¬( ^ a _ A a 0 )oua=a 0 . Exemple 1. les  espaces de cohe´  rence0 =>de trame vide et1 =⊥de trame singleton. Exemple 2. pour tout ensembleX”d“sircteh ´ erencepacedeco,se’l(X,=). En particulier, B= ({V, F},=)etN= (N,=).

00

5

Interaction

Uneueiqcludans un grapheAest un sous-ensemble de|A|tel que ∀(a, a 0 )∈ua, ^ _ A a 0 Uneueiqcltinavdans un grapheAest un sous-ensemble de|A|tel que ∀(a, a 0 )∈a, _ ^ v A a 0

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’intersectionu∩v.

Remarque:u∩vtnemel=(se ´ ratlutaenluupn ´ su ´ eelcnoit!t.)

6

La ne´  gation

SoitA ´ O.dnneec ´ hreitcodecepaesunnation ´ egsaA ⊥ comme le graphe dual deA: e n

—|A ⊥ |=|A| —a _ ^ A ⊥ a 0 ssi ^ a _ A a 0 . 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´  nit deux espaces de cohe´ la sommeA⊕Bcomme la somme des graphesAetB

—|A⊕B|=|A|+|B| —a ^ _ A⊕B a 0 ssia _ ^ A a 0 , — ^ b _ A⊕B b 0 ssi ^ _ b B b 0 , — _ ^ a A⊕B b.ismaja

exo. montrer que les graphesA⊕0etAsont isomorphes.

8

Le produit (avec)

SoientAetB deux espaces de cohe´  On rence. nit  de´ le produitA&Bcomme une somme “alternative” des graphesAetB.

—|A&B|=|A|+|B| —a ^ _ A&B a 0 ssi _ a ^ A a 0 , — b _ &B b 0 ssi _ ^ b B b 0 , ^ A —a _ ^ A&B bsr.juuoto

exo. montrer que

A&B= (A ⊥ ⊕B ⊥ ) ⊥

9

Tenseur

SoientAetBn ´ end.Oceenerh ´ tiedoccaseexpsduele tenseurA⊗Bcomme le produit des deux graphesAetB:

—|A⊗B|=|A| × |B|

00

—(a, b) _ ^ A⊗B (a 0 , b 0 )ssi ^ _ a A aet ^ _ b B b.

exo. montrer que les graphesA⊗1etAsont 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 (a 0 , b 0 )ssia _ A a 0 oub _ B b 0 .

exo. montrer que

A . B= (A ⊥ ⊗B ⊥ ) ⊥

11