Existe-t-il une théorie qui combine théorie des catégories / algèbre abstraite et complexité informatique?

La théorie des catégories et l'algèbre abstraite traitent de la façon dont les fonctions peuvent être combinées avec d'autres fonctions. La théorie de la complexité traite de la difficulté de calculer une fonction. C'est bizarre pour moi que je n'ai vu personne combiner ces domaines d'études, car ils ressemblent à de telles paires naturelles. Quelqu'un a-t-il déjà fait cela?

À titre d'exemple motivant, examinons les monoïdes. Il est bien connu que si une opération est monoïde, alors nous pouvons paralléliser l'opération.

Par exemple dans Haskell, nous pouvons définir trivialement que l'addition est un monoïde sur les entiers comme ceci:

instance Monoid Int where
    mempty = 0
    mappend = (+)

Maintenant, si nous voulons calculer la somme de 0 à 999, nous pourrions le faire séquentiellement comme:

foldl1' (+) [0..999]

ou on pourrait le faire en parallèle

mconcat [0..999] -- for simplicity of the code, I'm ignoring that this doesn't *actually* run in parallel

Mais paralléliser ce monoïde n'a de sens que parce que mappend s'exécute en temps constant. Et si ce n'était pas le cas? Les listes, par exemple, sont des monoïdes où mappend n'exécute pas de temps (ou d'espace!) Inconstant. Je suppose que c'est pourquoi il n'y a pas de fonction mconcat parallèle par défaut dans Haskell. La meilleure mise en œuvre dépend de la complexité du monoïde.

Il semble qu'il devrait y avoir un moyen pratique de décrire les différences entre ces deux monoïdes. Nous devrions alors être en mesure d'annoter notre code avec ces différences et que les programmes choisissent automatiquement les meilleurs algorithmes à utiliser en fonction de la complexité d'un monoïde.

[La complexité informatique et la théorie des catégories] semblent être de telles paires naturelles.

Compte tenu de l'importance de la complexité informatique en tant que domaine de recherche, s'il s'agissait de compagnons naturels, peut-être que quelqu'un aurait déjà fait ressortir le lien?

Spéculation sauvage. Permettez-moi de divertir le lecteur avec des réflexions sur les raisons pour lesquelles un rendu catégorique de la complexité de calcul est difficile. On peut soutenir que le groupe de concepts clés dans la théorie des catégories se concentre sur les constructions / propriétés universelles (avec l'appareil de foncteurs associé, les transformations naturelles, les adjonctions, etc.). Si nous pouvons montrer qu'une construction mathématique a une propriété universelle, cela donne beaucoup de perspicacité. Donc, si nous voulions une approche catégorielle de la complexité de calcul, nous aurions besoin de trouver une catégorie pratique et de montrer comment les concepts clés de la théorie de la complexité (par exemple LOGSPACE ou NP-hardness) peuvent être donnés par des constructions universelles utilisant cette catégorie. Cela n'a pas encore été fait, et je pense que c'est parce que c'est un problème vraiment difficile.

Je soupçonne que la raison de cette difficulté est que l'objet clé de la théorie de la complexité, la machine de Turing, n'est pas bien compris algébriquement. Le problème avec les MT est qu'elles ne sont pas naturellement équipées d'une belle algèbre qui permet de construire des programmes de manière compositionnelle. J'entends par là que nous ne programmons généralement pas de MT en disant que notre programme cible est le TM T qui est composé par exemple de où les sont des TM plus petites et sont opérateurs algébriques sur les MT: nous n'avons tout simplement pas d'opérations algébriques (naturelles) sur les MT qui nous permettent de construire des MT par étapes de manière perspicace ¹T i ⊕ , $T = T_1 \oplus T_2 \otimes T_3$$T_i$$\oplus, \otimes$. Au lieu de cela, nous construisons des MT en spécifiant leurs deux composants séparément: le contrôle (un FSM) et la bande. Ni le contrôle ni la bande n'ont eux-mêmes de bonnes algèbres.

Regardons d'abord les bandes. Il existe deux façons naturelles de composer des bandes, dont aucune ne semble fonctionner pour une description de la composition des MT.

• Collez-les ensemble comme addition ordinale. Ce n'est pas la bonne idée, parce que les bandes sont infinies et en les collant comme une addition ordinale, nous obtenons un double objet infini qui va au-delà de la calculabilité finie, conduisant à un calcul / hyper-calcul infini, qui sont intéressants en tant que mathématiques mais ne correspondent pas à calcul possible.

• Collez-les en parallèle , par exemple deux machines à 3 têtes se transforment en une machine à 6 têtes. Cela ne nous dit pas comment les machines composants interagissent entre elles.

• Bandes entrelacées. Un problème avec cette approche est qu'il n'est pas clair ce que l'entrelacement canonique pourrait être, le cas échéant. De plus, l'entrelacement «confondra» le contrôle existant, qui a tendance à être finement réglé vers une disposition de bande spécifique. Nous ne pouvons donc pas réutiliser le contrôle directement.

Avec les FSM, la situation est un peu meilleure, car nous avons des théories algébriques significatives sur le plan du calcul de la construction d'automates, dont les plus connues pourraient être des algèbres de processus comme CSP, CCS, -calculus, ACP, etc. Mais aucun d'eux n'est un calcul des mouvements de la tête de bande, ce dont nous aurions besoin si nous voulions composer des MT.$\pi$

Dans l'ensemble, nous sommes assez loin d'un traitement algébrique / catégorique substantiel de la complexité informatique, et nous aurions besoin de plusieurs avancées conceptuelles pour y arriver.

¹ Notez que ceci est assez différent des autres formalismes de calcul comme -calculus et -calculus, qui sont des calculs algébriques. Parce qu'ils sont algébriques, il a été facile de développer des théories de type pour -calculus et -calculus comme moyen de contraindre les programmes. Cependant, ces calculs ont des opérations puissantes comme la génération de nouveaux noms, l'extrusion de portée, conversion et la copie illimitée de termes, ce qui les rend a priori inadaptés comme formalismes de base pour la théorie de la complexité. En effet, on peut facilement montrer par exemple P = NP si on ne fait pas attention. Ce n'est qu'en 2014 qu'Accattoli et Dal Lago ont montré (dans: Beta Reduction is Invariant, Indeed ) queπ λ π α λ $\lambda$$\pi$$\lambda$$\pi$$\alpha$$\lambda$ -calculus peut être utilisé pour définir la complexité temporelle si l'on fait attention. Aucun résultat correspondant n'est connu pour la complexité de l'espace ou pour -calculus.$\pi$

Cette réponse sur les isomorphismes entre les langages formels combine les résultats algébriques de la théorie des codes avec des notions de la théorie des catégories pour étudier les notions possibles d'équivalence et d'isomorphisme entre les langages formels et les classes de complexité.

Ma propre interprétation de ces résultats est que les points de synchronisation dans les mots sont différents pour les transducteurs déterministes et non ambiguës non déterministes, et même différents entre les transducteurs déterministes avant et déterministes arrière. Prendre cette perspective des points de synchronisation permet de relier ces résultats à des langages visuellement déroulants, et pose la question de savoir si ceux-ci devraient également considérer de simples séparateurs (comme un espace ou une virgule) en plus des appels et des retours. (Je suppose qu'un séparateur pourrait être émulé par un appel combiné retour + appel, mais comme ceux-ci nécessitent deux symboles au lieu d'un, il n'est pas clair pour moi si cela est suffisant. Il pourrait également y avoir visiblement des langues qui n'ont que des séparateurs, mais pas appeler ou renvoyer des symboles.)