Théorie des catégories en logique et en informatique
Cours de recherche (30h de cours, travail
sur des articles scientifiques)
Cours : Tom Hirschowitz (Tom.Hirschowitz)
Résumé
La théorie des catégories, née dans les années 40 des travaux
d'Eilenberg et Mac Lane en topologie algébrique, a été utilisée
avec succès dans de nombreuses branches des mathématiques, mais
aussi en informatique et en physique.
Plus qu'un exposé exhaustif, qui paraît irréalisable dans un
domaine aussi large, le cours a pour buts principaux:
-
de démystifier la théorie des catégories, qui en tant que
langage scientifique largement utilisé est indispensable à la
compréhension de nombreux domaines de recherche,
- de montrer que des notions centrales à la théorie des
catégories, telles que celle de foncteurs adjoints, parties de la
topologie algébrique, fournissent un point de vue intéressant sur
la logique et l'informatique,
- de donner envie aux étudiants d'utiliser à leur tour, dans
leurs travaux futurs, le langage unificateur des catégories.
Plus techniquement, le cours introduira les notions de base de la
théorie des catégories et passera en revue des exemples
caractéristiques (voir le plan indicatif). Au passage
-
on montrera comment interpréter en termes catégoriques les
langages de programmation, typés ou non et y compris ceux avec
effets de bord,
- on caractérisera les structures catégoriques où on sait faire
de la logique, ainsi que la puissance d'expression de cette
logique,
- on survolera des applications rigolotes auxquelles je ne
saurai pas m'attaquer de trop près, telles que la formulation
catégorique des diagrammes de Feynman et de la mécanique
quantique.
Plan indicatif
-
λ-calcul et catégories cartésiennes fermées,
- catégories monoïdales, cohérence et linéarité,
- catégories dagger-compactes avec début d'application à la
mécanique quantique,
- effets de bords et catégories pré-monoïdales,
- théories algébriques et sémantique algébrique de Lawvere,
- logique du premier ordre et logique catégorique,
- théorie des ensembles et topos,
- sémantique des jeux et doubles catégories,
- syntaxe abstraite avec lieurs et monades exponentielles.
Bibliographie
-
N. Benton et M. Hyland. Traced Premonoidal Categories.
Theoretical Informatics and Applications 37(4):273-299, EDP
Sciences 2003. http://research.microsoft.com/ nick/premonitapdf.pdf
- Carsten Führmann. Varieties of effects. In Proceedings
of the 5th International Conference on Foundations of Software
Science and Computation Structures (FOSSACS 2002), volume 2303
of LNCS, pages 144-158, Grenoble, 2002. Springer-Verlag.
http://www.cs.bath.ac.uk/ cf/eff_hyper.pdf
- Saunders Mac Lane. Categories for the Working Mathematician
(2nd ed.). Graduate Texts in Mathematics 5. Springer, 1998. ISBN
0-387-98403-8.
- Saunders Mac Lane et Ieke Moerdijk. Sheaves in Geometry
and Logic: A First Introduction to Topos
Theory. Springer-Verlag, 1992.
- Benjamin C. Pierce. Basic Category Theory for Computer
Scientists. MIT Press, 1991.
- Andrew M. Pitts. Categorical Logic. Chapter 2 of S. Abramsky
and D. M. Gabbay and T. S. E. Maibaum (Eds) Handbook of Logic in
Computer Science, Volume 5. Algebraic and Logical Structures,
Oxford University Press, 2000. (A preliminary version appeared as
Cambridge University Computer Laboratory Tech. Rept. No. 367, May
1995
http://www.cl.cam.ac.uk/ amp12/papers/catl/catl.ps.gz.)