HOME

TheInfoList



OR:

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 curre ...
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.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. 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 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 t ...
, 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 i ...
. Trace monoids are commonly used to model concurrent computation, forming the foundation for process calculi. 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 algebraic definition of the free partially c ...
. 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 \Sigma^* denote the free monoid, that is, the set of all strings written in the alphabet \Sigma. Here, the asterisk denotes, as usual, the Kleene star. An independency relation I on \Sigma then induces a (symmetric) binary relation \sim on \Sigma^*, where u\sim v if and only if there exist x,y\in \Sigma^*, and a pair (a,b)\in I such that u=xaby and v=xbay. Here, u,v,x and y are understood to be strings (elements of \Sigma^*), while a and b are letters (elements of \Sigma). The trace is defined as the reflexive transitive closure of \sim. The trace is thus an equivalence relation on \Sigma^*, and is denoted by \equiv_D, where D is the dependency relation corresponding to I , that is D = (\Sigma \times \Sigma) \setminus I and conversely I = (\Sigma \times \Sigma) \setminus D . Clearly, different dependencies will give different equivalence relations. The transitive closure implies that u\equiv v if and only if there exists a sequence of strings (w_0,w_1,\cdots,w_n) such that u\sim w_0 and v\sim w_n and w_i\sim w_ for all 0\le i < n. The trace is stable under the monoid operation on \Sigma^* (
concatenation In formal language theory and computer programming, string concatenation is the operation of joining character strings end-to-end. For example, the concatenation of "snow" and "ball" is "snowball". In certain formalisations of concatenat ...
) 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 ...
on \Sigma^*. The trace monoid, commonly denoted as \mathbb (D), is defined as the quotient monoid :\mathbb (D) = \Sigma^* / \equiv_D. The homomorphism :\phi_D:\Sigma^*\to \mathbb (D) 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. One will also find the trace monoid denoted as M(\Sigma,I) where I 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 \Sigma=\. A possible dependency relation is :\begin D &=& \\times\ \quad \cup \quad \\times\ \\ &=& \^2 \cup \^2 \\ &=& \ \end The corresponding independency is :I_D=\ Therefore, the letters b,c commute. Thus, for example, a trace equivalence class for the string abababbca would be : bababbcaD = \ The equivalence class bababbcaD is an element of the trace monoid.


Properties

The cancellation property states that equivalence is maintained under right cancellation. That is, if w\equiv v, then (w\div a)\equiv (v\div a). Here, the notation w\div a 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: w \equiv v if and only if xwy\equiv xvy for strings ''x'' and ''y''. Thus, the trace monoid is a syntactic monoid. * Independence: if ua\equiv vb and a\ne b, then ''a'' is independent of ''b''. That is, (a,b)\in I_D. Furthermore, there exists a string ''w'' such that u\equiv wb and v\equiv wa. * Projection rule: equivalence is maintained under string projection, so that if w\equiv v, then \pi_\Sigma(w)\equiv \pi_\Sigma(v). A strong form of Levi's lemma holds for traces. Specifically, if uv\equiv xy for strings ''u'', ''v'', ''x'', ''y'', then there exist strings z_1, z_2, z_3 and z_4 such that (w_2, w_3)\in I_D for all letters w_2\in\Sigma and w_3\in\Sigma such that w_2 occurs in z_2 and w_3 occurs in z_3, and :u\equiv z_1z_2,\qquad v\equiv z_3z_4, :x\equiv z_1z_3,\qquad y\equiv z_2z_4.


Universal property

A dependency morphism (with respect to a dependency ''D'') is a morphism :\psi:\Sigma^*\to M to some monoid ''M'', such that the "usual" trace properties hold, namely: :1. \psi(w)=\psi(\varepsilon) implies that w=\varepsilon :2. (a,b)\in I_D implies that \psi(ab)=\psi(ba) :3. \psi(ua)=\psi(v) implies that \psi(u)=\psi(v\div a) :4. \psi(ua)=\psi(vb) and a\ne b imply that (a,b)\in I_D Dependency morphisms are universal, in the sense that for a given, fixed dependency ''D'', if \psi:\Sigma^*\to M 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 i ...
to the trace monoid \mathbb(D). 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 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 curre ...
who studied the trace monoid for its
combinatoric Combinatorics is an area of mathematics primarily concerned with counting, both as a means and an end in obtaining results, and certain properties of finite structures. It is closely related to many other areas of mathematics and has many app ...
s 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 \Sigma^*, the set of all possible strings, so a trace language is defined as a subset of \mathbb(D) all possible traces. Alternatively, but equivalently, a language L\subseteq\Sigma^* is a trace language, or is said to be consistent with dependency ''D'' if :L = D where : D = \bigcup_ D 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 * {{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 reprint
with 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