In
mathematics and
computer science
Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to practical disciplines (includi ...
, 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
In abstract algebra, a branch of mathematics, a monoid is a set equipped with an associative binary operation and an identity element. For example, the nonnegative integers with addition form a monoid, the identity element being 0.
Monoid ...
provides a set of
synchronization primitives (such as
locks
Lock(s) may refer to:
Common meanings
*Lock and key, a mechanical device used to secure items of importance
*Lock (water navigation), a device for boats to transit between different levels of water, as in a canal
Arts and entertainment
* ''Lock ...
,
mutex
In computer science, a lock or mutex (from mutual exclusion) is a synchronization primitive: a mechanism that enforces limits on access to a resource when there are many threads of execution. A lock is designed to enforce a mutual exclusion concur ...
es 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
In computer science, the process calculi (or process algebras) are a diverse family of related approaches for formally modelling concurrent systems. Process calculi provide a tool for the high-level description of interactions, communications, and ...
, such as CSP the language of
communicating sequential processes
In computer science, communicating sequential processes (CSP) is a formal language for describing patterns of interaction in concurrent systems. It is a member of the family of mathematical theories of concurrency known as process algebras, or ...
, or CCS, the
calculus of communicating systems. History monoids were first presented by M.W. Shields.
[M.W. Shields "Concurrent Machines", ''Computer Journal'', (1985) 28 pp. 449–465.]
History monoids are
isomorphic to
trace monoid In 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 certa ...
s (free partially
commutative
In mathematics, a binary operation is commutative if changing the order of the operands does not change the result. It is a fundamental property of many binary operations, and many mathematical proofs depend on it. Most familiar as the name of ...
monoids) and to the
monoid
In abstract algebra, a branch of mathematics, a monoid is a set equipped with an associative binary operation and an identity element. For example, the nonnegative integers with addition form a monoid, the identity element being 0.
Monoid ...
of
dependency graph
In mathematics, computer science and digital electronics, a dependency graph is a directed graph representing dependencies of several objects towards each other. It is possible to derive an evaluation order or the absence of an evaluation order t ...
s. As such, they are
free object
In mathematics, the idea of a free object is one of the basic concepts of abstract algebra. Informally, a free object over a set ''A'' can be thought of as being a "generic" algebraic structure over ''A'': the only equations that hold between eleme ...
s and are
universal
Universal is the adjective for universe.
Universal may also refer to:
Companies
* NBCUniversal, a media and entertainment company
** Universal Animation Studios, an American Animation studio, and a subsidiary of NBCUniversal
** Universal TV, a ...
. The history monoid is a type of semi-abelian
categorical product in the
category
Category, plural categories, may refer to:
Philosophy and general uses
*Categorization, categories in cognitive science, information science and generally
* Category of being
* ''Categories'' (Aristotle)
* Category (Kant)
* Categories (Peirce) ...
of monoids.
Product monoids and projection
Let
:
denote an ''n''-tuple of (not necessarily pairwise disjoint)
alphabets
An alphabet is a standardized set of basic written graphemes (called letters) that represent the phonemes of certain spoken languages. Not all writing systems represent language in this way; in a syllabary, each character represents a syllab ...
. Let
denote all possible combinations of one finite-length string from each alphabet:
:
(In more formal language,
is the
Cartesian product of the
free monoid In abstract algebra, the free monoid on a set is the monoid whose elements are all the finite sequences (or strings) of zero or more elements from that set, with string concatenation as the monoid operation and with the unique sequence of zero ele ...
s of the
. The superscript star is the
Kleene star
In mathematical logic and computer science, the Kleene star (or Kleene operator or Kleene closure) is a unary operation, either on sets of strings or on sets of symbols or characters. In mathematics,
it is more commonly known as the free monoid ...
.) 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
In mathematics, a disjoint union (or discriminated union) of a family of sets (A_i : i\in I) is a set A, often denoted by \bigsqcup_ A_i, with an injection of each A_i into A, such that the images of these injections form a partition of A ( ...
.) Given any string
, we can pick out just the letters in some
using the corresponding
string projection In computer science, in the area of formal language theory, frequent use is made of a variety of string functions; however, the notation used is different from that used for computer programming, and some commonly used functions in the theoretical r ...
. A distribution
is the mapping that operates on
with all of the
, separating it into components in each free monoid:
:
Histories
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
In formal language theory, the empty string, or empty word, is the unique string of length zero.
Formal theory
Formally, a string is a finite, ordered sequence of characters such as letters, digits or spaces. The empty string is the special cas ...
. 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
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
A process is a series or set of activities that interact to produce a result; it may occur once-only or be recurrent or periodic.
Things called a process include:
Business and management
*Business process, activities that produce a specific se ...
than
.
Properties
A history monoid is isomorphic to a
trace monoid In 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 certa ...
, and as such, is a type of semi-abelian
categorical product in the
category
Category, plural categories, may refer to:
Philosophy and general uses
*Categorization, categories in cognitive science, information science and generally
* Category of being
* ''Categories'' (Aristotle)
* Category (Kant)
* Categories (Peirce) ...
of monoids. In particular, the history monoid
is isomorphic to the trace monoid
with the
dependency relation
In computer science, in particular in concurrency (computer science), concurrency theory, a dependency relation is a binary relation on a finite domain \Sigma, symmetric relation, symmetric, and reflexive relation, reflexive; i.e. a finite toleran ...
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
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, 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.
Concurrency (computer science)
Semigroup theory
Formal languages
Free algebraic structures