Trace monoid

In computer science, a trace is a set of strings, wherein certain letters in the string are allowed to commute, but others are not. It generalizes the concept of a string, by not forcing the letters to always be in a fixed order, but allowing certain reshufflings to take place. 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 or free partially commutative monoid is a monoid of traces. In a nutshell, it is constructed as follows: 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 up the free monoid (the set of all strings of finite length) into a set of equivalence classes; the result is still a monoid; it is a quotient monoid and is 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 formula_1 denote the free monoid, that is, the set of all strings written in the alphabet formula_2. Here, the asterisk denotes, as usual, the Kleene star. An independency relation formula_3 on formula_2 then induces a binary relation formula_5 on formula_1, where formula_7 if and only if there exist formula_8, and a pair formula_9 such that formula_10 and formula_11. Here, formula_12 and formula_13 are understood to be strings (elements of formula_1), while formula_15 and formula_16 are letters (elements of formula_2).
The trace is defined as the symmetric, reflexive and transitive closure of formula_5. The trace is thus an equivalence relation on formula_1, and is denoted by formula_20. The subscript "D" on the equivalence simply denotes that the equivalence is obtained from the independency "I" induced by the dependency "D". Clearly, different dependencies will give different equivalence relations.
The transitive closure simply implies that formula_21 if and only if there exists a sequence of strings formula_22 such that formula_23 and formula_24 and formula_25 for all formula_26. The trace is stable under the monoid operation on formula_1 (concatenation) and is therefore a congruence relation on formula_1.
The trace monoid, commonly denoted as formula_29, is defined as the quotient monoid
The homomorphism 
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.
Examples.
Consider the alphabet formula_32. A possible dependency relation is
The corresponding independency is
Therefore, the letters formula_35 commute. Thus, for example, a trace equivalence class for the string formula_36 would be
The equivalence class formula_38 is an element of the trace monoid.
Properties.
The cancellation property states that equivalence is maintained under right cancellation. That is, if formula_39, then formula_40. Here, the notation formula_41 denotes right cancellation, the removal of the first occurrence of the letter "a" from the string "w", starting from the right-hand side. Equivalence is also maintained by left-cancellation. Several corollaries follow:
A strong form of Levi's lemma holds for traces. Specifically, if formula_51 for strings "u", "v", "x", "y", then there exist strings formula_52 and formula_53 such that formula_54
for all letters formula_55 and formula_56 such that formula_57 occurs in formula_58 and formula_59 occurs in formula_60, and
Universal property.
A dependency morphism (with respect to a dependency "D") is a morphism
to some monoid "M", such that the "usual" trace properties hold, namely:
Dependency morphisms are universal, in the sense that for a given, fixed dependency "D", if formula_63 is a dependency morphism to a monoid "M", then "M" is isomorphic to the trace monoid formula_74. In particular, the natural homomorphism is a dependency morphism.
Normal forms.
There are two well-known normal forms for words in trace monoids. One is the "lexicographic" normal form, due to Anatolij V. Anisimov and Donald Knuth, and the other is the "Foata" normal form due to Pierre Cartier and Dominique Foata who studied the trace monoid for its combinatorics in the 1960s.
Trace languages.
Just as a formal language can be regarded as a subset of formula_1 the set of all possible strings, so then a trace language is defined as subset of formula_74 all possible traces.
A language formula_77 is a trace language, or is said to be consistent with dependency "D" if
where
is the trace closure of a set of strings.
References.
General references
Seminal publications