A comparison of semantic domains for interleaving
Richard Connelly · 1990
This dissertation contains the construction of an epimorphism $\epsilon$: P(D) $\to$ R between two recursively defined semantic domains for concurrent programming that allow interleaving but do not require fairness. The domain R is an object in the NO-category ND$\perp$ (which has also been called NDO$\perp$ and is the non-deterministic resumption domain defined by Hennessy and Plotkin. As an object in ND$\perp$, R has a union (i.e., choice) operator built into its definition. The domain D is an object in the O-category CPO$\perp$ and is a recursively defined deterministic resumption domain given by the author. The functor P: CPO$\perp$ $\to$ ND$\perp$ is Plotkin's powerdomain functor. The application of P to D makes it non-deterministic. The key to the construction of $\epsilon$ is a newly defined tensor product $\otimes$ for the category NO which is also a tensor product for the category ND (which has also been called NDO). In ND, the tensor product $\otimes$ generates a tensor product $\otimes\sb N$ over a denumerable index. The construction of $\otimes$ is based on a tensor product for ND$\perp$ defined by Hennessy and Plotkin. The epimorphism $\epsilon$ is constructed by iterating along the definitions of D and R using an endofunctor on the comma category P$\downarrow$I. The specific definition of $\epsilon$ is done using Beierle's pointwise limit construction in a comma category. Additionally, it is proved that $\epsilon$ is operationally consistent. That is, $\epsilon$ is consistent with the two functions that remove the resumptions from D and R respectively.