In computer science, a trace is an equivalence class of stringss, 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. The trace monoid or free partially commutative monoid is a monoid of traces.

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 pointss or thread joinss.

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 graphss, 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

. The asterisk is a standard notation for the Kleene star. An independency relation if and only if).

The trace is defined as the reflexive transitive closure. The trace is thus an equivalence relation Different independencies or dependencies will give different equivalence relations.

The transitive closure, i.e., concatenation is therefore a congruence relation

, 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.

since letters "commute with themselves" in a free monoid of strings of those letters.

Examples

. A possible dependency relation is

The corresponding independency is

would be

would be an element of the trace monoid.

Properties

The cancellation property states that equivalence is maintained under right cancellation 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:

• for strings x and y. Thus, the trace monoid is a syntactic monoid.

• , then a is independent of b. Furthermore, there exists a string w.

• Projection rule: equivalence is maintained under string projection.

A strong form of Levi's lemma for strings u, v, x, y, 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 is a dependency morphism to a monoid M, then M is isomorphic. 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.

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.

Trace languages

all possible traces.

is a trace language, or is said to be consistent with dependency D if

where

is the trace closure of a set of strings.

See also

• Trace cache

Notes

References

General references

• Antoni Mazurkiewicz, "Introduction to Trace Theory", pp 3–41, in The Book of Traces, V. Diekert, G. Rozenberg, eds. (1995) World Scientific, Singapore

• Volker Diekert, Combinatorics on traces, LNCS 454, Springer, 1990, , pp.9–29

Seminal publications

• Pierre Cartier and Dominique Foata, Problèmes combinatoires de commutation et réarrangements, Lecture Notes in Mathematics 85, Springer-Verlag, Berlin, 1969, Free 2006 reprint with new appendixes

• Antoni Mazurkiewicz, Concurrent program schemes and their interpretations, DAIMI Report PB 78, Aarhus University, 1977