混合幂域：概率与非确定性的结合
Mixed powerdomains for probability and nondeterminism
AI总结：
本文研究结合普通非确定性与概率非确定性的混合幂域，将其刻画为自由代数，建立函数表示定理及状态与谓词变换器等价性，采用Kegelspitzen方法处理，涵盖下、上、序凸三种形式。
摘要：
我们考虑结合普通非确定性和概率非确定性的混合幂域。我们将它们刻画为合适的（不）等式理论的自由代数；我们建立了函数表示定理；并展示了状态变换器与适当健康的谓词变换器之间的等价性。扩展的非负实数作为“真值”。与幂域通常的情况一样，一切都有三种形式：下、上和序凸。这些幂域是合适的子概率估值的凸集，对应于在概率选择之前解析非确定性选择。在代数上，这对应于概率选择算子对非确定性选择算子的分配。（结合两种非确定性形式的另一种方法是在先解析概率选择，得到随机集的域论版本。然而，正如我们也展示的，代数方法随后会遇到困难。）我们不直接使用估值，而是采用域论泛函分析方法，使用称为Kegelspitzen的域论抽象凸集；这些等价于Graham和Jones的抽象概率代数，但更方便使用。因此，我们定义幂Kegelspitzen，并考虑自由代数、函数表示和谓词变换器。为此，我们利用了先前关于域论锥（d-锥）的工作，两者之间的桥梁由Kegelspitzen上的自由d-锥构造提供。
英文摘要：
We consider mixed powerdomains combining ordinary nondeterminism and probabilistic nondeterminism. We characterise them as free algebras for suitable (in)equation-al theories; we establish functional representation theorems; and we show equivalencies between state transformers and appropriately healthy predicate transformers. The extended nonnegative reals serve as `truth-values'. As usual with powerdomains, everything comes in three flavours: lower, upper, and order-convex. The powerdomains are suitable convex sets of subprobability valuations, corresponding to resolving nondeterministic choice before probabilistic choice. Algebraically this corresponds to the probabilistic choice operator distributing over the nondeterministic choice operator. (An alternative approach to combining the two forms of nondeterminism would be to resolve probabilistic choice first, arriving at a domain-theoretic version of random sets. However, as we also show, the algebraic approach then runs into difficulties.) Rather than working directly with valuations, we take a domain-theoretic functional-analytic approach, employing domain-theoretic abstract convex sets called Kegelspitzen; these are equivalent to the abstract probabilistic algebras of Graham and Jones, but are more convenient to work with. So we define power Kegelspitzen, and consider free algebras, functional representations, and predicate transformers. To do so we make use of previous work on domain-theoretic cones (d-cones), with the bridge between the two of them being provided by a free d-cone construction on Kegelspitzen.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
