VOOZH about

URL: https://en.wikipedia.org/wiki/History_monoid

⇱ History monoid - Wikipedia


Jump to content
From Wikipedia, the free encyclopedia

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

πŸ‘ {\displaystyle A=(\Sigma _{1},\Sigma _{2},\ldots ,\Sigma _{n})}

denote an n-tuple of (not necessarily pairwise disjoint) alphabets πŸ‘ {\displaystyle \Sigma _{k}}
. Let πŸ‘ {\displaystyle P(A)}
denote all possible combinations of one finite-length string from each alphabet:

πŸ‘ {\displaystyle P(A)=\Sigma _{1}^{*}\times \Sigma _{2}^{*}\times \cdots \times \Sigma _{n}^{*}}

(In more formal language, πŸ‘ {\displaystyle P(A)}
is the Cartesian product of the free monoids of the πŸ‘ {\displaystyle \Sigma _{k}}
. The superscript star is the Kleene star.) Composition in the product monoid is component-wise, so that, for

πŸ‘ {\displaystyle \mathbf {u} =(u_{1},u_{2},\ldots ,u_{n})\,}

and

πŸ‘ {\displaystyle \mathbf {v} =(v_{1},v_{2},\ldots ,v_{n})\,}

then

πŸ‘ {\displaystyle \mathbf {uv} =(u_{1}v_{1},u_{2}v_{2},\ldots ,u_{n}v_{n})\,}

for all πŸ‘ {\displaystyle \mathbf {u} ,\mathbf {v} }
in πŸ‘ {\displaystyle P(A)}
. Define the union alphabet to be

πŸ‘ {\displaystyle \Sigma =\Sigma _{1}\cup \Sigma _{2}\cup \cdots \cup \Sigma _{n}.\,}

(The union here is the set union, not the disjoint union.) Given any string πŸ‘ {\displaystyle w\in \Sigma ^{*}}
, we can pick out just the letters in some πŸ‘ {\displaystyle \Sigma _{k}^{*}}
using the corresponding string projection πŸ‘ {\displaystyle \pi _{k}:\Sigma ^{*}\to \Sigma _{k}^{*}}
. A distribution πŸ‘ {\displaystyle \pi :\Sigma ^{*}\to P(A)}
is the mapping that operates on πŸ‘ {\displaystyle w\in \Sigma ^{*}}
with all of the πŸ‘ {\displaystyle \pi _{k}}
, separating it into components in each free monoid:

πŸ‘ {\displaystyle \pi (w)\mapsto (\pi _{1}(w),\pi _{2}(w),\ldots ,\pi _{n}(w)).\,}

Histories

[edit]

For every πŸ‘ {\displaystyle a\in \Sigma }
, the tuple πŸ‘ {\displaystyle \pi (a)}
is called the elementary history of a. It serves as an indicator function for the inclusion of a letter a in an alphabet πŸ‘ {\displaystyle \Sigma _{k}}
. That is,

πŸ‘ {\displaystyle \pi (a)=(a_{1},a_{2},\ldots ,a_{n})}

where

πŸ‘ {\displaystyle a_{k}={\begin{cases}a{\mbox{ if }}a\in \Sigma _{k}\\\varepsilon {\mbox{ otherwise }}.\end{cases}}}

Here, πŸ‘ {\displaystyle \varepsilon }
denotes the empty string. The history monoid πŸ‘ {\displaystyle H(A)}
is the submonoid of the product monoid πŸ‘ {\displaystyle P(A)}
generated by the elementary histories: πŸ‘ {\displaystyle H(A)=\{\pi (a)|a\in \Sigma \}^{*}}
(where the superscript star is the Kleene star applied with a component-wise definition of composition as given above). The elements of πŸ‘ {\displaystyle H(A)}
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 πŸ‘ {\displaystyle \Sigma _{k}}
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, πŸ‘ {\displaystyle \Sigma _{1}=\{a,b,c\}}
and πŸ‘ {\displaystyle \Sigma _{2}=\{a,d,e\}}
. The union alphabet is of course πŸ‘ {\displaystyle \Sigma =\{a,b,c,d,e\}}
. The elementary histories are πŸ‘ {\displaystyle (a,a)}
, πŸ‘ {\displaystyle (b,\varepsilon )}
, πŸ‘ {\displaystyle (c,\varepsilon )}
, πŸ‘ {\displaystyle (\varepsilon ,d)}
and πŸ‘ {\displaystyle (\varepsilon ,e)}
. In this example, an individual history of the first process might be πŸ‘ {\displaystyle bcbcc}
while the individual history of the second machine might be πŸ‘ {\displaystyle ddded}
. Both of these individual histories are represented by the global history πŸ‘ {\displaystyle bcbdddcced}
, since the projection of this string onto the individual alphabets yields the individual histories. In the global history, the letters πŸ‘ {\displaystyle b}
and πŸ‘ {\displaystyle c}
can be considered to commute with the letters πŸ‘ {\displaystyle d}
and πŸ‘ {\displaystyle e}
, 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 πŸ‘ {\displaystyle a}
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 πŸ‘ {\displaystyle b}
and πŸ‘ {\displaystyle c}
can be re-ordered past πŸ‘ {\displaystyle d}
and πŸ‘ {\displaystyle e}
, they cannot be reordered past πŸ‘ {\displaystyle a}
. Thus, the global history πŸ‘ {\displaystyle bcdabe}
and the global history πŸ‘ {\displaystyle bdcaeb}
both have as individual histories πŸ‘ {\displaystyle bcab}
and πŸ‘ {\displaystyle dae}
, indicating that the execution of πŸ‘ {\displaystyle d}
may happen before or after πŸ‘ {\displaystyle c}
. However, the letter πŸ‘ {\displaystyle a}
is synchronizing, so that πŸ‘ {\displaystyle e}
is guaranteed to happen after πŸ‘ {\displaystyle c}
, even though πŸ‘ {\displaystyle e}
is in a different process than πŸ‘ {\displaystyle c}
.

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 πŸ‘ {\displaystyle H(\Sigma _{1},\Sigma _{2},\ldots ,\Sigma _{n})}
is isomorphic to the trace monoid πŸ‘ {\displaystyle \mathbb {M} (D)}
with the dependency relation given by

πŸ‘ {\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).}

In simple terms, this is just the formal statement of the informal discussion given above: the letters in an alphabet πŸ‘ {\displaystyle \Sigma _{k}}
can be commutatively re-ordered past the letters in an alphabet πŸ‘ {\displaystyle \Sigma _{j}}
, unless they are letters that occur in both alphabets. Thus, traces are exactly global histories, and vice versa.

Conversely, given any trace monoid πŸ‘ {\displaystyle \mathbb {M} (D)}
, one can construct an isomorphic history monoid by taking a sequence of alphabets πŸ‘ {\displaystyle \Sigma _{a,b}=\{a,b\}}
where πŸ‘ {\displaystyle (a,b)}
ranges over all pairs in πŸ‘ {\displaystyle D}
.

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.