Calcul symbolique avec des diagrammes de Penrose / Anne Massol ; sous la direction de Yves Lafont

Bibliogr. p. 121

Thèse de doctorat informatique et mathématiques 1997 université de la méditerranée

Nous nous intéressons à un calcul formel de type nouveau où les expressions sont remplacées par des diagrammes que l'on appelle diagrammes de Penrose. En s'appuyant sur la notion de catégorie monoïdale, Burroni a établi le fondement théorique de ce type de calcul. Lafont a proposé une définition formelle des diagrammes et a décrit quelques exemples de calculs planaires. Ces définitions et résultats sont rappelés dans le premier chapitre. Afin de faciliter l'utilisation de ce calcul nous avons réalisé un logiciel avec une interface graphique pour la manipulation de ces diagrammes. Ce travail est décrit dans le deuxième chapitre. Dans le troisième chapitre, nous étudions un certain nombre de problèmes algorithmiques liés à ce calcul (calcul de formes normales, reconnaissance de l'isotopie...). Dans le dernier chapitre, nous démontrons que la présentation finie proposée par Burroni et Lafont pour la catégorie monoïdale des ensembles finis (l'exemple de base de la théorie) est en fait minimale, c'est-à-dire qu'elle ne contient pas d'équation superflue. Cette preuve a été obtenue à l'aide de l'ordinateur par une recherche systématique de modèles finis.