fbpx
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 provides a set of synchronization primitives (such as locks, mutexes or thread joins) for providing rendezvous points between a set of independently executing processes or threads.

History monoids occur in the theory of concurrent computation, and provide a low-level mathematical foundation for process calculi, such as CSP the language of communicating sequential processes, or CCS, the calculus of communicating systems. History monoids were first presented by M.W. Shields.[1]

History monoids are isomorphic to trace monoids (free partially commutative monoids) and to the monoid of dependency graphs. As such, they are free objects and are universal. The history monoid is a type of semi-abelian categorical product in the category of monoids.

Product monoids and projection edit

Let

 

denote an n-tuple of (not necessarily pairwise disjoint) alphabets  . Let   denote all possible combinations of one finite-length string from each alphabet:

 

(In more formal language,   is the Cartesian product of the free monoids of the  . The superscript star is the Kleene star.) Composition in the product monoid is component-wise, so that, for

 

and

 

then

 

for all   in  . Define the union alphabet to be

 

(The union here is the set union, not the disjoint union.) Given any string  , we can pick out just the letters in some   using the corresponding string projection  . A distribution   is the mapping that operates on   with all of the  , separating it into components in each free monoid:

 

Histories edit

For every  , the tuple   is called the elementary history of a. It serves as an indicator function for the inclusion of a letter a in an alphabet  . That is,

 

where

 

Here,   denotes the empty string. The history monoid   is the submonoid of the product monoid   generated by the elementary histories:   (where the superscript star is the Kleene star applied with a component-wise definition of composition as given above). The elements of   are called global histories, and the projections of a global history are called individual histories.

Connection to computer science edit

The use of the word history in this context, and the connection to concurrent computing, can be understood as follows. An individual history is a record of the sequence of states of a process (or thread or machine); the alphabet   is the set of states of the process.

A letter that occurs in two or more alphabets serves as a synchronization primitive between the various individual histories. That is, if such a letter occurs in one individual history, it must also occur in another history, and serves to "tie" or "rendezvous" them together.

Consider, for example,   and  . The union alphabet is of course  . The elementary histories are  ,  ,  ,   and  . In this example, an individual history of the first process might be   while the individual history of the second machine might be  . Both of these individual histories are represented by the global history  , since the projection of this string onto the individual alphabets yields the individual histories. In the global history, the letters   and   can be considered to commute with the letters   and  , in that these can be rearranged without changing the individual histories. Such commutation is simply a statement that the first and second processes are running concurrently, and are unordered with respect to each other; they have not (yet) exchanged any messages or performed any synchronization.

The letter   serves as a synchronization primitive, as its occurrence marks a spot in both the global and individual histories, that cannot be commuted across. Thus, while the letters   and   can be re-ordered past   and  , they cannot be reordered past  . Thus, the global history   and the global history   both have as individual histories   and  , indicating that the execution of   may happen before or after  . However, the letter   is synchronizing, so that   is guaranteed to happen after  , even though   is in a different process than  .

Properties edit

A history monoid is isomorphic to a trace monoid, and as such, is a type of semi-abelian categorical product in the category of monoids. In particular, the history monoid   is isomorphic to the trace monoid   with the dependency relation given by

 

In simple terms, this is just the formal statement of the informal discussion given above: the letters in an alphabet   can be commutatively re-ordered past the letters in an alphabet  , unless they are letters that occur in both alphabets. Thus, traces are exactly global histories, and vice versa.

Conversely, given any trace monoid  , one can construct an isomorphic history monoid by taking a sequence of alphabets   where   ranges over all pairs in  .

Notes edit

  1. ^ M.W. Shields "Concurrent Machines", Computer Journal, (1985) 28 pp. 449–465.

References edit

  • 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, 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.

history, monoid, mathematics, computer, science, history, monoid, representing, histories, concurrently, running, computer, processes, collection, strings, each, string, representing, individual, history, process, history, monoid, provides, synchronization, pr. 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 provides a set of synchronization primitives such as locks mutexes or thread joins for providing rendezvous points between a set of independently executing processes or threads History monoids occur in the theory of concurrent computation and provide a low level mathematical foundation for process calculi such as CSP the language of communicating sequential processes or CCS the calculus of communicating systems History monoids were first presented by M W Shields 1 History monoids are isomorphic to trace monoids free partially commutative monoids and to the monoid of dependency graphs As such they are free objects and are universal The history monoid is a type of semi abelian categorical product in the category of monoids Contents 1 Product monoids and projection 2 Histories 3 Connection to computer science 4 Properties 5 Notes 6 ReferencesProduct monoids and projection editLet A S 1 S 2 S n displaystyle A Sigma 1 Sigma 2 ldots Sigma n nbsp denote an n tuple of not necessarily pairwise disjoint alphabets S k displaystyle Sigma k nbsp Let P A displaystyle P A nbsp denote all possible combinations of one finite length string from each alphabet P A S 1 S 2 S n displaystyle P A Sigma 1 times Sigma 2 times cdots times Sigma n nbsp In more formal language P A displaystyle P A nbsp is the Cartesian product of the free monoids of the S k displaystyle Sigma k nbsp The superscript star is the Kleene star Composition in the product monoid is component wise so that for u u 1 u 2 u n displaystyle mathbf u u 1 u 2 ldots u n nbsp and v v 1 v 2 v n displaystyle mathbf v v 1 v 2 ldots v n nbsp then u v u 1 v 1 u 2 v 2 u n v n displaystyle mathbf uv u 1 v 1 u 2 v 2 ldots u n v n nbsp for all u v displaystyle mathbf u mathbf v nbsp in P A displaystyle P A nbsp Define the union alphabet to be S S 1 S 2 S n displaystyle Sigma Sigma 1 cup Sigma 2 cup cdots cup Sigma n nbsp The union here is the set union not the disjoint union Given any string w S displaystyle w in Sigma nbsp we can pick out just the letters in some S k displaystyle Sigma k nbsp using the corresponding string projection p k S S k displaystyle pi k Sigma to Sigma k nbsp A distribution p S P A displaystyle pi Sigma to P A nbsp is the mapping that operates on w S displaystyle w in Sigma nbsp with all of the p k displaystyle pi k nbsp separating it into components in each free monoid p w p 1 w p 2 w p n w displaystyle pi w mapsto pi 1 w pi 2 w ldots pi n w nbsp Histories editFor every a S displaystyle a in Sigma nbsp the tuple p a displaystyle pi a nbsp is called the elementary history of a It serves as an indicator function for the inclusion of a letter a in an alphabet S k displaystyle Sigma k nbsp That is p a a 1 a 2 a n displaystyle pi a a 1 a 2 ldots a n nbsp where a k a if a S k e otherwise displaystyle a k begin cases a mbox if a in Sigma k varepsilon mbox otherwise end cases nbsp Here e displaystyle varepsilon nbsp denotes the empty string The history monoid H A displaystyle H A nbsp is the submonoid of the product monoid P A displaystyle P A nbsp generated by the elementary histories H A p a a S displaystyle H A pi a a in Sigma nbsp where the superscript star is the Kleene star applied with a component wise definition of composition as given above The elements of H A displaystyle H A nbsp are called global histories and the projections of a global history are called individual histories Connection to computer science editThe use of the word history in this context and the connection to concurrent computing can be understood as follows An individual history is a record of the sequence of states of a process or thread or machine the alphabet S k displaystyle Sigma k nbsp is the set of states of the process A letter that occurs in two or more alphabets serves as a synchronization primitive between the various individual histories That is if such a letter occurs in one individual history it must also occur in another history and serves to tie or rendezvous them together Consider for example S 1 a b c displaystyle Sigma 1 a b c nbsp and S 2 a d e displaystyle Sigma 2 a d e nbsp The union alphabet is of course S a b c d e displaystyle Sigma a b c d e nbsp The elementary histories are a a displaystyle a a nbsp b e displaystyle b varepsilon nbsp c e displaystyle c varepsilon nbsp e d displaystyle varepsilon d nbsp and e e displaystyle varepsilon e nbsp In this example an individual history of the first process might be b c b c c displaystyle bcbcc nbsp while the individual history of the second machine might be d d d e d displaystyle ddded nbsp Both of these individual histories are represented by the global history b c b d d d c c e d displaystyle bcbdddcced nbsp since the projection of this string onto the individual alphabets yields the individual histories In the global history the letters b displaystyle b nbsp and c displaystyle c nbsp can be considered to commute with the letters d displaystyle d nbsp and e displaystyle e nbsp in that these can be rearranged without changing the individual histories Such commutation is simply a statement that the first and second processes are running concurrently and are unordered with respect to each other they have not yet exchanged any messages or performed any synchronization The letter a displaystyle a nbsp serves as a synchronization primitive as its occurrence marks a spot in both the global and individual histories that cannot be commuted across Thus while the letters b displaystyle b nbsp and c displaystyle c nbsp can be re ordered past d displaystyle d nbsp and e displaystyle e nbsp they cannot be reordered past a displaystyle a nbsp Thus the global history b c d a b e displaystyle bcdabe nbsp and the global history b d c a e b displaystyle bdcaeb nbsp both have as individual histories b c a b displaystyle bcab nbsp and d a e displaystyle dae nbsp indicating that the execution of d displaystyle d nbsp may happen before or after c displaystyle c nbsp However the letter a displaystyle a nbsp is synchronizing so that e displaystyle e nbsp is guaranteed to happen after c displaystyle c nbsp even though e displaystyle e nbsp is in a different process than c displaystyle c nbsp Properties editA history monoid is isomorphic to a trace monoid and as such is a type of semi abelian categorical product in the category of monoids In particular the history monoid H S 1 S 2 S n displaystyle H Sigma 1 Sigma 2 ldots Sigma n nbsp is isomorphic to the trace monoid M D displaystyle mathbb M D nbsp with the dependency relation given by D S 1 S 1 S 2 S 2 S n S n displaystyle D left Sigma 1 times Sigma 1 right cup left Sigma 2 times Sigma 2 right cup cdots cup left Sigma n times Sigma n right nbsp In simple terms this is just the formal statement of the informal discussion given above the letters in an alphabet S k displaystyle Sigma k nbsp can be commutatively re ordered past the letters in an alphabet S j displaystyle Sigma j nbsp unless they are letters that occur in both alphabets Thus traces are exactly global histories and vice versa Conversely given any trace monoid M D displaystyle mathbb M D nbsp one can construct an isomorphic history monoid by taking a sequence of alphabets S a b a b displaystyle Sigma a b a b nbsp where a b displaystyle a b nbsp ranges over all pairs in D displaystyle D nbsp Notes edit M W Shields Concurrent Machines Computer Journal 1985 28 pp 449 465 References editAntoni 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 Yves Metivier 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 Retrieved from https en wikipedia org w index php title History monoid amp oldid 1166185336, wikipedia, wiki, book, books, library,

article

, read, download, free, free download, mp3, video, mp4, 3gp, jpg, jpeg, gif, png, picture, music, song, movie, book, game, games.