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.
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.
Let 
denote an "n"-tuple of (not necessarily pairwise disjoint) alphabets formula_2. Let formula_3 denote all possible combinations of one finite-length string from each alphabet:
(In more formal language, formula_3 is the Cartesian product of the free monoids of the formula_2. The superscript star is the Kleene star.) Composition in the product monoid is component-wise, so that, for
and
then
for all formula_10 in formula_3. Define the union alphabet to be
(The union here is the set union, not the disjoint union.) Given any string formula_13, we can pick out just the letters in some formula_14 using the corresponding string projection formula_15. A distribution formula_16 is the mapping that operates on formula_13 with all of the formula_18, separating it into components in each free monoid:
Histories.
For every formula_20, the tuple formula_21 is called the elementary history of "a". It serves as an indicator function for the inclusion of a letter "a" in an alphabet formula_2. That is,
where
Here, formula_25 denotes the empty string. The history monoid formula_26 is the submonoid of the product monoid formula_3 generated by the elementary histories: formula_28 (where the superscript star is the Kleene star applied with a component-wise definition of composition as given above). The elements of formula_26 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 formula_2 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, formula_31 and formula_32. The union alphabet is of course formula_33. The elementary histories are formula_34, formula_35, formula_36, formula_37 and formula_38. In this example, an individual history of the first process might be formula_39 while the individual history of the second machine might be formula_40. Both of these individual histories are represented by the global history formula_41, since the projection of this string onto the individual alphabets yields the individual histories. In the global history, the letters formula_42 and formula_43 can be considered to commute with the letters formula_44 and formula_45, 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 formula_46 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 formula_42 and formula_43 can be re-ordered past formula_44 and formula_45, they cannot be reordered past formula_46. Thus, the global history formula_52 and the global history formula_53 both have as individual histories formula_54 and formula_55, indicating that the execution of formula_44 may happen before or after formula_43. However, the letter formula_46 is synchronizing, so that formula_45 is guaranteed to happen after formula_43, even though formula_45 is in a different process than formula_43.
Properties.
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 formula_63 is isomorphic to the trace monoid formula_64 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 formula_2 can be commutatively re-ordered past the letters in an alphabet formula_67, unless they are letters that occur in both alphabets. Thus, traces are exactly global histories, and vice versa.
Conversely, given any trace monoid formula_64, one can construct an isomorphic history monoid by taking a sequence of alphabets formula_69 where formula_70 ranges over all pairs in formula_71.