In computer science, a trace is an equivalence class of strings, wherein certain letters in the string are allowed to commute, but others are not.
Traces generalize the concept of strings by relaxing the requirement for all the letters to have a definite order, instead allowing for indefinite orderings in which certain reshufflings could take place.
In an opposite way, traces generalize the concept of sets with multiplicities by allowing for specifying some incomplete ordering of the letters rather than requiring complete equivalence under all reorderings.
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.
[1] 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.
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.
denote the free monoid on a set of generators
, that is, the set of all strings written in the alphabet
The asterisk is a standard notation for the Kleene star.
then induces a symmetric binary relation
The trace is defined as the reflexive transitive closure of
The trace is stable under the monoid operation on
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
A possible dependency relation is The corresponding independency is Therefore, the letters
Thus, for example, a trace equivalence class for the string
denotes right cancellation, the removal of the first occurrence of the letter a from the string w, starting from the right-hand side.
Several corollaries follow: A strong form of Levi's lemma holds for traces.
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.
[3] Unicode's Normalization Form Canonical Decomposition (NFD) is an example of a lexicographic normal form - the ordering is to sort consecutive characters with non-zero canonical combining class by that class.
Just as a formal language can be regarded as a subset of
, the set of all possible strings, so a trace language is defined as a subset of
General references Seminal publications