In
mathematics
Mathematics is a field of study that discovers and organizes methods, Mathematical theory, theories and theorems that are developed and Mathematical proof, proved for the needs of empirical sciences and mathematics itself. There are many ar ...
and
computer science
Computer science is the study of computation, information, and automation. Computer science spans Theoretical computer science, theoretical disciplines (such as algorithms, theory of computation, and information theory) to Applied 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
In abstract algebra, 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 .
Monoids are semigroups with identity ...
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
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 p ...
, 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
In mathematics, an isomorphism is a structure-preserving mapping or morphism between two structures of the same type that can be reversed by an inverse mapping. Two mathematical structures are isomorphic if an isomorphism exists between the ...
to
trace monoids (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. Perhaps most familiar as a pr ...
monoids) and to the
monoid
In abstract algebra, 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 .
Monoids are semigroups with identity ...
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
Category, plural categories, may refer to:
General uses
*Classification, the general act of allocating things to classes/categories Philosophy
* Category of being
* ''Categories'' (Aristotle)
* Category (Kant)
* Categories (Peirce)
* Category ( ...
of monoids.
Product monoids and projection
Let
:
denote an ''n''-tuple of (not necessarily pairwise disjoint)
alphabets
An alphabet is a standard set of letter (alphabet), letters written to represent particular sounds in a spoken language. Specifically, letters largely correspond to phonemes as the smallest sound segments that can distinguish one word from a ...
. 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 and , denoted , is the set of all ordered pairs where is an element of and is an element of . In terms of set-builder notation, that is
A\times B = \.
A table c ...
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 ...
s of the
. The superscript star is the
Kleene star
In mathematical logic and theoretical computer science, the Kleene star (or Kleene operator or Kleene closure) is a unary operation on a Set (mathematics), set to generate a set of all finite-length strings that are composed of zero or more repe ...
.) 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, the disjoint union (or discriminated union) A \sqcup B of the sets and is the set formed from the elements of and labelled (indexed) with the name of the set from which they come. So, an element belonging to both and appe ...
.) 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 , then the indicator functio ...
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 (computer science), string of length zero.
Formal theory
Formally, a string is a finite, ordered sequence of character (symbol), characters such as letters, digits ...
. 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
A machine is a physical system that uses power to apply forces and control movement to perform an action. The term is commonly applied to artificial devices, such as those employing engines or motors, but also to natural biological macromol ...
); 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 s ...
than
.
Properties
A history monoid is isomorphic to a
trace monoid, and as such, is a type of semi-abelian
categorical product in the
category
Category, plural categories, may refer to:
General uses
*Classification, the general act of allocating things to classes/categories Philosophy
* Category of being
* ''Categories'' (Aristotle)
* Category (Kant)
* Categories (Peirce)
* 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
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