Descriptions calculatoires de catégories supérieures

Higher categories are algebraic structures consisting of cells of various dimensions equipped with notions of composition, which have found many applications in mathematics (algebraic topology in particular) and theoretical computer science. They are notably complicated structures whose manipulation is technical and error-prone. The purpose of this thesis is to introduce several computational tools for strict and semi-strict variants of higher categories that ease the study of these objects. In order to represent higher categories as finite data, so that they can be given as input to a program, we use the structure of polygraph, initially introduced by Street and Burroni for strict categories and then generalized by Batanin to any algebraic theory of higher category, which allows presenting higher categories by means of systems of generators. The first problem tackled by this thesis is then the one of the word problem on strict categories, which consists in deciding whether two formal composites of cells of strict categories represent the same cell. We give an implementable and relatively efficient solution for it by improving the decidability procedure initially given by Makkai. Then, we turn to pasting diagram formalisms for strict categories, which enable to efficiently represent cells of strict categories using set-like structures and for which a reliable implementation is desirable. We consider the three main formalisms which have been introduced until now, namely Street's parity complexes, Johnson's pasting schemes and Steiner's augmented directed complexes. Our study reveals that the axiomatics of the first two ones are defective, which motivates the introduction of a new structure, called torsion-free complexes, whose axioms have nice properties and generalize those of the three other formalisms. We also show that they are amenable to concrete computation, by providing an implementation of those. Finally, we consider the problem of coherence of presentations of algebraic structures expressed in 3-dimensional weak categories, the latter being known to be equivalent to Gray categories. Taking inspiration from a celebrated result given by Squier in the context of monoids, we adapt the classical tools from rewriting theory to the setting of Gray categories and relate the coherence of presentations of Gray categories to the confluence of the critical branchings of an associated rewriting system. From this result, we deduce a semi-automated procedure to find coherent presentations of Gray categories that we apply on several examples.Les catégories supérieures sont des structures algébriques constituées de cellules de différentes dimensions et équipées d'opérations de composition. Elles ont trouvé plusieurs applications en mathématiques (en particulier, dans le domaine de la topologie algébrique) et en informatique théorique. Ce sont des structures notoirement complexes, dont la manipulation est technique et sujette aux erreurs. Le but de cette thèse est d'introduire plusieurs outils informatiques pour les variantes strictes et semi-strictes des catégories supérieures qui facilitent l'étude de ces objets. Afin de répresenter les catégories supérieures par des données finies, de sorte que ces dernières puissent être transmises comme entrée à un programme, on utilise la structure de polygraphe, initialement introduite par Street et Burroni pour les catégories strictes, et généralisée par Batanin à toute théorie algébrique de catégorie supérieure, qui permet de présenter des catégories supérieures par des systèmes de générateurs. Le premier problème abordé par cette thèse est celui du problème du mot sur les catégories strictes, qui consiste à déterminer si deux composées formelles de cellules d'une catégorie stricte représentent la même cellule. On donne une solution implémentable et relativement efficace pour ce problème en améliorant la procédure de décision initialement donnée par Makkai. Ensuite, nous traitons les formalismes pour les diagrammes de recollement. Ces derniers permettent de représenter efficacement les cellules de catégories strictes en utilisant des structures ensemblistes et pour lesquels une implémentation efficace est désirable. On étudie en particulier les trois principaux formalismes qui ont été introduits jusqu'ici : les complexes de parité de Street, les schémas de recollement de Johnson et les complexes dirigés augmentés de Steiner. Notre étude révèle que les axiomatiques des deux premiers est défectueuse, ce qui motive l'introduction d'une nouvelle structure, appelée complexe sans torsion, dont les axiomes ont de bonnes propriétés et généralisent ceux des autres formalismes. On montre que cette nouvelle structure est adéquate pour représenter informatiquement les catégories strictes en en donnant une implémentation. Pour finir, on considère le problème des présentations cohérentes de structures algébriques exprimées dans les catégories faibles de dimension 3, ces dernières étant connues pour être équivalentes aux catégories de Gray. En s'inspirant d'un résultat important de Squier dans le context des monoïdes, on adapte les résultats classiques de la théorie de la réécriture au contexte des catégories de Gray et relions la cohérence de présentations de catégories de Gray à la confluence de branchements critiques d'un système de réécriture associé. Avec ce résultat, nous déduisons une procédure semi-automatique pour produire des présentations cohérentes de catégories de Gray, et nous l'appliquons sur plusieurs exemples