In
computer science
Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to Applied science, practical discipli ...
, a trace is a set of
strings, wherein certain letters in the string are allowed to
commute
Commute, commutation or commutative may refer to:
* Commuting, the process of travelling between a place of residence and a place of work
Mathematics
* Commutative property, a property of a mathematical operation whose result is insensitive to th ...
, 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
Dominique Foata (born October 12, 1934) is a mathematician who works in enumerative combinatorics. With Pierre Cartier and Marcel-Paul Schützenberger he pioneered the modern approach to classical combinatorics, that lead, in part, to the current ...
in 1969 to give a combinatorial proof of
MacMahon's master theorem. Traces are used in theories of
concurrent computation
Concurrent computing is a form of computing in which several computations are executed '' concurrently''—during overlapping time periods—instead of ''sequentially—''with one completing before the next starts.
This is a property of a syst ...
, 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 join
In computer science, a thread of execution is the smallest sequence of programmed instructions that can be managed independently by a scheduler, which is typically a part of the operating system. The implementation of threads and processes dif ...
s.
[Sándor & Crstici (2004) p.161]
The trace monoid or free partially commutative monoid is a
monoid
In abstract algebra, a branch of mathematics, a monoid is a set equipped with an associative binary operation and an identity element. For example, the nonnegative integers with addition form a monoid, the identity element being 0.
Monoids ...
of traces. In a nutshell, it is constructed as follows: sets of commuting letters are given by an
independency relation
In computer science, in particular in concurrency (computer science), concurrency theory, a dependency relation is a binary relation on a finite domain \Sigma, symmetric relation, symmetric, and reflexive relation, reflexive; i.e. a finite toleran ...
. 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 In abstract algebra, the free monoid on a set is the monoid whose elements are all the finite sequences (or strings) of zero or more elements from that set, with string concatenation as the monoid operation and with the unique sequence of zero eleme ...
(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
In mathematics, a semigroup is an algebraic structure consisting of a set together with an associative internal binary operation on it.
The binary operation of a semigroup is most often denoted multiplicatively: ''x''·''y'', or simply ''xy ...
and is called the ''trace monoid''. The trace monoid is
universal
Universal is the adjective for universe.
Universal may also refer to:
Companies
* NBCUniversal, a media and entertainment company
** Universal Animation Studios, an American Animation studio, and a subsidiary of NBCUniversal
** Universal TV, a ...
, in that all dependency-homomorphic (see below) monoids are in fact
isomorphic
In mathematics, an isomorphism is a structure-preserving mapping between two structures of the same type that can be reversed by an inverse mapping. Two mathematical structures are isomorphic if an isomorphism exists between them. The word is ...
.
Trace monoids are commonly used to model
concurrent computation
Concurrent computing is a form of computing in which several computations are executed '' concurrently''—during overlapping time periods—instead of ''sequentially—''with one completing before the next starts.
This is a property of a syst ...
, forming the foundation for
process calculi
In computer science, the process calculi (or process algebras) are a diverse family of related approaches for formally modelling concurrent systems. Process calculi provide a tool for the high-level description of interactions, communications, and ...
. They are the object of study in
trace theory
In mathematics and computer science, trace theory aims to provide a concrete mathematical underpinning for the study of concurrent computation and process calculi. The underpinning is provided by an abstract algebra, algebraic definition of the fr ...
. The utility of trace monoids comes from the fact that they are isomorphic to the monoid of
dependency graph
In mathematics, computer science and digital electronics, a dependency graph is a directed graph representing dependencies of several objects towards each other. It is possible to derive an evaluation order or the absence of an evaluation order t ...
s; thus allowing algebraic techniques to be applied to
graph
Graph may refer to:
Mathematics
*Graph (discrete mathematics), a structure made of vertices and edges
**Graph theory, the study of such graphs and their properties
*Graph (topology), a topological space resembling a graph in the sense of discre ...
s, and vice versa. They are also isomorphic to
history monoid In mathematics and computer science, a history monoid is a way of representing the histories of concurrently running computer processes as a collection of strings, each string representing the individual history of a process. The history monoid p ...
s, which model the history of computation of individual processes in the context of all scheduled processes on one or more computers.
Trace
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
In mathematical logic and computer science, the Kleene star (or Kleene operator or Kleene closure) is a unary operation, either on sets of strings or on sets of symbols or characters. In mathematics,
it is more commonly known as the free monoid c ...
. An
independency relation
In computer science, in particular in concurrency (computer science), concurrency theory, a dependency relation is a binary relation on a finite domain \Sigma, symmetric relation, symmetric, and reflexive relation, reflexive; i.e. a finite toleran ...
on
then induces a (symmetric) binary relation
on
, where
if and only if there exist
, and a pair
such that
and
. Here,
and
are understood to be strings (elements of
), while
and
are letters (elements of
).
The trace is defined as the reflexive transitive closure of
. The trace is thus an equivalence relation on
, and is denoted by
, where
is the dependency relation corresponding to
that is
and conversely
Clearly, different dependencies will give different equivalence relations.
The
transitive closure
In mathematics, the transitive closure of a binary relation on a set is the smallest relation on that contains and is transitive. For finite sets, "smallest" can be taken in its usual sense, of having the fewest related pairs; for infinite ...
implies that
if and only if there exists a sequence of strings
such that
and
and
for all
. The trace is stable under the monoid operation on
(
concatenation
In formal language, formal language theory and computer programming, string concatenation is the operation of joining character string (computer science), character strings wikt:end-to-end, end-to-end. For example, the concatenation of "sno ...
) and is therefore a
congruence relation
In abstract algebra, a congruence relation (or simply congruence) is an equivalence relation on an algebraic structure (such as a group, ring, or vector space) that is compatible with the structure in the sense that algebraic operations done wi ...
on
.
The trace monoid, commonly denoted as
, is defined as the quotient monoid
:
The homomorphism
:
is commonly referred to as the
natural homomorphism
In category theory, a branch of mathematics, a natural transformation provides a way of transforming one functor into another while respecting the internal structure (i.e., the composition of morphisms) of the categories involved. Hence, a natura ...
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
where
is the independency relation. Confusingly, one can also find the commutation relation used instead of the independency relation (it differs by including all the diagonal elements).
Examples
Consider the alphabet
. A possible dependency relation is
:
The corresponding independency is
:
Therefore, the letters
commute. Thus, for example, a trace equivalence class for the string
would be
:
The equivalence class
is an element of the trace monoid.
Properties
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:
* Embedding:
if and only if
for strings ''x'' and ''y''. Thus, the trace monoid is a syntactic monoid.
* Independence: if
and
, then ''a'' is independent of ''b''. That is,
. Furthermore, there exists a string ''w'' such that
and
.
* Projection rule: equivalence is maintained under
string projection In computer science, in the area of formal language theory, frequent use is made of a variety of string functions; however, the notation used is different from that used for computer programming, and some commonly used functions in the theoretical r ...
, so that if
, then
.
A strong form of
Levi's lemma
In theoretical computer science and mathematics, especially in the area of combinatorics on words, the Levi lemma states that, for all strings ''u'', ''v'', ''x'' and ''y'', if ''uv'' = ''xy'', then there exists a string ''w'' such tha ...
holds for traces. Specifically, if
for strings ''u'', ''v'', ''x'', ''y'', then there exist strings
and
such that
for all letters
and
such that
occurs in
and
occurs in
, 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:
:1.
implies that
:2.
implies that
:3.
implies that
:4.
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
In mathematics, an isomorphism is a structure-preserving mapping between two structures of the same type that can be reversed by an inverse mapping. Two mathematical structures are isomorphic if an isomorphism exists between them. The word is ...
to the trace monoid
. 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
Lexicography is the study of lexicons, and is divided into two separate academic disciplines. It is the art of compiling dictionaries.
* Practical lexicography is the art or craft of compiling, writing and editing dictionaries.
* Theoretica ...
'' normal form, due to Anatolij V. Anisimov and
Donald Knuth
Donald Ervin Knuth ( ; born January 10, 1938) is an American computer scientist, mathematician, and professor emeritus at Stanford University. He is the 1974 recipient of the ACM Turing Award, informally considered the Nobel Prize of computer sc ...
, and the other is the ''Foata'' normal form due to
Pierre Cartier and
Dominique Foata
Dominique Foata (born October 12, 1934) is a mathematician who works in enumerative combinatorics. With Pierre Cartier and Marcel-Paul Schützenberger he pioneered the modern approach to classical combinatorics, that lead, in part, to the current ...
who studied the trace monoid for its
combinatorics in the 1960s.
[Section 2.3, Diekert and Métivier 1997.]
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
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
all possible traces.
Alternatively, but equivalently, a language
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
In computer architecture, a trace cache or execution trace cache is a specialized instruction cache which stores the dynamic stream of instructions known as trace. It helps in increasing the instruction fetch bandwidth and decreasing power consump ...
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
''Lecture Notes in Computer Science'' is a series of computer science books published by Springer Science+Business Media since 1973.
Overview
The series contains proceedings, post-proceedings, monographs, and Festschrifts. In addition, tutorials, ...
454, Springer, 1990, , pp. 9–29
* {{citation , last1=Sándor , first1=Jozsef , last2=Crstici , first2=Borislav , title=Handbook of number theory II , location=Dordrecht , publisher=Kluwer Academic , year=2004 , isbn=1-4020-2546-7 , pages=32–36 , zbl=1079.11001
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 reprintwith new appendixes
* Antoni Mazurkiewicz, ''Concurrent program schemes and their interpretations'', DAIMI Report PB 78, Aarhus University, 1977
Semigroup theory
Formal languages
Free algebraic structures
Combinatorics
Trace theory