Semantic Domains for Combining Probability and Non-Determinism
Semantic Domains for Combining Probability and Non-Determinism
复制标题
DOI：
10.1016/j.entcs.2004.06.063
复制
发表时间：
2005-04
期刊：
影响因子：
--
通讯作者：
Regina Tix;K. Keimel;G. Plotkin
中科院分区：
文献类型：
--
作者：
Regina Tix;K. Keimel;G. Plotkin
我们提出了支持概率选择和不确定性选择的领域理论模型。在一个。麦克艾弗和摩根。概率恶魔程序的部分正确性。理论计算机科学266 (2001)513-541]，Morgan和McIver使用领域理论工具，为一种简单的命使式语言开发了一种特别语义，该语言具有离散状态空间上的概率和非确定性选择算子。我们提出了一个模型，也使用了D.S. Scott意义上的领域理论(参见[G。吉尔兹，K.H.霍夫曼，k.k Keimel， J.D.劳森，M.W.米斯洛夫和D.S.斯科特。连续格和连续域，《数学百科全书及其应用》第93卷。剑桥大学出版社，剑桥，2003])，但建立在相当一般的连续域而不是离散状态空间上。我们的构造结合了众所周知的非确定性建模领域——下、上和凸幂域，以及Jones和Plotkin的概率幂域[C]。琼斯和G.普洛特金。评估的概率幂域。第四届计算机科学逻辑年会论文集，页186-195。IEEE计算机学会出版社，1989]建模概率选择。结果是概率幂域上的上幂域、下幂域和凸幂域的变体（见第4章）。为了证明这些组合幂域的理想的普遍方程性质，我们发展了具有Scott拓扑的连续有向完全部分有序锥上的Scott-连续线性泛函、次线性泛函和超线性泛函的夹心和分离定理，类似于泛函分析中拓扑向量空间的相应定理（见第3章）。最后，我们展示了我们的语义域可以很好地适用于Morgan和McIver使用的语言。
We present domain-theoretic models that support both probabilistic and nondeterministic choice. In [A. McIver and C. Morgan. Partial correctness for probablistic demonic programs. Theoretical Computer Science 266 (2001) 513–541], Morgan and McIver developed an ad hoc semantics for a simple imperative language with both probabilistic and nondeterministic choice operators over a discrete state space, using domain-theoretic tools. We present a model also using domain theory in the sense of D.S. Scott (see e.g. [G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M.W. Mislove, and D.S. Scott. Continuous Lattices and Domains, volume 93 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge, 2003]), but built over quite general continuous domains instead of discrete state spaces. Our construction combines the well-known domains modelling nondeterminism – the lower, upper and convex powerdomains, with the probabilistic powerdomain of Jones and Plotkin [C. Jones and G. Plotkin. A probabilistic powerdomain of evaluations. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science, pages 186–195. IEEE Computer Society Press, 1989] modelling probabilistic choice. The results are variants of the upper, lower and convex powerdomains over the probabilistic powerdomain (see Chapter 4). In order to prove the desired universal equational properties of these combined powerdomains, we develop sandwich and separation theorems of Hahn-Banach type for Scott-continuous linear, sub- and superlinear functionals on continuous directed complete partially ordered cones, endowed with their Scott topologies, in analogy to the corresponding theorems for topological vector spaces in functional analysis (see Chapter 3). In the end, we show that our semantic domains work well for the language used by Morgan and McIver.