Towards a foundation for semantics in complete metric spaces (Q1173767)

In the last years a series of papers appeared that deal with the semantics of those languages or systems that allow for some notion of concurrency. We present here an investigation and foundation of the metric space approach of \textit{J. W. de Bakker} and \textit{J. I. Zucker} [Inf. Control 54, 70-120 (1982; Zbl 0508.68011)]. In order to do so we briefly sketch how semantics is defined in [loc. cit.]. The basic concepts are the notion of a ``process domain'' and a ``domain equation''. Given a language \(L\) for which semantics is to be defined, the authors suggest to construct a suitable equation \(P={\mathcal F}(P)\), called domain equation, such that the solution of this equation (a complete metric space) provides a domain for the interpretation of programs, i.e., the meaning function maps programs to elements of this solution. De Bakker and Zucker demonstrate their ideas concerning the solution of such equations by considering the following four prototypes: \[ \begin{aligned} P &= \{p_ 0\}\cup (A\times P) \tag{1}\\ P &= \{p_ 0\}\cup \wp_ c(A\times P) \tag{2}\\ P &= \{p_ 0\}\cup (A\to \wp_ c(B\times P)) \tag{3}\\ P &= \{p_ 0\}\cup (A\to \wp_ c((B\times P)\cup (C\to P))), \tag{4}\end{aligned} \] where, e.g., the Cartesian product is used to model the sequencing of actions, the powerset construction \(\wp_ c\) and the function space construction are used to model nondeterminism, concurrency, and communication. For each equation \(P={\mathcal F}_ i(P)\), \(i=1,2,3\), de Bakker and Zucker construct a solution as follows (the last equation is left to the reader): A sequence \(((P_ n,d_ n))\) of metric spaces is constructed by setting \(P_ 0=\{p_ 0\}\), \(P_ j={\mathcal F}_ i(P_{j-1})\), and \(P_ \omega\) is defined as \((\cup P_ n, \cup d_ n)\). It is then shown that the completion \((P,d)\) of \(P_ \omega\) is a solution of the given equation. The thus constructed solutions serve as semantic domains for various sample languages. When looking closer at the proposed handling of process domain equations, a number of questions arise immediately: Is the thus constructed solution the only solution? If not, what features characterize the constructed solution? And most important, under what conditions is it possible to give a solution of an equation \(P={\mathcal F}(P)\) in such a way? What properties must the operator \({\mathcal F}\) have in order to guarantee the existence of a solution altogether? In this paper, we deal with these questions.