Monoïde des traces

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 Cartier et Foata 1969. 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 Mazurkiewicz 1977.

Définition modifier

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.

Exemple modifier

 
Graphe d'indépendance
 
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.

Traces modifier

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. Le morphisme de   sur   qui associe à un mot   sa trace, notée  , est appelé le morphisme canonique.

Si la relation   est vide, le monoïde   est le monoïde libre sur  . Si  , alors   est le monoïde commutatif libre sur  .

Exemple (suite) modifier

Pour la relation   donnée dans l'exemple, on a

 

Pour un mot   de  , on note   l'ensemble des lettres qui apparaissent dans  . Comme tous les mots de la trace   ont le même alphabet, l'écriture  , où   est une trace, a un sens.

Une trace   est connexe si toutes les lettres de   appartiennent à la même composante connexe de  . Deux traces   et   sont indépendantes si  .

Propriétés modifier

Lemme de projection modifier

On note   le morphisme de projection de   dans lui-même qui efface toutes les lettres sauf   et   et laisse ces deux lettres inchangées.

Soient  . On a   si et seulement si   pour tout  .

Simplifiabilité modifier

Le monoïde de traces   est un semi-groupe, c'est-à-dire que pour  , l'équation   implique  .

Lemme de Levi modifier

Le résultat suivant est l'analogue, pour les monoïdes de traces, du lemme de Levi des monoïdes libres.

Soient  ,  ,  ,   des traces. Si  , il existe des traces  , avec   indépendantes, telles que

 .

Formes normales modifier

Il existe deux formes normales pour les éléments d'un monoïde partiellement commutatif libre, la forme normale lexicographique et la forme normale de Foata. La forme normale lexicographique est due à Anatolij V. Anisimov et Donald Knuth, la forme normale de Foata est due à Pierre Cartier et Dominique Foata qui ont étudié le monoïde des traces pour ses propriétés combinatoires.

L'alphabet   est supposé totalement ordonné. On note   l'ordre lexicographique induit sur  . Un mot   de   est en forme normale lexicographique s'il est minimal, pour cet ordre, parmi les mots de la trace  . Comme chaque trace est finie et que l'ordre lexicographique est un ordre total, toute trace a un unique représentant minimal qui est la forme normal lexicographique de la trace.

Un mot   de   est en forme normale de Foata si   est le mot vide ou si   est le produit de   mots non vides   tels que

  • chaque mot   est composé de lettres qui commutent deux-à-deux, et   est lexicographiquement minimal.
  • pour chaque   et pour chaque lettre   de  , il existe une lettre   de   telle que  .

Exemple (suite) modifier

La forme normale lexicographique de   est  , et forme normale de Foata de   est  .

Langages de traces modifier

Un langage de traces est simplement un ensemble de traces. On peut considérer un tel ensemble comme l'image, par le morphisme canonique, d'un langage de mots.

Source modifier

Diekert et Métivier 1997

Références modifier

Ouvrages de référence modifier

  • (en) Volker Diekert et Yves Métivier, « Partial Commutation and Traces », dans G. Rozenberg, A. Salomaa (éditeurs), Handbook of Formal Languages, vol. 3 : Beyond Words, Springer Verlag, (ISBN 978-3-5406-0649-9, lire en ligne), p. 457-533
  • (en) Volker Diekert et Gregorz Rozenberg (éditeurs), The Book of Traces, Singapour, World Scientific, , 576 p. (ISBN 978-981-02-2058-7, LCCN 94039387, lire en ligne)
  • (en) Antoni Mazurkiewicz, « Introduction to Trace Theory », dans V. Diekert, G. Rozenberg (éditeurs), The Book of Traces, World Scientific, (ISBN 9810220588), p. 3–41
  • (en) Volker Diekert, « Combinatorics on traces », Lecture Notes in Computer Science, vol. 454,‎ , p. 9-29 (ISBN 3540530312)

Travaux historiques modifier

Voir aussi modifier

Langage formel