Des applications solides de la théorie des catégories dans TCS?

J'ai appris quelques notions de la théorie des catégories. C'est certainement une façon différente de voir les choses. (Résumé très approximatif pour ceux qui ne l’ont pas vue: la théorie des catégories permet d’exprimer toutes sortes de comportements mathématiques uniquement en termes de relations fonctionnelles entre objets. Par exemple, le produit cartésien de deux ensembles est défini complètement en termes de comment se comportent d’autres fonctions avec elle, et non en termes de quels éléments sont membres de l’ensemble.)

Je ne comprends pas très bien que la théorie des catégories soit utile du côté des langages de programmation / logique (la "Théorie B") et je me demande combien d’algorithmes et de complexité ("Théorie A") pourraient en tirer parti. Cela pourrait m'aider à décoller cependant si je connais quelques applications solides de la théorie des catégories dans la théorie B. (je suppose déjà implicitement qu’aucune application dans la théorie A n’a été trouvée à ce jour, mais si vous en avez quelques-unes, c mieux pour moi!)

Par "application solide", j'entends:

(1) L’application dépend tellement de la théorie des catégories qu’il est très difficile à réaliser sans utiliser les machines.

(2) L'application invoque au moins un théorème non trivial de la théorie des catégories (par exemple, le lemme de Yoneda).

Il se pourrait bien que (1) implique (2), mais je veux m'assurer que ce sont des applications "réelles".

Bien que j'aie un peu de "Théorie B", cela fait un moment, donc tout jargonage serait très apprécié.

(En fonction du type de réponses que je reçois, je pourrais transformer cette question en wiki de communauté plus tard. Mais je veux vraiment de bonnes applications avec de bonnes explications, il semble donc dommage de ne pas récompenser le (s) répondant (s) avec quelque chose.)

Je peux penser à un cas où la théorie des catégories a été directement "appliquée" pour résoudre un problème ouvert dans les langages de programmation: Thorsten Altenkirch, Peter Dybjer, Martin Hofmann et Phil Scott, "Normalisation par évaluation pour le lambda calcul typé avec des coproduits" . De leur résumé: "Nous résolvons le problème de décision pour le calcul lambda simplement typé avec de fortes sommes binaires, de manière équivalente le problème de mot pour les catégories fermées cartésiennes libres avec des coproduits binaires. Notre méthode est basée sur la technique sémantique dite" normalisation par évaluation "et implique inverser l'interprétation de la syntaxe dans un modèle de gerbe approprié et en extraire des formes normales uniques et appropriées. "

En général, cependant, je pense que la théorie des catégories n’est généralement pas appliquée pour prouver des théorèmes profonds dans les langages de programmation (ils sont peu nombreux), mais offre plutôt un cadre conceptuel souvent utile (par exemple, le sémantique de la gerbe).

Eugenio Moggi suggère par exemple que la notion de monade (fondamentale et omniprésente dans la théorie des catégories) pourrait être utilisée dans le cadre d'une explication sémantique des effets secondaires dans les langages de programmation (par exemple, état, non déterminisme). Cela a également inspiré des réflexions sur la syntaxe des langages de programmation, par exemple, menant directement à la "classe de types Monad" en Haskell (utilisée pour encapsuler des effets).

Plus récemment (la dernière décennie), cette explication des effets en termes de monades a été revisitée du point de vue du lien ancien (établi par les théoriciens des catégories, dans les années 60) entre les monades et les théories algébriques: voir Martin Hyland et John Power , "La compréhension théorique de la théorie des catégories de l'algèbre universelle: théories de Lawvere et monades" . L'idée est que la vue monadique des effets est compatible avec la vue algébrique (à certains égards plus attrayante) des effets, dans laquelle les effets (par exemple, la mémoire) peuvent être expliqués en termes d'opérations (par exemple, "recherche" et "mise à jour"). et les équations associées (par exemple, idempotence de la mise à jour). Paul-André Melliès a récemment publié un article sur ce lien: "La condition de Segal rencontre les effets de calcul", qui repose également largement sur des idées issues de la "théorie des catégories supérieures" (par exemple, la notion de "structure de Yoneda" en tant que moyen d’organiser la sémantique des présées).

Une autre classe d’exemples apparentés provient de la logique linéaire . Peu de temps après son introduction par Jean-Yves Girard dans les années 80 (dans le but de mieux comprendre la logique constructive), des liens solides ont été établis avec la théorie des catégories. Pour une explication de cette connexion, voir John Baez et Mike Stay, "Physics, Topology, Logic and Computation: A Rosetta Stone" .

Enfin, cette réponse serait incomplète sans référence au blog éclairant de sigfpe "Un voisinage d'infini" . En particulier, vous pouvez consulter "Un classement partiel de la théorie des catégories appliquée à Haskell" .

Calcul quantique

L’application de diverses catégories monoïdales au calcul quantique est un domaine très intéressant. Certains pourraient dire que c'est aussi de la physique, mais le travail est fait par des gens des départements d'informatique. Une première publication dans ce domaine est Une sémantique catégorique des protocoles quantiques de Samson Abramsky et Bob Coecke; de nombreux articles récents d’ Abramsky , de Coecke et d’autres continuent de travailler dans cette direction.

Dans ce corpus, les protocoles quantiques sont axiomatisés en tant que (certains types de) catégories fermées compactes. Ces catégories ont un beau langage graphique en termes de diagrammes de chaînes (et de rubans). Les équations de la catégorie correspondent à certains mouvements des cordes, tels que le redressement d'une chaîne enchevêtrée mais non nouée, qui correspondent à quelque chose de significatif en mécanique quantique, telle qu'une téléportation quantique.

L'approche catégorique offre une vue logique de haut niveau sur ce qui implique généralement des calculs de très bas niveau.

Théorie des systèmes

Coalgebra a été utilisé comme cadre général pour modéliser des systèmes (flux, automates, systèmes de transition, systèmes probabilistes). Sa théorie est enracinée dans la théorie des catégories, basée sur la notion de coalgèbre , où est un foncteur qui décrit la structure du système de transition. Ainsi, le type de système change avec le foncteur sous-jacent, mais une grande partie de la théorie, telle que la notion de bisimulation, est applicable à tous les foncteurs. La théorie des catégories permet également la construction modulaire de logiques modales permettant de raisonner sur des systèmes qualifiés de coalgebras.$F$$F$

Transformations de graphique

Les transformations de graphes peuvent être très bien exprimées dans le langage de la théorie des catégories. Cela a trouvé une application, par exemple, dans la transformation de modèle (comme dans les modèles UML) et dans d'autres formalismes de modélisation visuelle. L'approche se situe dans la catégorie des graphes et des homomorphismes de graphes. Tout d'abord, une découpe peut être vue comme une construction par collage: deux graphiques . Un graphe et deux morphismes et désignent les parties communes des deux graphes. Le pushout unifie ces parties, en ajoutant dans les parties restantes de et , en effet, le collage et ensemble le long de$G_1,G_2$$P$$e_1:P\to G_1$$e_2:P\to G_2$$G_1$$G_2$$G_1$$G_2$$P$ .

Un double affichage est utilisé pour décrire une transformation de graphique. La règle est représentée par un tuple , où indique la condition préalable de la règle, indique la post-condition de la règle et désigne la partie du graphique à laquelle appliquer la règle. Il existe des cartes de et de , dont l'une sera utilisée pour faire correspondre une partie du graphique d'origine, l'autre pour créer le graphique obtenu. décrit la partie du graphe à supprimer. décrit la pièce à créer. Une carte de dans un contexteL R K l $(L, K, R)$$L$$R$$K$$l:K\to L$$r:K\to R$$L\setminus K$$R\setminus K$$d$$K$graphique doit être fournie, et la pushout de et de la carte doit être égal au graphe d'intérêt . Les poussées de et donnent alors le résultat de la transformation.$D$$d$$l$$G$$d$$k$

Langages de programmation (via MathOverflow)

Il y a eu de nombreuses applications de la théorie des catégories dans la conception des langages de programmation et la théorie des langages de programmation. Des réponses détaillées peuvent être trouvées sur MathOverflow. https://mathoverflow.net/questions/3721/programming-languages-based-on-category-theory ) https://mathoverflow.net/questions/4235/relating-category-theory-to-programming-language-theory .

Bigraphs - Calculs de processus

Enfin, il y a les bigraphes de Milner , un cadre général permettant de décrire et de raisonner les systèmes d'agents en interaction. Cela peut être considéré comme un cadre général pour raisonner sur les algèbres de processus et leurs théories structurelles et comportementales. L'approche est également basée sur des pushouts.

Je suppose déjà implicitement qu’aucune application de la théorie A n’a été trouvée à ce jour, mais si vous en possédez, c’est encore mieux pour moi!

• D'après ce que je comprends, la théorie des espèces de Joyal est utilisée assez largement dans la combinatoire énumérative, en tant que généralisation des fonctions génératrices qui vous indiquent également comment permuter les choses en plus du nombre.

• Pippenger a appliqué la dualité de pierre pour relier les langages réguliers et les variétés de semigroupes. Jeandel a introduit les automates topologiques qui appliquent ces idées pour donner des comptes unifiés (et des preuves!) Pour les automates quantiques, probabilistes et ordinaires.

• Roland Backhouse a donné des caractérisations abstraites d'algorithmes gloutons au moyen de connexions de Galois avec le semiring tropical.

Dans une veine beaucoup plus spéculative, Noam a mentionné les modèles de gerbe. Celles-ci caractérisent de manière abstraite la technique syntaxique des relations logiques, qui est probablement l'une des techniques les plus puissantes en sémantique. Nous les utilisons principalement pour prouver des résultats d'inexpressibilité et de cohérence, mais cela devrait être intéressant pour les théoriciens de la complexité, car il s'agit d'un bel exemple de technique de preuve pratique non naturelle (au sens de Razborov / Rudich). (Cependant, les relations logiques sont généralement soigneusement conçues pour garantir leur relativisation - en tant que concepteurs de langage, nous voulons pouvoir assurer aux programmeurs que les appels de fonction sont des boîtes noires!)

EDIT: Je vais continuer à spéculer, à la demande de Ryan. Si je comprends bien, une preuve naturelle est en gros une tentative de définir un invariant inductif de la structure d’un circuit, soumis à diverses conditions sensibles. Des idées similaires sont (sans surprise) assez courantes dans les langages de programmation également, lorsque vous essayez de définir un invariant maintenu inductivement par un terme de lambda-calcul (par exemple, pour prouver la sécurité du type). 1

Cependant, cette technique se brise souvent au niveau des types plus élevés (c'est-à-dire des fonctions). Par exemple, le calcul lambda simplement typé est total - chaque programme écrit dans celui-ci se termine. Cependant, de simples tentatives pour le prouver tendent à se fonder sur le problème des fonctions de premier ordre: il ne suffit pas de prouver que chaque terme de type termine. Comme nous pouvons en outre appliquer des arguments à des fonctions, nous devons non seulement veiller à ce que chaque terme de type interrompu, nous devons également nous assurer que cette propriété a une propriété "héréditaire" - nous devons également savoir que type , l’application s’arrête également.A → B $A \to B$$A \to B$$A$

C'est ce que font les relations logiques. Au lieu de définir un seul invariant inductif, nous définissons toute une famille de prédicats par récurrence sur la structure (généralement) du type. Ensuite, nous prouvons que chaque terme définissable réside dans le prédicat approprié, ce qui nous permet d’établir ce que nous recherchions. Donc, pour la terminaison, nous dirions que les bonnes valeurs du type de base sont les valeurs du type de base, et les bonnes valeurs du type sont les valeurs de ce type qui, avec une bonne valeur de , est évalué à une bonne valeur deA $A \to B$$A$$B$. Notez qu'il n'y a pas d'invariant inductif unique - nous définissons toute une famille d'invariants par récursion sur la structure de l'entrée et utilisons d'autres moyens pour montrer que tous les termes sont compris dans ces invariants. En théorie, c'est une technique beaucoup plus puissante, et c'est pourquoi elle vous permet de prouver la cohérence des résultats.

Le lien avec les gerbes provient du fait que nous avons souvent besoin de raisonner sur les termes ouverts (c'est-à-dire, les termes avec des variables libres), et nous devons donc faire la distinction entre rester bloqué pour des erreurs et rester bloqué en raison de la nécessité de réduire une variable. Les réas proviennent de la considération des réductions du lambda calcul comme définissant les morphismes d'une catégorie dont les termes sont les objets (ie, l'ordre partiel induit par la réduction), puis de considérer les foncteurs de cette catégorie en ensembles (c'est-à-dire, les prédicats). Jean Gallier a écrit quelques articles intéressants à ce sujet au début des années 2000, mais je doute qu'ils soient lisibles à moins que vous n'ayez déjà assimilé une bonne quantité de calcul lambda.

Il existe de nombreux exemples, le premier qui me vienne à l’esprit est l’utilisation par Alex Simpson de la théorie des catégories pour prouver les propriétés des langages de programmation, voir par exemple " Adéquation calculatoire pour les types récursifs dans les modèles de théorie des ensembles intuitionnistes ", Annals of Pure and Applied Logic , 130: 207-275, 2004. Bien que le titre mentionne la théorie des ensembles, la technique est une théorie de la catégorie. Voir la page d'accueil d'Alex pour plus d'exemples.

Je pense que vous posez deux questions sur l'applicabilité, de type A et de type B séparément.

Comme vous le constatez, il existe de nombreuses applications de fond de la théorie des catégories aux sujets de type B: sémantique des langages de programmation (monades, catégories fermées cartésiennes), logique et prouvabilité (topoi, variétés de logique linéaire).

Cependant, il semble y avoir peu d'applications de fond à la théorie A (algorithmes ou complexité).

Il existe certaines utilisations dans les objets élémentaires, telles que la description de catégories d'automates ou d'objets combinatoires (graphes, séquences, permutations, etc.). Mais cela ne semble pas expliquer une compréhension plus profonde de la théorie des langages ou des algorithmes.

Spéculativement, cela pourrait être un décalage entre les stratégies actuelles de la théorie des catégories et celles de la théorie A:

• La stratégie centrale de la théorie des catégories a trait à l'égalité (quand les choses sont identiques, quand elles sont différentes et comment elles se correspondent).

• Pour la théorie de la complexité, la stratégie principale consiste à réduire et à fixer des limites (on pourrait penser que la réduction est comme une flèche, mais je ne pense pas que rien de plus que cette similarité superficielle ait été étudié).

• Pour les algorithmes, il n’ya pas de stratégie globale autre que la pensée combinatoire intelligente et ad hoc. Pour certains domaines, je pense qu’il pourrait y avoir une exploration fructueuse (algorithmes pour les algèbres?), Mais je ne l’ai pas encore vue.

Les applications "TCS-A" qui me viennent à l’esprit sont les espèces combinatoires de Joyal (généralisations des séries de puissances aux foncteurs de manière à décrire des objets combinatoires comme des arbres, des ensembles, des multisets, etc.) et la formalisation de "sauts de jeu" cryptographiques par le biais de relations, la logique probabiliste de Hoare (Easycrypt, Certicrypt, le travail d'Andreas Lochbihler). Bien que les catégories n'apparaissent pas directement dans ces dernières, elles ont joué un rôle déterminant dans le développement des logiques sous-jacentes (par exemple, les monades).

PS: Depuis mon nom a été mentionné dans la première réponse: l'utilisation de fibrations de groupoïdes pour montrer la nondionnabilité d'un certain axiome dans la théorie des types de Martin-Löf par Thomas Streicher et moi-même peut également être considérée comme une utilisation "solide" de la théorie des catégories (bien que en logique ou "TCS-B").

Le livre plus récent Seven Sketches in Compositionality énumère plusieurs applications de la théorie des catégories en informatique et en génie. Il convient de noter le chapitre sur les bases de données dans lequel les auteurs décrivent les bases de données interrogées, combinées, migrées et évolutives basées sur un modèle catégorique. Les auteurs ont approfondi cette démarche et mis au point le langage de requête catégorique (CQL) et un environnement de développement intégré (IDE) basé sur leur modèle de bases de données catégoriel.