Catégories, Homotopie et Réécriture – CATHRE

Le projet Cathre prend ses racines dans les travaux de Squier et d'Anick, notamment, sur les propriétés des présentations de monoïdes et d'algèbres. En particulier, Squier a montré que, si un monoïde M admet une présentation par un système de réécriture fini, confluent et terminant, alors son troisième groupe d'homologie intégrale H_3(M,Z) est finiment engendré en tant que groupe abélien. Plus tard, il a raffiné ce résultat pour prouver que, sous les mêmes hypothèses, M est de type de dérivation fini, une propriété de nature homotopique. Nous pensons qu'il ne s'agit pas de résultats isolés mais qu'ils doivent faire partie d'une vaste théorie homotopique de la réécriture, comprenant les mots, les termes, les combinaisons linéaires de termes, ainsi que différents types de diagrammes.
Le projet a pour but de développer une telle théorie, ainsi que des outils calculatoires basés sur celle-ci, à partir des deux observations suivantes :
- tous les objets étudiés, tels que les mots, les termes ou les règles de réécriture peuvent être exprimés naturellement dans le langage des catégories (strictes, globulaires) de dimension supérieure ;
- la catégorie de ces catégories supérieures possède une structure homotopique non triviale.
Même dans le cas simple des monoïdes, des dimensions arbitrairement élevées apparaissent dans le processus de résolution : le calcul d'invariants homotopiques ou homologiques tient compte des mots, en dimension 1, et des chemins de réécriture, en dimension 2, mais aussi des déformations entre chemins, en dimension 3, et ainsi de suite. Notre approche est étayée par des résultats forts déjà obtenus dans cette direction:
- l'analyse de nombreux exemples de réécriture en dimension supérieure par Yves Guiraud et Philippe Malbos,
- la découverte d'une structure de modèle naturelle sur les catégories supérieures par Yves Lafont, François Métayer et Krzysztof Worytkiewicz.
Le projet Cathre propose de développer ces deux directions de recherche avec pour objectifs de produire un système de calcul, capable de manipuler différentes sortes de structures algébriques, et d'explorer trois domaines d'application :
- en algèbre formelle, pour le calcul dans des algèbres et des opérades,
- en théorie combinatoire des groupes, pour le calcul dans des groupes intervenant en algèbre et en géométrie,
- en réécriture de terme, pour la programmation fonctionnelle.