Trace monoid

Traces were introduced by Pierre Cartier and Dominique Foata in 1969 to give a combinatorial proof of MacMahon's master theorem. Traces are used in theories of concurrent computation, where commuting letters stand for portions of a job that can execute independently of one another, while non-commuting letters stand for locks, synchronization points or thread joins.

The trace monoid is constructed from the free monoid (the set of all strings of finite length) as follows. First, sets of commuting letters are given by an independency relation. These induce an equivalence relation of equivalent strings; the elements of the equivalence classes are the traces. The equivalence relation then partitions the elements of the free monoid into a set of equivalence classes; the result is still a monoid; it is a quotient monoid now called the trace monoid. The trace monoid is universal, in that all dependency-homomorphic (see below) monoids are in fact isomorphic.

Trace monoids are commonly used to model concurrent computation, forming the foundation for process calculi. They are the object of study in trace theory. The utility of trace monoids comes from the fact that they are isomorphic to the monoid of dependency graphs; thus allowing algebraic techniques to be applied to graphs, and vice versa. They are also isomorphic to history monoids, which model the history of computation of individual processes in the context of all scheduled processes on one or more computers.

Trace

Let ${\displaystyle {\mathrm{\Sigma }}^{\ast }}$ denote the free monoid on a set of generators ${\displaystyle \mathrm{\Sigma }}$, that is, the set of all strings written in the alphabet ${\displaystyle \mathrm{\Sigma }}$. The asterisk is a standard notation for the Kleene star. An independency relation ${\displaystyle I}$ on the alphabet ${\displaystyle \mathrm{\Sigma }}$ then induces a symmetric binary relation ${\displaystyle \sim }$ on the set of strings ${\displaystyle {\mathrm{\Sigma }}^{\ast }}$: two strings ${\displaystyle u,v}$ are related, ${\displaystyle u\sim v,}$ if and only if there exist ${\displaystyle x,y\in {\mathrm{\Sigma }}^{\ast }}$, and a pair ${\displaystyle (a,b)\in I}$ such that ${\displaystyle u=xaby}$ and ${\displaystyle v=xbay}$. Here, ${\displaystyle u,v,x}$ and ${\displaystyle y}$ are understood to be strings (elements of ${\displaystyle {\mathrm{\Sigma }}^{\ast }}$), while ${\displaystyle a}$ and ${\displaystyle b}$ are letters (elements of ${\displaystyle \mathrm{\Sigma }}$).

The trace is defined as the reflexive transitive closure of ${\displaystyle \sim }$. The trace is thus an equivalence relation on ${\displaystyle {\mathrm{\Sigma }}^{\ast }}$ and is denoted by ${\displaystyle {\equiv }_D}$, where ${\displaystyle D}$ is the dependency relation corresponding to ${\displaystyle I.}$ ${\displaystyle D=(\mathrm{\Sigma }\times \mathrm{\Sigma })\setminus I}$ and ${\displaystyle I=(\mathrm{\Sigma }\times \mathrm{\Sigma })\setminus D.}$ Different independencies or dependencies will give different equivalence relations.

The transitive closure implies that ${\displaystyle u{\equiv }_{D}v}$ if and only if there exists a sequence of strings ${\displaystyle (w_0,w_1,\cdots ,w_n)}$ such that ${\displaystyle u\sim w_0,}$ ${\displaystyle v\sim w_n,}$ and ${\displaystyle w_i\sim w_{i+1}}$ for all ${\displaystyle 0\le i<n}$. The trace is stable under the monoid operation on ${\displaystyle {\mathrm{\Sigma }}^{\ast }}$, i.e., concatenation, and ${\displaystyle {\equiv }_D}$ is therefore a congruence relation on ${\displaystyle {\mathrm{\Sigma }}^{\ast }.}$

The trace monoid, commonly denoted as ${\displaystyle \mathbb{M}(D)}$, is defined as the quotient monoid

${\displaystyle \mathbb{M}(D)={\mathrm{\Sigma }}^{\ast }/{\equiv }_D.}$

The homomorphism

${\displaystyle {\varphi }_D:{\mathrm{\Sigma }}^{\ast }\to \mathbb{M}(D)}$

is commonly referred to as the natural homomorphism or canonical homomorphism. That the terms natural or canonical are deserved follows from the fact that this morphism embodies a universal property, as discussed in a later section.

One will also find the trace monoid denoted as ${\displaystyle M(\mathrm{\Sigma },I)}$ where ${\displaystyle I}$ is the independency relation. One can also find the commutation relation used instead of the independency relation; it differs from the independency relation by also including all the diagonal elements of $\mathrm{\Sigma }\times \mathrm{\Sigma }$ since letters "commute with themselves" in a free monoid of strings of those letters.