Home | Monoids and X-Machines X-Machines.Com


Theory of X-Machines



Monoids and X-Machines

A key feature of X-machine theory is the number of natural constructions that give rise to monoid homomorphisms. Far from being a mathematical curiosity this is an exciting development, for in general, monoids play an important role in the study of real concurrency, and the close relationship between X-machines and monoids therefore points to a currently unexploited role for X-machines in the study of concurrent semantics.

Recall that a semigroup is a set S together with a binary function : S S ----> S satisfying the associative rule

for all s1, s2, s3 in S : (s1 s2 ) s3 = s1 ( s2 s3 ) ( Equ. 1 )

A semigroup (S,) is a monoid if there is some two-sided identity element 1 in S identified by the property

for all s in S : s 1S = s = 1S s ( Equ. 2 )

A function f: (S, S, 1S) ----> (T, T, 1T) from one monoid S to another monoid T is a monoid homomorphism if it a semigroup homomorphism i.e.,

for all s1, s2 in S : (s1 S s2 )f = s1f T s2f ( Equ. 3 )

and, in addition,

1Sf = 1T ( Equ. 4 )

It is worth noting also, the easy fact that chaining together two monoid homomorphisms F: s1 ----> s2 and G: s2 ----> s3 gives a third monoid homomorphism FG: s1 ----> s3.

The monoid RelX

Given a set X, we shall write RelX to denote the type [ X ~~~> X ] of all binary relations on X. Each R in RelX can be thought of as a subset of XX, whence RelX = 2 XX i.e., the set of all subsets of XX, also called the power set of XX, P(XX). In particular, if |X| = n is finite, then |RelX| = 2n, and if |X| = aleph is infinite, then |RelX| = 2aleph. The size of RelX is super-exponential in the size of X, and quickly becomes large for even small values of |X|, viz.

46.55 104
53.35 107
101.27 1030
202.58 10120
308.45 10270

For x, y in X it is common to see the statement (x, y) R RelX expressed in various ways, including xR = y and x R y. More accurately, we define xR to be the set of all y in X for which (x, y) R. Algebraically speaking, RelX is a monoid under relational composition, where the product of two binary relations R1 and R2 is the binary relation R1R2 defined by x ( R1R2 ) = (xR1)R2 and the relation 1X = { (x, x) | x X } is the unique two-sided identity for this product. p>

The homomorphisms *: A* ----> RelX

The set A* of all (finitary) strings over some alphabet A is another monoid. The product in A* is string concatenation, and the unique two-sided identity is the empty string, denoted ( ) or e. Any function : A ----> RelX induces a monoid homomorphism *: A* ----> RelX, under which the string a = a0...an is mapped to the relation a* = a0...an and e* = 1X.

The homomorphisms fU: PS ----> RelX

Given any set S, the power set PS is a monoid twice over. Given two subsets U, V of S we shall take UV = U U V and 1PS = . It would, however, be as valid to use intersection as the "product" with identity S. The complementation map U |---> S\U is a homomorphism between the two monoid structures on PS. However, the importance of power sets to X-machines lies in the ease with which they allow us to construct new homomorphisms.

Lemma. If S and T are sets, any relation f: S ~~~> PT induces a monoid homomorphism fU: PS ----> PT defined by

for all subsets U of S : UfU = U{ uf | u U }. ( Equ. 5 )

Proof. Note first that the identity element in both PS and PT is , whence the identity is preserved by virtue of the convention U = . All that remains is to observe that

(U U V) fU
     = U{ wf | w U U V }
     = U{ wf | w U } U U{ wf | w V }
     = UfU U VfU
( Equ. 6 )

i.e., fU preserves the "multiplication" in PS. Q.E.D.

If we choose T = XX, and recall that P(XX) = RelX, we see that, no matter what the set S, any relation from S to RelX induces a corresponding monoid homomorphism from PS to RelX. In particular, the identity map on RelX induces a monoid homomorphism 1U: PRelX ----> RelX that is relevant to the representation of non-deterministic X-machines by their deterministic counterparts. This homomorphism maps each collection { ~n } of relations on X to their union, the relation

x ~ y <===> for some n : x ~n y ( Equ. 7 )

Algebraic X-machines

An algebraic X-machine M = F comprises a finite state recogniser F and a labelling function : A ----> RelX, where A is the set of labels on the arcs of F. As one traverses a recognised path through F, so one encounters one relation after another, and the path computation corresponding to this traversal is the relation obtained by composing the individual arrow labels in the order encountered. In general there will be many valid paths through F, each contributing to the computational behaviour of M. The relation, |M|, computed by M is defined as the union of all its constituent path computations.

We've seen that the function : A ----> RelX induces a monoid homomorphism *: A* ----> RelX, under which the string a = a0...an is mapped to the relation a* = a0...an RelX. and e* = 1X. Clearly, the homomorphism * encapsulates the process of determining path computations, in that a* is the computation corresponding to traversal of any path that recognises a. Moreover, the relation |M| is just the union of all the path computations, which is just the monoid homomorphism *U: P(A*) ----> RelX given by

for each subset L of A* : L*U = U{ a* | a L } ( Equ. 8 )

applied to the particular (regular) language L = L(F) recognised by F. It is now a straightforward exercise to verify that

|M| = L*U ( Equ. 9 )

As this equality illustrates, the actual structure of F is irrelevant to our calculations - all that matters is the language recognised, which we shall normally denote |F|. This is why X-machine refinement is particularly tricky. We cannot simply ask that the computed relations of a given machine be preserved during refinement, because refinement concerns the replacement of structural and functional components with other, more closely detailed, components, while the relation |M| has no dependence upon those structures. Rather, refinement has to be defined at a lower, machine dependent, level, or its equivalent.

It's important to notice, also, that whatever the language |F| may be, we can be certain that it is fairly limited in representational scope, because finite state recognisers can only generate regular languages, which are particularly simple in structure. If we allowed X-machines to be defined over more powerful finitary languages, for example Turing-recognisable languages, we might not necessarily be capable of computing any new class of relation, but the computational complexities of doing so might be greatly reduced.

Moreover, restricting ourselves to using A* to represent typical behavioural sequences is by no means justified, especially as the finite-state structure of F imposes the further constraint that A be finite. Ever since Mazurkiewicz demonstrated their relevance to concurrency theory, for example, there has been a clear case for examining the properties of partially commutative monoids [Kir99], and we have argued elsewhere for the significance of infinite alphabets [Sta94]. Moreover, real-time theorists might challenge the need for strings to be finitary at all.

Towards a Generalised Theory of X-machines

In our own work we have found it useful to introduce a generalised theory of X-machines, since the results of the standard theory often depend only on the monoid-based properties of its constructions, and these can usually be applied much more generally, with no extra effort.

For each set A we first need some canonical construction that associates with the "alphabet" A some monoid A@, whose elements will be the "strings" over A. Moreover, the relationship between A and A@ must be such that any function : A ----> RelX is associated in a canonical way with a related monoid homomorphism @: A@ ----> RelX. In computational terms, the mapping A |---> A@ encapsulates the particular recursion regime within which we choose to operate. So, for example, the standard X-machine choice, A@ = A*, encapsulates the recursion regime in which operations occur discretely in a definite linear order, and only finitely many operations can occur during any period of interest. Similarly, introducing some independency i (i.e., some set of commutativity relations) and taking A@ = A*/i would generate a recursion regime akin to that of Mazurkiewicz trace theory.

Typically we would define A@ in terms of some function space (AU{A})Z, for some ordered space Z which may or may not be independent of A. For example, the standard X-machine choice A@ = A* is essentially the function space

{ a : w0 ----> (AU{A}) |
     (for some n : a(n)={A}) & (for all m,n: a(n)= {A} &m>n ==> a(m)={A}) }
( Equ. 10 )

of sequences over A which eventually become undefined. Likewise, Kwiatkowska & Stannett's research on transfinite (Mazurkiewicz) trace theory, where it was noted that well-ordered observations of real-time processes always generate traces over countable ordinals, focussed on monoids of the form

{ a : w1 ----> (AU{A}) |
     (for some n : a(n)={A}) & (for all m,n: a(n)= {A} &m>n ==> a(m)={A}) } / i
( Equ. 11 )

It is easy to see that every initial ordinal w generates a corresponding recursion regime. Nor, of course, need we restrict attention to ordinals. Our own TXM constructions rely on the observation that, given any collection of directed spaces D, we can construct suitable D-based monoids based on A.

No matter what recursion regime we select, however, we are assured that each labelling induces a monoid homomorphism @U: P(A*) ----> RelX given by

for each subset L of A@ : L@U = U{ a@ | a L } ( Equ. 12 )

i.e., "languages" over A are mapped in a consistent manner to relations on X. This allows us to ask additional questions concerning computational technologies, e.g., given such-and-such a relation R, for which combination of language type and recursion regime will R be computable?

Further Reading

Samuel Eilenberg (1974) Automata, Languages and Machines, vol A. Academic Press.
Mazurkiewicz trace languages as partially commutative monoids
Daniel Kirsten (1999) On Decision Problems of Recognisable Trace Languages. Ph.D. Thesis, Dresden University of Technology.
Transfinite Mazurkiewicz traces
Marta Kwiatkowska & Mike Stannett (1992) On Transfinite Traces. ASMICS Proc. Universitat Stuttgart Fakultat Informatik, Bericht 4/92, 123-57.
Convergence of Mazurkiewicz traces
Mike Stannett (1994) Infinite Concurrent Systems - I. The relationship between metric and order convergence. Formal Aspects of Computing 6, 696-715.
Copyright © 2000-2013 Mike Stannett. All Rights Reserved.