Concept
En mathématiques et en informatique, une trace est un ensemble de mots, où certaines lettres peuvent commuter, et d'autres non. Le monoïde des traces ou monoïde partiellement commutatif libre est le monoïde quotient du monoïde libre par une relation de commutation de lettres. Le monoïde des traces est donc une structure qui se situe entre le monoïde libre et le monoïde commutatif libre. L'intérêt mathématique du monoïde des traces a été mis en évidence dans l'ouvrage fondateur . Les traces apparaissent dans la modélisation en programmation concurrente, où les lettres qui peuvent commuter représentent des parties de processus qui peuvent s'exécuter de façon indépendante, alors que les lettres qui ne commutent pas représentent des verrous, leur synchronisation ou l'union de threads. Ce modèle a été proposé dans . Soit un alphabet. Une relation d'indépendance ou relation de commutation est une relation binaire sur qui est irréflexive et symétrique. Le couple est le graphe d'indépendance ou graphe de commutation. Le complément d'une relation d'indépendance est une relation de dépendance. C'est une relation réflexive et symétrique. Le couple est le graphe de dépendance. thumb|Graphe d'indépendance thumb|Graphe de dépendance Soit et . Le graphe d'indépendance et le graphe de dépendance, si l'on omet les boucles, sont décrits dans les figures ci-contre. La relation d'indépendance induit sur une relation d'équivalence notée . Deux mots et sont équivalents modulo s'il existe une suite de mots tels que , , et pour il existe des mots et des lettres tels que et et Ainsi, deux mots sont équivalents exactement quand ils peuvent être obtenus, l'un de l'autre, par une suite de transpositions de lettres indépendantes adjacentes. La relation est une congruence. Le quotient de par est donc un monoïde. C'est le monoïde partiellement commutatif libre induit par Il est noté . Les éléments de qui ont les classes d'équivalence de mots pour la relation , sont appelés des traces, et le monoïde est appelé le monoïde des traces.