ens-mellies-cours-6
59
pages
Catalan
Documents
Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres
59
pages
Catalan
Documents
Le téléchargement nécessite un accès à la bibliothèque YouScribe Tout savoir sur nos offres
Lambda calculs et catégoriesPaul-André MellièsMaster Parisien de Recherche en InformatiqueEcole Normale Supérieure1Plan de la séance1 – Théorie formelle des monades2 – Lambda-calcul avec effets3 – Monades fortes2Première partieThéorie formelle des monadesCatégorie de Kleisli, catégorie d’Eilenberg-Moore3Monade formelleSoit A une 0-cellule dans une 2-catégorieB.Une monade s sur la 0-cellule A est une 1-cellules : A ! Amunie d’une multiplication : ss ) s : A ! Aet d’une unité : Id ) s : A ! AAsatisfaisant les lois d’associativité et d’unité.Autrement dit, une monades est un monoïde de la catégorie monoïdaleB(A;A).4Toute adjonction définit une monade(démonstration graphique)5 // ///>>/AlgèbreUne algèbre de la monade (T; ; ) est une paire (A;h) constituée— d’un objet A morphisme— d’un morphismeh : TA! Afaisant commuterA2TAA TAT A} AA}} A} AA}} A} A} AA} Ah} A} A} A hTh} A} AA}} A} A} A} A}A A TA Aid h6////Morphismes d’algèbreUn morphisme d’algèbref : (A;h )! (B;h )A Best un morphismef : A! Bentre les objets sous-jacents dans la catégorieC, tel que le diagrammeTfTBTAh hA BA Bfcommute.7777777Catégorie de KleisliLa catégorie de KleisliC d’une monade (T; ; ) sur une catégorieC aT— pour objets les objets deC,— pour morphismes A! B les morphismes de A! TB dans la catégorieC,Les identités A! A sont données par les morphismes : A! TA:AOn compose f : A! B et ...
Voir
Lambda calculsetcatégories
Paul-André Melliès
Master Parisien de Recherche en Informatique
Ecole Normale Supérieure
1
1
2
3
–
–
–
Plan
Théorie formelle des monades
Lambda-calcul avec
Monades fortes
effets
de
la
séance
2
Première partie
Théorie formelle des monades
Catégorie de Kleisli, catégorie d’Eilenberg-Moore
3
Monade formelle
SoitAune0-cellule dans une 2-catégorieB.
Une monadessur la0leluel-cAest une 1-cellule
munie d’une multiplication
et d’une unité
s:A−→A
µ:s◦s⇒s:A−→
η:IdA⇒s:A−→ satisfaisant les lois d’associativité et d’unité.
A
A
Autrement dit, une monadesest un monoïde de la catégorie monoïdaleB(A,A).
4
Toute
adjonction
définit
(démonstration
une
graphique)
monade
5
Algèbre Une algèbre de la monade(T, µ, η)est une paire(A,h)ocsntituée — d’un objetAmemorphis — d’un morphisme h:TA−→A faisant commuter
TA }}}}}}}>>AAAAAAAAAh ηAAAAAAA}}}AA}AA }}} }}}} }}A Aid//A
T2A Th TA
µA h
//
TA h //A
6
Morphismes d’algèbre
Un morphisme d’algèbre
est un morphisme
f: (A,hA)−→(B,hB)
f:A−→B entre les objets sous-jacents dans la catégorieC, tel que le diagramme
commute.
TA
h
hA
A
A
T f
f
//
TB
//
hB
B
7
Catégorie de Kleisli La catégorie de KleisliCTd’une monade(T, µ, η)sur une catégorieCa — pour objets les objets deC, — pour morphismesA→Bles morphismes deA−→TBdans la catégorieC, Les identitésA→Asont données par les morphismes ηA:A−→TA. On composef:A→Betg:B→Cde la manière suivante:
TTC oo77 oo ooo ooooTogooooooµC ooo ooooo TB TC g◦Kf:=pp77ooo oo77 o ApppppppppppppfpppppppppppBoooooooooooooogoooooooo
8
Exercice Montrer que les identités sont des identités, et que la composition est associative. Remarque: la démonstration d’associativité de la loi de composition amène à considérer le diagramme
T3D o77 oo oTo2oohooooTµ oooo T2C T2D Tgooooooo77µoo77µ Thooooo ooooooo o ooooooooo TB TC TD pfpppppppp88ooooogooooooooo77nnnnhnnnnnnnnnn77 AppppppBoooCnnnnD dans la catégorieC, et de vérifier que les deux morphismes deAàTD.tnedicnioc
9
Principe de représentation
Toute monade (au sens 2-catégorique)
t:A−→A induit une monade (au sens catégorique)
B(X,t) :B(X,A)−→B(X,A) définie par post-composition
t Xf//A7→Xf//A//A et cela pour toute0leluel-cXde la 2-catégorieB.
Exercice.Vérifier queB(X,t)définit bien une monade surB(X,A).
10
Principe de représentation (dual)
Dualement, toute monade (au sens 2-catégorique)
t:A−→A induit une monade (au sens catégorique)
B(t,X) :B(A,X)−→B(A,X) définie par pré-composition cette fois-ci:
f
Af//X7→At//A cela pour toute0ulelc-leXde la 2-catégorieB.
Exercice.Montrer queB(t,X)=Bop(Xop,top).
f
//
X
11
