Trace monoid

Trace monoid

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 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 then induces a binary relation sim on Sigma^*, where usim v, if and only if there exist x,yin 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 symmetric, reflexive and transitive closure of sim. The trace is thus an equivalence relation on Sigma^*, and is denoted by 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 uequiv v if and only if there exists a sequence of strings (w_0,w_1,cdots,w_n) such that usim w_0, and vsim w_n, and w_isim w_{i+1}, for all 0le i < n.

Trace monoid

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

:mathbb {M}(D) = Sigma^* / equiv_D.

The homomorphism :phi_D:Sigma^* o 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 Sigma={a,b,c}. A possible dependency relation is

:egin{matrix} D &=& {a,b} imes{a,b} quad cup quad {a,c} imes{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)}

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

: [abababbca] _D = {abababbca,,; abababcba,,; ababacbba }

The equivalence class [abababbca] _D is an element of the trace monoid.

Properties

The cancellation property states that equivalence is maintained under right cancellation. That is, if wequiv v, then (wdiv a)equiv (vdiv a). Here, the notation wdiv 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 xwyequiv xvy for strings "x" and "y". Thus, the trace monoid is a syntactic monoid.

* Independence: if uaequiv vb and a e b, then "a" is independent of "b". That is, (a,b)in I_D. Furthermore, there exists a string "w" such that u=wb and v=wa.

* Projection rule: equivalence is maintained under string projection, so that if wequiv v, then pi_Sigma(w)equiv pi_Sigma(v).

A strong form of the Levi lemma holds for traces. Specifically, if uvequiv xy for strings "u", "v", "x", "y", then there exist strings z_1, z_2, z_3 and z_4 such that (z_2,z_3)in I_D, and

:uequiv z_1z_2qquad v=z_3z_4:xequiv z_1z_3qquad y=z_2z_4

Universal property

A dependency morphism (with respect to a dependency "D") is a morphism:psi:Sigma^* o 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(vdiv a)

:4. psi(ua)=psi(vb), and a e 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^* o M, is a dependency morphism to a monoid "M", then "M" is isomorphic to the trace monoid 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 Sigma^* the set of all possible strings, so then a trace language is defined as subset of mathbb{M}(D) all possible traces.

A language LsubsetSigma^* is a trace language, or is said to be consistent with dependency "D" if

:L=igcup [L] _D

where

: [L] _D={ [w] _D vert win L }

is the trace closure of a set of strings, and

:igcup T = {w vert [w] _Din T }

is the set of strings in a set of traces.

References

* 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, Yves Métivier, " [http://citeseer.ist.psu.edu/diekert97partial.html 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.


Wikimedia Foundation. 2010.

Игры ⚽ Поможем решить контрольную работу

Look at other dictionaries:

  • Trace — may refer to:;Mathematics, computing and electronics: * Trace (linear algebra) of a square matrix or a linear transformation * Trace class, a certain set of operators in a Hilbert space * Trace operator, a restriction to boundary operator in a… …   Wikipedia

  • Monoid — This article is about the mathematical concept. For the alien creatures in the Doctor Who adventure, see The Ark (Doctor Who). Coherence law for monoid unit In abstract algebra, a branch of mathematics, a monoid is an algebraic structure with a… …   Wikipedia

  • 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 underpining is provided by an algebraic definition of the free partially… …   Wikipedia

  • 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… …   Wikipedia

  • Syntactic monoid — In mathematics, the syntactic monoid M ( L ) of a formal language L is the smallest monoid that recognizes the language L .yntactic quotientGiven Ssubset M a subset of a monoid M , one may define sets that consist of formal left or right inverses …   Wikipedia

  • Communicating sequential processes — In computer science, Communicating Sequential Processes (CSP) is a formal language for describing patterns of interaction in concurrent systems.[1] It is a member of the family of mathematical theories of concurrency known as process algebras, or …   Wikipedia

  • List of mathematics articles (T) — NOTOC T T duality T group T group (mathematics) T integration T norm T norm fuzzy logics T schema T square (fractal) T symmetry T table T theory T.C. Mits T1 space Table of bases Table of Clebsch Gordan coefficients Table of divisors Table of Lie …   Wikipedia

  • Théorème de Kleene —  Ne doit pas être confondu avec Théorème de récursion de Kleene ni Théorème du point fixe de Kleene. En informatique théorique, et plus précisément en théorie des automates, le théorème de Kleene affirme qu un langage peut être décrit par… …   Wikipédia en Français

  • Process calculus — In computer science, the process calculi (or process algebras) are a diverse family of related approaches to formally modelling concurrent systems. Process calculi provide a tool for the high level description of interactions, communications, and …   Wikipedia

  • Representation theory — This article is about the theory of representations of algebraic structures by linear transformations and matrices. For the more general notion of representations throughout mathematics, see representation (mathematics). Representation theory is… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”