Misplaced Pages

Trace monoid: Difference between revisions

Article snapshot taken from Wikipedia with creative commons attribution-sharealike license. Give it a read and then ask your questions in the chat. We can research this topic together.
Browse history interactively← Previous editNext edit →Content deleted Content addedVisualWikitext
Revision as of 20:59, 10 August 2009 editPcap (talk | contribs)Pending changes reviewers, Rollbackers18,285 edits References: Add Diekert's 1990 book, which while a lot shorter focuses on the essentials (despite the unfortunate title)← Previous edit Revision as of 09:21, 4 September 2009 edit undoAboutmovies (talk | contribs)Autopatrolled, Extended confirmed users, IP block exemptions, Pending changes reviewers, Rollbackers412,301 editsm References: link publisherNext edit →
Line 88: Line 88:


==References== ==References==
* Volker Diekert, Yves Métivier, "", In G. Rozenberg and A. Salomaa, editors, ''Handbook of Formal Languages'', Vol. '''3''', Beyond Words, pages 457--534. Springer-Verlag, Berlin, 1997. * Volker Diekert, Yves Métivier, "", In G. Rozenberg and A. Salomaa, editors, ''Handbook of Formal Languages'', Vol. '''3''', ], pages 457--534. Springer-Verlag, Berlin, 1997.
* Antoni Mazurkiewicz, "Introduction to Trace Theory", pp 3-41, in ''The Book of Traces'', V. Diekert, G. Rozenberg, eds. (1995) World Scientific, Singapore ISBN 9810220588 * Antoni Mazurkiewicz, "Introduction to Trace Theory", pp 3-41, in ''The Book of Traces'', V. Diekert, G. Rozenberg, eds. (1995) World Scientific, Singapore ISBN 9810220588
* Volker Diekert, ''Combinatorics on traces'', ] 454, Springer, 1990, ISBN 3540530312, pp. 9-29 * Volker Diekert, ''Combinatorics on traces'', ] 454, Springer, 1990, ISBN 3540530312, pp. 9-29

Revision as of 09:21, 4 September 2009

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.

Trace

Let Σ {\displaystyle \Sigma ^{*}} denote the free monoid, that is, the set of all strings written in the alphabet Σ {\displaystyle \Sigma } . Here, the asterisk denotes, as usual, the Kleene star. An independency relation I {\displaystyle I} then induces a binary relation {\displaystyle \sim } on Σ {\displaystyle \Sigma ^{*}} , where u v {\displaystyle u\sim v\,} if and only if there exist x , y Σ {\displaystyle x,y\in \Sigma ^{*}} , and a pair ( a , b ) I {\displaystyle (a,b)\in I} such that u = x a b y {\displaystyle u=xaby} and v = x b a y {\displaystyle v=xbay} . Here, u , v , x {\displaystyle u,v,x} and y {\displaystyle y} are understood to be strings (elements of Σ {\displaystyle \Sigma ^{*}} ), while a {\displaystyle a} and b {\displaystyle b} are letters (elements of Σ {\displaystyle \Sigma } ).

The trace is defined as the symmetric, reflexive and transitive closure of {\displaystyle \sim } . The trace is thus an equivalence relation on Σ {\displaystyle \Sigma ^{*}} , and is denoted by D {\displaystyle \equiv _{D}} . 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 u v {\displaystyle u\equiv v} if and only if there exists a sequence of strings ( w 0 , w 1 , , w n ) {\displaystyle (w_{0},w_{1},\cdots ,w_{n})} such that u w 0 {\displaystyle u\sim w_{0}\,} and v w n {\displaystyle v\sim w_{n}\,} and w i w i + 1 {\displaystyle w_{i}\sim w_{i+1}\,} for all 0 i < n {\displaystyle 0\leq i<n} .

Trace monoid

The trace monoid, commonly denoted as M ( D ) {\displaystyle \mathbb {M} (D)} , is defined as the quotient monoid

M ( D ) = Σ / D . {\displaystyle \mathbb {M} (D)=\Sigma ^{*}/\equiv _{D}.}

The homomorphism

ϕ D : Σ M ( D ) {\displaystyle \phi _{D}:\Sigma ^{*}\to \mathbb {M} (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.

Examples

Consider the alphabet Σ = { a , b , c } {\displaystyle \Sigma =\{a,b,c\}} . A possible dependency relation is

D = { a , b } × { a , b } { a , c } × { a , c } = { a , b } 2 { a , c } 2 = { ( a , b ) , ( b , a ) , ( a , c ) , ( c , a ) , ( a , a ) , ( b , b ) , ( c , c ) } {\displaystyle {\begin{matrix}D&=&\{a,b\}\times \{a,b\}\quad \cup \quad \{a,c\}\times \{a,c\}\\&=&\{a,b\}^{2}\cup \{a,c\}^{2}\\&=&\{(a,b),(b,a),(a,c),(c,a),(a,a),(b,b),(c,c)\}\end{matrix}}}

The corresponding independency is

I D = { ( b , c ) , ( c , b ) } {\displaystyle I_{D}=\{(b,c)\,,\,(c,b)\}}

Therefore, the letters b , c {\displaystyle b,c} commute. Thus, for example, a trace equivalence class for the string a b a b a b b c a {\displaystyle abababbca} would be

[ a b a b a b b c a ] D = { a b a b a b b c a , a b a b a b c b a , a b a b a c b b a } {\displaystyle _{D}=\{abababbca\,,\;abababcba\,,\;ababacbba\}}

The equivalence class [ a b a b a b b c a ] D {\displaystyle _{D}} is an element of the trace monoid.

Properties

The cancellation property states that equivalence is maintained under right cancellation. That is, if w v {\displaystyle w\equiv v} , then ( w ÷ a ) ( v ÷ a ) {\displaystyle (w\div a)\equiv (v\div a)} . Here, the notation w ÷ a {\displaystyle 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 v {\displaystyle w\equiv v} if and only if x w y x v y {\displaystyle xwy\equiv xvy} for strings x and y. Thus, the trace monoid is a syntactic monoid.
  • Independence: if u a v b {\displaystyle ua\equiv vb} and a b {\displaystyle a\neq b} , then a is independent of b. That is, ( a , b ) I D {\displaystyle (a,b)\in I_{D}} . Furthermore, there exists a string w such that u = w b {\displaystyle u=wb} and v = w a {\displaystyle v=wa} .
  • Projection rule: equivalence is maintained under string projection, so that if w v {\displaystyle w\equiv v} , then π Σ ( w ) π Σ ( v ) {\displaystyle \pi _{\Sigma }(w)\equiv \pi _{\Sigma }(v)} .

A strong form of Levi's lemma holds for traces. Specifically, if u v x y {\displaystyle uv\equiv xy} for strings u, v, x, y, then there exist strings z 1 , z 2 , z 3 {\displaystyle z_{1},z_{2},z_{3}} and z 4 {\displaystyle z_{4}} such that ( z 2 , z 3 ) I D {\displaystyle (z_{2},z_{3})\in I_{D}} , and

u z 1 z 2 v = z 3 z 4 {\displaystyle u\equiv z_{1}z_{2}\qquad v=z_{3}z_{4}}
x z 1 z 3 y = z 2 z 4 {\displaystyle x\equiv z_{1}z_{3}\qquad y=z_{2}z_{4}}

Universal property

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

ψ : Σ M {\displaystyle \psi :\Sigma ^{*}\to M\,}

to some monoid M, such that the "usual" trace properties hold, namely:

1. ψ ( w ) = ψ ( ε ) {\displaystyle \psi (w)=\psi (\varepsilon )} implies that w = ε {\displaystyle w=\varepsilon }
2. ( a , b ) I D {\displaystyle (a,b)\in I_{D}} implies that ψ ( a b ) = ψ ( b a ) {\displaystyle \psi (ab)=\psi (ba)\,}
3. ψ ( u a ) = ψ ( v ) {\displaystyle \psi (ua)=\psi (v)\,} implies that ψ ( u ) = ψ ( v ÷ a ) {\displaystyle \psi (u)=\psi (v\div a)}
4. ψ ( u a ) = ψ ( v b ) {\displaystyle \psi (ua)=\psi (vb)\,} and a b {\displaystyle a\neq b} imply that ( a , b ) I D {\displaystyle (a,b)\in I_{D}}

Dependency morphisms are universal, in the sense that for a given, fixed dependency D, if ψ : Σ M {\displaystyle \psi :\Sigma ^{*}\to M\,} is a dependency morphism to a monoid M, then M is isomorphic to the trace monoid M ( D ) {\displaystyle \mathbb {M} (D)} . In particular, the natural homomorphism is a dependency morphism.

Trace languages

Just as a formal language can be regarded as a subset of Σ {\displaystyle \Sigma ^{*}} the set of all possible strings, so then a trace language is defined as subset of M ( D ) {\displaystyle \mathbb {M} (D)} all possible traces.

A language L Σ {\displaystyle L\subset \Sigma ^{*}} is a trace language, or is said to be consistent with dependency D if

L = [ L ] D {\displaystyle L=\bigcup _{D}}

where

[ L ] D = { [ w ] D | w L } {\displaystyle _{D}=\{_{D}\vert w\in L\}}

is the trace closure of a set of strings, and

T = { w | [ w ] D T } {\displaystyle \bigcup T=\{w\vert _{D}\in T\}}

is the set of strings in a set of traces.

References

  • Volker Diekert, Yves Métivier, "Partial Commutation and Traces", In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Languages, Vol. 3, Beyond Words, pages 457--534. Springer-Verlag, Berlin, 1997.
  • Antoni Mazurkiewicz, "Introduction to Trace Theory", pp 3-41, in The Book of Traces, V. Diekert, G. Rozenberg, eds. (1995) World Scientific, Singapore ISBN 9810220588
  • Volker Diekert, Combinatorics on traces, LNCS 454, Springer, 1990, ISBN 3540530312, pp. 9-29
Categories: