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 (includin ...
, a history monoid is a way of representing the histories of concurrently running computer
processes
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 ...
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.
Monoids ...
provides a set of
synchronization primitive
In computer science, synchronization refers to one of two distinct but related concepts: synchronization of processes, and synchronization of data. ''Process synchronization'' refers to the idea that multiple processes are to join up or handshake ...
s (such as
locks,
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 concu ...
es or
thread joins) for providing rendezvous points between a set of independently executing processes or
threads
Thread may refer to:
Objects
* Thread (yarn), a kind of thin yarn used for sewing
** Thread (unit of measurement), a cotton yarn measure
* Screw thread, a helical ridge on a cylindrical fastener
Arts and entertainment
* ''Thread'' (film), 2016 ...
.
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 o ...
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.
Monoids ...
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 ele ...
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 category theory, the product of two (or more) objects in a category is a notion designed to capture the essence behind constructions in other areas of mathematics such as the Cartesian product of sets, the direct product of groups or rin ...
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 syl ...
. Let
denote all possible combinations of one finite-length string from each alphabet:
:
(In more formal language,
is the
Cartesian product
In mathematics, specifically set theory, the Cartesian product of two sets ''A'' and ''B'', denoted ''A''×''B'', is the set of all ordered pairs where ''a'' is in ''A'' and ''b'' is in ''B''. In terms of set-builder notation, that is
: A\ ...
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 elem ...
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
In set theory, the union (denoted by ∪) of a collection of sets is the set of all elements in the collection. It is one of the fundamental operations through which sets can be combined and related to each other.
A refers to a union of ze ...
, 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 . 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
In mathematics, an indicator function or a characteristic function of a subset of a set is a function that maps elements of the subset to one, and all other elements to zero. That is, if is a subset of some set , one has \mathbf_(x)=1 if x ...
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
Thread may refer to:
Objects
* Thread (yarn), a kind of thin yarn used for sewing
** Thread (unit of measurement), a cotton yarn measure
* Screw thread, a helical ridge on a cylindrical fastener
Arts and entertainment
* ''Thread'' (film), 2016 ...
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
In computer science, synchronization refers to one of two distinct but related concepts: synchronization of processes, and synchronization of data. ''Process synchronization'' refers to the idea that multiple processes are to join up or handshake ...
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 category theory, the product of two (or more) objects in a category is a notion designed to capture the essence behind constructions in other areas of mathematics such as the Cartesian product of sets, the direct product of groups or rin ...
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 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