Revision as of 11:44, 20 March 2015 editSuslindisambiguator (talk | contribs)Extended confirmed users63,348 edits →Normal forms← Previous edit | Latest revision as of 01:57, 19 September 2024 edit undoRowanElder (talk | contribs)Extended confirmed users1,534 edits →Trace: General copyedit and clarification, esp. tone, punctuation, pronoun referents, and explicit definitions. Might still be errors and there are certainly still some unclarities.Tag: Visual edit | ||
(28 intermediate revisions by 22 users not shown) | |||
Line 1: | Line 1: | ||
{{Short description|Generalization of strings in computer science}} | |||
⚫ | |||
In ], a '''trace''' is an ] of ]s, wherein certain letters in the string are allowed to ], 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 ] 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 ] of traces. | |||
⚫ | Traces were introduced by ] and ] in 1969 to give a combinatorial proof of ]. Traces are used in theories of ], where commuting letters stand for portions of a job that can execute independently of one another, while non-commuting letters stand for locks, ]s or ]s.<ref name="CS161">Sándor & Crstici (2004) p.161</ref> | ||
⚫ | The |
||
⚫ | The trace monoid is constructed from the ] (the set of all strings of finite length) as follows. First, sets of commuting letters are given by an ]. 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 ] now called the ''trace monoid''. The trace monoid is ], in that all dependency-homomorphic (see below) monoids are in fact ]. | ||
⚫ | Trace monoids are commonly used to model ], forming the foundation for ]. 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 |
||
⚫ | Trace monoids are commonly used to model ], forming the foundation for ]. They are the object of study in ]. The utility of trace monoids comes from the fact that they are isomorphic to the monoid of ]s; thus allowing algebraic techniques to be applied to ]s, and vice versa. They are also isomorphic to ]s, which model the history of computation of individual processes in the context of all scheduled processes on one or more computers. | ||
==Trace== | ==Trace== | ||
Let <math>\Sigma^*</math> denote the free monoid, that is, the set of all strings written in the alphabet <math>\Sigma</math>. |
Let <math>\Sigma^*</math> denote the free monoid on a set of generators <math>\Sigma</math>, that is, the set of all strings written in the alphabet <math>\Sigma</math>. The asterisk is a standard notation for the ]. An ] <math>I</math> on the alphabet <math>\Sigma</math> then induces a symmetric binary relation <math>\sim</math> on the set of strings <math>\Sigma^*</math>: two strings <math>u,v</math> are related, <math>u\sim v,</math> if and only if there exist <math>x,y\in \Sigma^*</math>, and a pair <math>(a,b)\in I</math> such that <math>u=xaby</math> and <math>v=xbay</math>. Here, <math>u,v,x</math> and <math>y</math> are understood to be strings (elements of <math>\Sigma^*</math>), while <math>a</math> and <math>b</math> are letters (elements of <math>\Sigma</math>). | ||
The '''trace''' is defined as the |
The '''trace''' is defined as the ] of <math>\sim</math>. The trace is thus an ] on <math>\Sigma^*</math> and is denoted by <math>\equiv_D</math>, where <math>D</math> is the dependency relation corresponding to <math>I .</math> <math>D = (\Sigma \times \Sigma) \setminus I</math> and <math>I = (\Sigma \times \Sigma) \setminus D .</math> Different independencies or dependencies will give different equivalence relations. | ||
The ] |
The ] implies that <math>u\equiv_D v</math> if and only if there exists a sequence of strings <math>(w_0,w_1,\cdots,w_n)</math> such that <math>u\sim w_0,</math> <math>v\sim w_n,</math> and <math>w_i\sim w_{i+1}</math> for all <math>0\le i < n</math>. The trace is stable under the monoid operation on <math>\Sigma^*</math>, i.e., ], and <math>\equiv_D</math> is therefore a ] on <math>\Sigma^*.</math> | ||
⚫ | ==Trace |
||
The trace monoid, commonly denoted as <math>\mathbb {M}(D)</math>, is defined as the quotient monoid | The trace monoid, commonly denoted as <math>\mathbb {M}(D)</math>, is defined as the quotient monoid | ||
Line 21: | Line 23: | ||
is commonly referred to as the ] 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. | is commonly referred to as the ] 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 <math>M(\Sigma,I)</math> where <math>I</math> is the independency relation. One can also find the commutation relation used instead of the independency relation; it differs from the independency relation by also including all the diagonal elements of <math display="inline">\Sigma \times \Sigma</math> since letters "commute with themselves" in a free monoid of strings of those letters. | |||
==Examples== | ==Examples== | ||
Consider the alphabet <math>\Sigma=\{a,b,c\}</math>. A possible dependency relation is |
Consider the alphabet <math>\Sigma=\{a,b,c\}</math>. A possible dependency relation is | ||
:<math>\begin{matrix} D | :<math>\begin{matrix} D | ||
&=& \{a,b\}\times\{a,b\} \quad \cup \quad \{a,c\}\times\{a,c\} \\ | &=& \{a,b\}\times\{a,b\} \quad \cup \quad \{a,c\}\times\{a,c\} \\ | ||
&=& \{a,b\}^2 \cup \{a,c\}^2 \\ | &=& \{a,b\}^2 \cup \{a,c\}^2 \\ | ||
&=& \{ (a,b),(b,a),(a,c),(c,a),(a,a),(b,b),(c,c)\} |
&=& \{ (a,b),(b,a),(a,c),(c,a),(a,a),(b,b),(c,c)\}. | ||
\end{matrix}</math> | \end{matrix}</math> | ||
The corresponding independency is |
The corresponding independency is | ||
:<math>I_D=\{(b,c)\,,\,(c,b)\}</math> | :<math>I_D=\{(b,c)\,,\,(c,b)\}.</math> | ||
Therefore, the letters <math>b,c</math> commute. Thus, for example, a trace equivalence class for the string <math>abababbca</math> would be | Therefore, the letters <math>b,c</math> commute. Thus, for example, a trace equivalence class for the string <math>abababbca</math> would be | ||
Line 39: | Line 43: | ||
:<math>_D = \{abababbca\,,\; abababcba\,,\; ababacbba \}</math> | :<math>_D = \{abababbca\,,\; abababcba\,,\; ababacbba \}</math> | ||
and the equivalence class <math>_D</math> would be an element of the trace monoid. | |||
==Properties== | ==Properties== | ||
The '''cancellation property''' states that equivalence is maintained under ]. That is, if <math>w\equiv v</math>, then <math>(w\div a)\equiv (v\div a)</math>. Here, the notation <math>w\div a</math> 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: | The '''cancellation property''' states that equivalence is maintained under ]. That is, if <math>w\equiv v</math>, then <math>(w\div a)\equiv (v\div a)</math>. Here, the notation <math>w\div a</math> 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: <math>w \equiv v</math> if and only if <math>xwy\equiv xvy</math> for strings ''x'' and ''y''. Thus, the trace monoid is a syntactic monoid. | * Embedding: <math>w \equiv v</math> if and only if <math>xwy\equiv xvy</math> for strings ''x'' and ''y''. Thus, the trace monoid is a syntactic monoid.{{Non-sequitur|post-text=See ]|date=April 2022}} | ||
⚫ | * Independence: if <math>ua\equiv vb</math> and <math>a\ne b</math>, then ''a'' is independent of ''b''. That is, <math>(a,b)\in I_D</math>. Furthermore, there exists a string ''w'' such that <math>u\equiv wb</math> and <math>v\equiv wa</math>. | ||
⚫ | * Projection rule: equivalence is maintained under ], so that if <math>w\equiv v</math>, then <math>\pi_\Sigma(w)\equiv \pi_\Sigma(v)</math>. | ||
⚫ | * Independence: if <math>ua\equiv vb</math> and <math>a\ne b</math>, then ''a'' is independent of ''b''. That is, <math>(a,b)\in I_D</math>. Furthermore, there exists a string ''w'' such that <math>u |
||
⚫ | * Projection rule: equivalence is maintained under ], so that if <math>w\equiv v</math>, then <math>\pi_\Sigma(w)\equiv \pi_\Sigma(v)</math>. | ||
A strong form of ] holds for traces. Specifically, if <math>uv\equiv xy</math> for strings ''u'', ''v'', ''x'', ''y'', then there exist strings <math>z_1, z_2, z_3</math> and <math>z_4</math> such that <math>(w_2, w_3)\in I_D</math> | A strong form of ] holds for traces. Specifically, if <math>uv\equiv xy</math> for strings ''u'', ''v'', ''x'', ''y'', then there exist strings <math>z_1, z_2, z_3</math> and <math>z_4</math> such that <math>(w_2, w_3)\in I_D</math> | ||
Line 58: | Line 60: | ||
==Universal property== | ==Universal property== | ||
A '''dependency morphism''' (with respect to a dependency ''D'') is a morphism | A '''dependency morphism''' (with respect to a dependency ''D'') is a morphism | ||
:<math>\psi:\Sigma^*\to M |
:<math>\psi:\Sigma^*\to M</math> | ||
to some monoid ''M'', such that the "usual" trace properties hold, namely: | to some monoid ''M'', such that the "usual" trace properties hold, namely: | ||
:1. <math>\psi(w)=\psi(\varepsilon)</math> implies that <math>w=\varepsilon</math> | :1. <math>\psi(w)=\psi(\varepsilon)</math> implies that <math>w=\varepsilon</math> | ||
:2. <math>(a,b)\in I_D</math> implies that <math>\psi(ab)=\psi(ba) |
:2. <math>(a,b)\in I_D</math> implies that <math>\psi(ab)=\psi(ba)</math> | ||
:3. <math>\psi(ua)=\psi(v) |
:3. <math>\psi(ua)=\psi(v)</math> implies that <math>\psi(u)=\psi(v\div a)</math> | ||
:4. <math>\psi(ua)=\psi(vb) |
:4. <math>\psi(ua)=\psi(vb)</math> and <math>a\ne b</math> imply that <math>(a,b)\in I_D</math> | ||
Dependency morphisms are universal, in the sense that for a given, fixed dependency ''D'', if <math>\psi:\Sigma^*\to M |
Dependency morphisms are universal, in the sense that for a given, fixed dependency ''D'', if <math>\psi:\Sigma^*\to M</math> is a dependency morphism to a monoid ''M'', then ''M'' is ] to the trace monoid <math>\mathbb{M}(D)</math>. In particular, the natural homomorphism is a dependency morphism. | ||
==Normal forms== | ==Normal forms== | ||
{{Expand section|date=December 2009}} | {{Expand section|date=December 2009}} | ||
There are two well-known normal forms for words in trace monoids. One is the '']'' normal form, due to Anatolij V. Anisimov and Donald Knuth, and the other is the ''Foata'' normal form due to ] and ] who studied the trace monoid for its |
There are two well-known normal forms for words in trace monoids. One is the '']'' normal form, due to Anatolij V. Anisimov and ], and the other is the ''Foata'' normal form due to ] and ] who studied the trace monoid for its ]s in the 1960s.<ref>Section 2.3, Diekert and Métivier 1997.</ref> | ||
Unicode's ] (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 <math>\Sigma^*</math> the set of all possible strings, so |
||
⚫ | ==Trace languages== | ||
⚫ | |||
⚫ | Just as a formal language can be regarded as a subset of <math>\Sigma^*</math>, the set of all possible strings, so a trace language is defined as a subset of <math>\mathbb{M}(D)</math> all possible traces. | ||
⚫ | Alternatively, but equivalently, a language <math>L\subseteq\Sigma^*</math> is a trace language, or is said to be '''consistent''' with dependency ''D'' if | ||
⚫ | :<math>L= |
||
⚫ | :<math>L = _D</math> | ||
⚫ | where |
||
⚫ | where | ||
⚫ | :<math>_D=\{ |
||
⚫ | :<math>_D = \bigcup_{w \in L} _D</math> | ||
⚫ | is the trace closure of a set of strings |
||
⚫ | is the trace closure of a set of strings. | ||
:<math>\bigcup T = \{w \vert _D\in T \}</math> | |||
==See also== | |||
is the set of strings in a set of traces. | |||
* ] | |||
==Notes== | ==Notes== | ||
Line 98: | Line 101: | ||
==References== | ==References== | ||
'''General references''' | '''General references''' | ||
*{{Citation | editor-first=G. | editor-last=Rozenberg | editor2-first=A. | editor2-last=Salomaa | last = Diekert | first = Volker | last2 = Métivier | first2 = Yves | title = Handbook of Formal Languages Vol. 3; Beyond Words | publisher = Springer-Verlag, Berlin | year = 1997 | chapter=Partial Commutation and Traces | |
*{{Citation | editor-first=G. | editor-last=Rozenberg | editor2-first=A. | editor2-last=Salomaa | last = Diekert | first = Volker | last2 = Métivier | first2 = Yves | title = Handbook of Formal Languages Vol. 3; Beyond Words | publisher = Springer-Verlag, Berlin | year = 1997 | chapter=Partial Commutation and Traces | chapter-url= http://citeseer.ist.psu.edu/diekert97partial.html | pages = 457–534 | isbn = 3-540-60649-1}} | ||
* {{citation | last=Lothaire | first=M. | |
* {{citation | last=Lothaire | first=M. | author-link=M. Lothaire | title=Algebraic combinatorics on words | others=With preface by Jean Berstel and Dominique Perrin | edition=Reprint of the 2002 hardback | series=Encyclopedia of Mathematics and Its Applications | volume=90| publisher=Cambridge University Press | year=2011 | isbn=978-0-521-18071-9 | zbl=1221.68183 }} | ||
* Antoni Mazurkiewicz, "Introduction to Trace Theory", pp 3–41, in ''The Book of Traces'', V. Diekert, G. Rozenberg, eds. (1995) World Scientific, Singapore |
* Antoni Mazurkiewicz, "Introduction to Trace Theory", pp 3–41, in ''The Book of Traces'', V. Diekert, G. Rozenberg, eds. (1995) World Scientific, Singapore {{isbn|981-02-2058-8}} | ||
* Volker Diekert, ''Combinatorics on traces'', ] 454, Springer, 1990, |
* Volker Diekert, ''Combinatorics on traces'', ] 454, Springer, 1990, {{isbn|3-540-53031-2}}, 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 }} | * {{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''' | '''Seminal publications''' | ||
Line 111: | Line 114: | ||
] | ] | ||
] | ] | ||
] |
Latest revision as of 01:57, 19 September 2024
Generalization of strings in computer scienceIn 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. 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 points or thread joins.
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 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 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. An independency relation on the alphabet then induces a symmetric binary relation on the set of strings : two strings are related, 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 and Different independencies or dependencies will give different equivalence relations.
The transitive closure implies that if and only if there exists a sequence of strings such that and for all . The trace is stable under the monoid operation on , i.e., concatenation, and is therefore a congruence relation on
The trace monoid, commonly denoted as , 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.
One will also find the trace monoid denoted as where is the independency relation. One can also find the commutation relation used instead of the independency relation; it differs from the independency relation by also including all the diagonal elements of since letters "commute with themselves" in a free monoid of strings of those letters.
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
and the equivalence class would be 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, so that if , then .
A strong form of Levi's lemma 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 to the trace monoid . In particular, the natural homomorphism is a dependency morphism.
Normal forms
This section needs expansion. You can help by adding to it. (December 2009) |
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
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
Notes
- Sándor & Crstici (2004) p.161
- Proposition 2.2, Diekert and Métivier 1997.
- Section 2.3, Diekert and Métivier 1997.
References
General references
- Diekert, Volker; Métivier, Yves (1997), "Partial Commutation and Traces", in Rozenberg, G.; Salomaa, A. (eds.), Handbook of Formal Languages Vol. 3; Beyond Words, Springer-Verlag, Berlin, pp. 457–534, ISBN 3-540-60649-1
- Lothaire, M. (2011), Algebraic combinatorics on words, Encyclopedia of Mathematics and Its Applications, vol. 90, With preface by Jean Berstel and Dominique Perrin (Reprint of the 2002 hardback ed.), Cambridge University Press, ISBN 978-0-521-18071-9, Zbl 1221.68183
- Antoni Mazurkiewicz, "Introduction to Trace Theory", pp 3–41, in The Book of Traces, V. Diekert, G. Rozenberg, eds. (1995) World Scientific, Singapore ISBN 981-02-2058-8
- Volker Diekert, Combinatorics on traces, LNCS 454, Springer, 1990, ISBN 3-540-53031-2, pp. 9–29
- Sándor, Jozsef; Crstici, Borislav (2004), Handbook of number theory II, Dordrecht: Kluwer Academic, pp. 32–36, ISBN 1-4020-2546-7, 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