In mathematics and 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 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 homomorphic 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.
Contents |
Let Σ * denote the free monoid, that is,
the set of all strings written in the alphabet Σ. Here, the asterisk denotes, as usual, the
Kleene star. An independency relation I then induces a binary relation
˜ on Σ
* , where
if and only if there exist
,
and a pair
such that u =
xaby and v =
xbay. Here, u,v,x and y are understood to be strings
(elements of Σ * ), while
a and b are letters (elements of Σ).
The trace is defined as the symmetric,
reflexive and transitive closure of ˜. The trace is thus an equivalence relation on Σ * , and is denoted by
.
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
if and only if there exists a sequence of strings
such that
and
and
for all
.
The trace monoid, commonly denoted as
,
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.
Consider the alphabet Σ = {a,b,c}. A possible dependency relation is

The corresponding independency is

Therefore, the letters b,c commute. Thus, for example, a trace equivalence class for the string ababa bbca would be
![[abababbca]_D = \{abababbca\,,\; abababcba\,,\; ababacbba \}](http://images-mediawiki-sites.thefullwiki.org/01/3/6/7/3198441153458522.png)
The equivalence class [ababa bbca]D is an element of the trace monoid.
The cancellation property states that
equivalence is maintained under right
cancellation. That is, if
,
then
.
Here, the notation
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:
if and only if
for strings x and y. Thus, the trace monoid is a
syntactic
monoid.
and
,
then a is independent of b. That is,
.
Furthermore, there exists a string w such that u = wb and v = wa.
,
then
.A strong form of Levi's lemma holds for traces.
Specifically, if
for strings u, v, x, y, then
there exist strings z1,z2,z
3 and z4 such that
,
and


A dependency morphism (with respect to a dependency D) is a morphism

to some monoid M, such that the "usual" trace properties hold, namely:
implies that 
implies that 
implies that 
and
imply that 
Dependency morphisms are universal, in the sense that for a
given, fixed dependency D, if
is a dependency morphism to a monoid M, then M is
isomorphic to the trace monoid
.
In particular, the natural homomorphism is a dependency
morphism.
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.
Just as a formal language can be regarded as a
subset of Σ * the set of
all possible strings, so then a trace language is defined as subset
of
all possible traces.
A language
is a trace language, or is said to be consistent
with dependency D if
![L=\bigcup [L]_D](http://images-mediawiki-sites.thefullwiki.org/10/5/5/0/949134341186121.png)
where
![[L]_D=\{[w]_D \vert w\in L \}](http://images-mediawiki-sites.thefullwiki.org/01/2/7/8/31612813077626.png)
is the trace closure of a set of strings, and
![\bigcup T = \{w \vert [w]_D\in T \}](http://images-mediawiki-sites.thefullwiki.org/10/2/3/0/87657743650630011.png)
is the set of strings in a set of traces.
General references
Seminal publications
|
|