概率编程的低级别指称语义研究

可在www.sciencedirect.com在线获取理论计算机科学电子笔记347（2019）303-324www.elsevier.com/locate/entcs低层概率程序的指称语义关于Nondeterminism王迪a Jan Ho Rummanna和Thomas Repsb，c卡内基梅隆大学威斯康星大学c GrammaTech公司摘要概率编程是一种越来越流行的建模随机性和不确定性的形式主义。为概率程序设计语义模型已经得到了广泛的研究，但在技术上具有挑战性。 当试图解释（i）非结构化控制时，会出现特别的复杂性--低级别命令式程序中的特性;（ii）一般递归，一种广泛使用的编程范式;（iii）非确定性，通常用于表示概率模型中的对抗行为，以及以支持以房地产为基础的发展。本文提出了一个指称语义框架，支持上述三个功能，同时允许以不同的方式处理非确定性。为了同时支持概率选择和非确定性选择，给出了控制流超图的语义.语义遵循代数方法：只要某些代数属性成立，它就可以以不同的方式实例化。特别是，语义可以被实例化，以支持程序状态或状态转换器之间的非确定性。我们开发了一个新的形式化的非确定性的基础上的次概率核的幂域。权力域中的语义对象享有我们称之为广义凸性的概念，这是凸性的推广。作为一个应用程序，本文勾勒出一个代数框架的概率程序，这已经提出了一个配套文件中的静态分析。关键词：概率规划，指称语义，控制流超图，不确定性，幂域1引言概率编程为实现随机算法[2]、加密协议[3]、认知模型[31]和机器学习算法[29]提供了一个强大的框架。近年来概率规划研究的一个重要焦点是对概率规划和系统进行严格的在这样的工作的第一步是提供一个合适的形式语义概率程序。尽管许多现有的工作集中在高级概率程序上，例如，lambda演算[8]，高阶函数[32，20]和递归https://doi.org/10.1016/j.entcs.2019.09.0161571-0661/© 2019作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。304D. Wang等人/理论计算机科学电子笔记347（2019）303−⊕⊕类型[63]，我们观察到低级特征可以自然出现。例如，当为概率编程语言开发编译器时[26，56]，我们需要命令式目标语言的语义来证明编译器的正确性。已经有关于结构良好的命令式程序的指称语义的研究[43，44，47，48，62，34，38，55，7]，以及基于马尔可夫链（MC）和马尔可夫决策过程（MDP）的控制流图（CFG）的操作语义（[25，14，15]）。一方面，我们更喜欢CFG作为程序表示，因为它们支持丰富的低级功能，例如非结构化的流，例如，由break和continue引入的。另一方面，从严格推理的角度来看，指称语义（i）从程序执行的细节中抽象出来，专注于程序效果，（ii）在程序片段的语义是从片段的适当成分的语义中建立的意义上是组合的因此，在本文中，我们设计了一个指称语义的低级别的我们的工作有三个主要贡献：• 我们使用超图表示低层次的概率程序与非结构化的控制流，一般递归，和不确定性。• 我们开发了一个新的模型的不确定性的概率规划，其中涉及状态转换器之间的不确定性，反对一个共同的模型，涉及程序状态之间的不确定性域理论表征。• 我们设计了一个代数的指称语义框架。 拥有一个框架的好处是它可以用不同的非确定性模型来实例化。我们将展示如何实例化的框架，使用两种不同的方法来正式非决定论在Ex。5.2.我们还表明，对于没有过程调用和非确定性的程序，所得到的指称语义等价于基于分布的操作语义（§5.2）。我们将指称语义直接定义为对第2节中介绍的低级概率程序的控制流超图（CFHG）的解释。超图由超边组成，每条超边连接一个源节点和可能的多个目的节点。例如，概率选择由具有两个目的地的加权超边然后，非确定性由从同一节点开始的多个超边表示超边缘的解释如果CFHG被视为一个标准图，从每个分支节点的后继者的子路径将被独立地分析。相比之下，我们的超图方法将概率为p的概率选择超边解释为函数λa.λb.ap b，其中p是通过两个后继者的子路径加权p和1p的操作。 换句话说，我们不单独地推理从节点开始的子路径，而是将这些子路径作为概率分布进行联合分析。如果一个节点有两个输出的概率选择超边，它代表两个D. Wang等人/理论计算机科学电子笔记347（2019）303305→→·当我们开发低层语义时，一些关于非确定性的高层决策选择出现了从两个角度来看，非确定性本身是一个重要的特征：（i）它自然地产生于概率模型，例如MDP的代理 [6]，或用于建模容错的未知输入分布[40]，以及（ii）它是抽象和细化1的常见范式所要求的。在节目[19，48]。虽然非确定性在标准编程语言中已经得到了很好的研究，但概率和非确定性的结合却很棘手。一个实质性的问题是非决定论何时被解决。概率规划中的非确定性的一个研究得很好的模型是在非确定性之前解决程序输入[18，50，47，51，48，62]。该模型遵循语义研究的常见原则，将非确定性函数表示为将输入映射到可能输出的集合的集值函数，即，X中的一个元素，其中X是程序状态空间，X（）是幂集运算符。 然而，有时期望在程序输入之前解决非确定性，即，一个不确定的程序应该表示一个在xD（X X）中的元素集合。例如，人们可能想证明，对于一个非确定性程序的每个细化版本，每个非确定性选择都被一个条件替换，它在所有输入上的行为都是不可区分的。我们把共同模型称为非决定论-最后一个，而把另一个非决定论-第一个。在§4中，我们首先提出了一个关于非决定论的域理论研究。从技术上讲，我们提出了广义凸性（简称g-凸性）的概念，它表示一组状态转换器在精化下是稳定的（而标准凸性描述了一组状态在精化下是稳定的），以及设计一个g-凸幂域来表征可表达的语义对象。为了实现我们发展指称语义的最终目标，我们不局限于一个特定的非确定性模型，而是在§5中提出了一个通用的代数指称语义，它可以用非确定性的不同处理来实例化。语义是代数的，它在程序状态和状态转换器的空间中进行推理，而转换器应该遵守一些代数定律。例如，程序命令skip应该被解释为程序状态转换器代数中用于排序的身份元素。此外，代数方法是一个很好的适合静态分析的概率程序。在§6中，我们勾画了一个在同伴论文[64]中提出的静态分析框架，作为指称语义学的应用。本文所采用的代数方法在概率规划的背景下是具有挑战性的。相比之下，对于标准的、非概率性的编程语言来说，一旦手头有了结构良好的程序的语义，那么推导出一个低级指称语义几乎是微不足道的。 诀窍是首先将语义运算定义为Kleene代数[41，16，42，45]，它允许扩展操作，用于排序，组合操作，用于分支，以及闭包操作，用于循环;然后从CFG中提取正则表达式通过Tarjan的路径表达式算法捕获所有执行路径1抽象使推理程序通过其高层次的规格，和细化允许逐步的软件开发，其中程序是“细化”从规格到低层次的实现。306D. Wang等人/理论计算机科学电子笔记347（2019）303if*then if prob（1 /2）thent：= 0else t：=1<$else if prob（1/3）thent：= 0else t：=1<$Fig. 1.一个不确定的概率程序最后使用Kleene代数重新解释正则表达式，以获得CFG的语义。然而，当概率和非决定论同时出现时，这种方法就失败了。考虑图1中带有非确定性选择的概率规划。该程序的目的是从一个公平的硬币随机数或有偏见的一个随机值t。如果采用路径表达式方法，则最终得到描述四个程序执行的单个集合的正则表达式：（i）t：= 0，概率为1/2，（ii）t：= 1，概率为1/2，(iii)t：= 0，概率为1/3，以及（iv）t：= 1，概率为2/3。该系列没有描述预期的含义，甚至没有形成一个明确的概率分布-所有概率之和为2而不是1。直觉上，路径表达式方法对于概率程序是失败的，因为它只能将语义表达为具有概率的执行的集合，而概率程序实际上指定了执行上的分布虽然本文提出的指称语义支持有趣的功能，包括非结构化的控制流，一般递归，和非确定性，还有一些其他重要的功能，语义不支持，如连续分布和高阶函数。我们将在第7节中讨论这些缺失的特性，并将它们留给未来的工作。2一种低层概率程序的操作语义在本节中，我们将按照Borgström等人的方法，为一个命令式、单过程、确定性、2概率编程语言勾画一个操作语义。的基于分布的语义[8]。我们使用操作语义来（i）说明如何在操作上对概率程序的执行进行建模，(ii)在后面的章节中证明指称语义学的发展是正确的。2.1超图程序模型我们定义了程序CFHG上的操作语义。我们采用标准CFG的常见方法，其中节点表示程序位置，用指令标记的边描述程序位置之间的转换（例如，[24、54、46]）。而不是标准的有向图，我们使用超图[27]。定义2.1超图H是一个四重图V，E，v入口，v出口，其中V是一个有限的节点集，E是一个超边集，v入口∈V是一个区别入口[2]“确定性”一词D. Wang等人/理论计算机科学电子笔记347（2019）303307∈⟨⟩⟨ ⟩ ∈⊆∈≤ ≤∈∈∈≤ ≤def我我1I n行为和确定性条件节点，vexitV是一个可区分的出口节点。 超边是一个有序对x，Y，其中xV是一个节点，YV是一个有序的、非空的节点集合。对于超边e=x，Y在E中，我们用src（e）表示x，用Dst（e）表示Y.根据图中的术语，我们说e是x的输出边和每个节点y Y的输入边。我们假设ventry没有传入边，vexit没有传出边。定 义 2.2一个概率规划包含一个有限的过程集{Hi}1≤i≤n，其中每个过程Hi=<$Vi，Ei，v进入，v退出<$是一个控制流超图（CFHG）其中除了v_exit之外每个节点具有至少一个外出超边，并且v_exit具有我没有外发的高压线。定义Vd=ef程序对数据动作取模我第五章 赋予概率可概率地，我们将具有以下三种形式之一的控制流动作Ctrl（e）与每个超边eE=1inEi相关联：Ctrl：：=seq[act]，其中 act∈ Act|cond[]，其中∈Cond| 调用[i→j]，其中1≤i，j≤n其中目的节点的数量|Dst（e）|如 果 Ctrl （e）为，则超边e的值为1，seq[act]或call[i→j]，否则为2。例2.3图2（b）显示了图2（a）中程序的CFHG，其中v0是入口，v4是出口。超边v2，{v3}与排序动作seq[n：=n+1]相关联，而v1，{v2，v4}被分配确定性选择动作cond[prob（0. 5）双探针（0. 5）]，即，两枚硬币同时露出正面的事件请注意，break、continue（以及goto）不是数据操作，而是以标准方式直接编码为CFHG中的边下面的语法定义数据动作Act和可用于算术程序的确定性条件Cond，其中p∈[0，1]，c∈Q，a，b∈Z，n∈N.Act：：= x：= e |x x D|观察|skip ∈ Cond：：= T |¬ϕ |ϕ1∧ ϕ2|e1≤ e2|概率e∈ Exp：：=x|C|e1+e2|e1× e2D ∈ Dist：：= Binomial（n，p）|制服（a，b）|几何（p）|···Dist代表离散概率分布的集合。例如，Binomial（n，p）（nN andp[0，1]）描述了n个独立实验中成功次数的分布，每个实验的成功概率为p;Uniform（a，b）表示[a，b]<$Z上的离散均匀分布2.2一种基于分布的小步操作语义下一步是定义基于CFHG的语义。我们采用Borgström等人的方法。的基于分布的小步操作语义lambda演算[8]到我们的超图设置，而我们现在抑制多过程和非确定性的功能。使用三个组件来定义语义：• 一个p_r_g_am状态s_p_ac_e_Ω，例如，对于算术程序，我们可以定义Ω=Var-finQ，即，从程序变量到其值的一组有限部分映射。308D. Wang等人/理论计算机科学电子笔记347（2019）303prob（0. 5）双探针（0.5）真实v1vn：=n+ 1真v42v3n≥10假（Ⅲ）动作Δ：Ω→[0，1]（3）∈（Ⅲ）（2）∧⟨⟩• 一个[0，1]-值函数（<$1），来自每个确定性条件的程序状态（ω）是条件在状态ω∈Ω中成立的概率。- 是的直ϕn：= 0;而prob（0. 5）双探针（0. 5）做n：= n+ 1;如果n≥10，则中断，否则继续od（一）假n：= 0（b）第（1）款图二、（a）概率程序的一个例子;（b）相应的CFHG• 从程序状态到每个数据动作的程序状态（子概率）分布的函数动作。 分布是一个函数，使得ωΩΔ（ω）≤1。 直觉上，act（ω）（ωJ）是动作act在状态ω ∈ Ω开始，在状态ωJ∈ Ω停止的概率[44]。点分布δ（ω）定义为λωJ。[ω=ωJ]其中[ωj]是一个艾弗森括号，如果ω j为真，则计算为1，否则为0。 如果Δ是一个分布且r∈[0，1]，我们将分布λω写成r·Δ.r·Δ（ω）。若Δ1，Δ2是分布，且r1，r2∈[0，1]满足r1+r2≤1，则对于分布λω.r1·Δ1（ω）+r2·Δ（ω），我们记为r1·Δ1+r2·Δ2.图3显示了对§2.1中给出的数据动作和确定性条件的解释，其中ω（e）在状态ω中计算表达式e，[x<$→v]ω用v更新ω中的x，ΔD：Q→[0，1]是分布D的概率质量函数。如果如果n不包含任何概率选择prob（p），则n（ω）是0或1。直觉，（ω）是在状态ω，w.r.t.中为真的概率。一个概率空间，由所有的prob（p）在然后，定义了概率为1.1.1.2，作为个体概率的乘积，因为101和102被解释为w.r.t.概率选择分别在101和102中，这两组选择是不相交的，因此是独立的。设P=V，E，ventry，vexit是一个单过程确定性程序。因此，P中除了vexit之外的每个节点都只与一条超边相关联。程序配置T=V×Ω是形式为ωv，ωω v的对，其中v∈V是av0D. Wang等人/理论计算机科学电子笔记347（2019）303309（Ⅲ）（2）⟨ ⟩ −→ ⟨⟩Σ观察（θ））= λω。 δ（ω）（1）λ ω = λω。v∈supp（ΔD）ΔD（v）·δ（[x <$→ v]ω）<$prob（p））=λω.p<$x：=e）=λω.δ（[x<$→ω（e）]ω）<$skip）=λω.δ（ω）defdefdefΣ<$T）=λω。1defdefdef（λω）=λω。）（ω）·）（ω）（e≤e）=λω。[ω（e）≤ω（e）]1 2（1）=λω。1−<$）（ω）def12defdef1 2 1 2图3.第三章。数据操作和确定性条件的解释节点，并且ω∈Ω是程序状态。我们将一步评估定义为配置之间的关系Δv，ωv −→Δ图4所示为构型上的ωv、ωv和分布Δ。λv，ω−→λv′，ω′。[v′=u] ·act（ω）（ω′）其中e=v，{u} ∈E，Ctrl（e）=seq[act]v，ω当e ree=nv，{u1，u2} n∈E，Ctrl（e）=cond[n]时见图4。 一步求值关系例2.4对于图2中的程序，一些一步求值是：233} −→δ（v1，{n<$→0}），v1，{n<$→1} −→0. 25·δ（δv2，{n<$→1} δ）+ 0.75·δ（n=4，{n<$→1} n）和n=3，n<$→9n −→δ（n=1，{n<$→9} n）。我们现在将步索引求值定义为n-索引关系族v，ωnΔ之间的配置v，ω和分布Δ的程序状态归纳，如图所示。五 、ω v，ω ω −→0λω′。0如果n >0，则ωε−→nδ（ω）ωv，ωn−→n+1τ∈supp（Δ）Δ（τ）·Δ′τ其中，对于任意τ∈supp（Δ），ωv，ωv −→Δ和τ−→nΔ′τ图五. 阶标求值关系例2.5对于图2中的程序，一些步骤索引的求值是n=4，{n<$→10} −→1δ（{n <$→ 10}），v1，{n <$→ 0} −→20. 75·δ（{n<$→0}），且δv1，{n<$→0} δ −→50。75·δ（{n<$→0}）+ 0. 1875·δ（{n<$→1}）。def对于程序P=V，E，ventry，vexit，我们定义它的语义（P）os（ω）=super n∈N {Δ |v项，ω例2.6对于图2中的程序P，2，P（ω）对于任意初始状态ω，109k（Ⅲ）骨n∈dom（ω）由下式给出：δ（[ n<$→10] ω）。k=0（0. 75× 0。25）·δ（[n <$→ k]ω）+0.00000095367431640625·2.3为什么指称语义学是可取的？我们已经展示了概率程序是如何在操作上执行的。正如第1节所提到的，我们对310D. Wang等人/理论计算机科学电子笔记347（2019）303开发指称语义学感兴趣，它集中于程序的效果，并从程序如何执行中抽象出来。指称语义的这种特征确实有利于严格的D. Wang等人/理论计算机科学电子笔记347（2019）303311（）（）（）◦（Ⅲ））¢调用Q; C2ds关于堆栈的信息。C2DS网络QDS¢关于程序的推理，例如静态分析和模型检查，因为人们通常只关心程序是否满足某些属性，例如，如果它们终止于所有可能的输入。更好的是，指称语义通常是组合的--也就是说，整个程序的属性可以从其适当成分的属性中建立。换句话说，人们可以开发基于指称语义的局部--从而可扩展--推理技术。相比之下，§2.2中的操作语义不是组合的，它考虑了整个程序P定义P（Ⅲ）骨指称语义的另一个好处是它通常更容易扩展而不是一个操作。在本节的其余部分，我们将简要比较向操作语义和指称语义添加过程调用和非确定性的复杂性。为了在§2.2中提出的语义中支持多个过程和过程调用，需要引入堆栈的概念来跟踪的过程调用，如[22，23，55]。 然后，程序配置变成调用堆栈、控制流图节点和程序状态的三元组。因此，图1和图2中的一步和一步索引评价关系被简化。4和5将变得更加复杂。然而，这样的扩展几乎是微不足道的指称语义。假设我们能够组合语义对象，例如C1;C2ds=C2ds<$C1ds，其中C1，C2是程序片段，表示组合操作，Cds给出C的表示。如果C1确实是一个过程调用，则调用Q，其中Q是一个过程，因为我们可以得到Q的表示Q，我们可以解释仅作为）（（Ⅱ）DS另一个重要的编程特性是非确定性。对于概率程序的操作语义，非确定性通常使用调度器的概念来形式化，调度器从导致它的计算中解析非确定性选择[25、14、15]）。当调度器固定时，程序可以确定性地执行（如§2.2所示）。为了推理关于操作语义的非确定性程序，需要考虑所有可能的解释器。然而，如果一个人只关心程序的效果，那么就有可能通过切换到指称的方法来避开这些限制。语义例如，设C，C是两个程序片段，C，C是12¢最后的国家。 那么外延否则Cfi 如果 *然后C1）dsⅣ2）ds之间选择1 2）ds. 注意C1C2可以是λω。<$C1）ds（ω）<$C2）ds（ω）这种方法不需要明确地考虑干扰因素。3现有领域理论发展综述我们对非确定性模型的发展极大地利用了现有的关于幂域的域理论研究，因此在本节中，我们给出了一个简短的总结。其中我们回顾了来自域理论[33，1，49]的一些标准概念，以及关于概率幂域[36，35]和非确定性幂域的一些结果. 通过这种方式，我们不需要推理它们的外延，应该是从初始状态到可能的.一个不确定的-312D. Wang等人/理论计算机科学电子笔记347（2019）303→←→.ADf：D → EDE→...∈±±⊥→↑∈↑{∈|∃ <$±}↓\OC\↑↑C cCdef主电源[18，50，47，51，48，62]。3.1Domain Theory的背景设 P 是 具 有 偏 序 ± 的 非 空 集 ， 即 ， 偏 序 集 子 集 A 的 下 闭 包 定 义 为↓A={x∈P|a∈A：x±a}。子集A的上闭包定义为Ad=ef XP一A：aX. 一个子集A满足A=A称为低集。 一个子集A满足A=A称为上集。 如果所有P的元素在单个元素x之上P，则x称为最小元素，通常表示为。在两个偏序集P和Q之间的函数f：P Q是单调的，如果对所有x，y P，使得xy，我们有f（x）f（y）。P的子集A是有向的，如果它是非空的，并且A中的每对元素在A中有上界。如果A是全序的且同构于自然数，则A称为ω-链。如果一个有向集A有一个上确界，则它被记为↑A。偏序集D称为有向完备集或dcpo，如果D的每个有向子集A都有一个上确界↑在. 一个在两个dcpos和之间的函数是Scott连续的，如果它是单调的并且保持有向上确界，即， f（↑A）= ↑f（A）对于D的所有有向子集A。设D为dcpo。对于D的两个元素x，y，我们说x逼近y，记为yxy，如果D的所有有向子集sA，w∈y±。↑A蕴涵x±adef def对于a∈A。 我们定义A={x∈D|A∈A：xa}和A={x∈ D|a∈A：ax}。 dcpoD称为连续的，如果存在D的子集B使得对于D的每个元素x，集合B称为D的基。x∈B是有向的，且x=。杨晓（xB）。设D为dcpo。一个子集A是Scott-闭的，如果A是一个下集并且在有向上确界下闭。一个Scott闭子集A的补集D A称为Scott开子集。这些Scott-开子集构成D上的Scott-拓扑。子集A的闭包是包含A作为子集的最小Scott-闭集，记为A。设X是一个拓扑空间，其开集记为（X）。的盖X的子集A的集合是其并集包含A作为子集的子集的集合。的子封面的子集它仍然覆盖A。 盖称为开覆盖，如果它的每个成员都是开集。 一个子集A是紧的，如果A的每个开覆盖包含一个有限子覆盖。一个子集A是饱和的，如果A是它的邻域的交集。子集A的饱和度是其邻域的交集。 在具有Scott拓扑的dcpo中dcpoD上的Lawson-拓扑由Scott-开集和Dx形式的集生成。透镜是一个非空子集，它是一个Scott闭子集和一个Scott紧子集的交集饱和子集透镜总是劳森闭集。一个连续dcpoD称为相干的，如果任何两个Scott紧饱和子集的交集也是Scott紧的。凝聚dcpo上的Lawson拓扑是紧的。我们将在技术开发中使用以下定理命题3.1（Kleene不动点定理）设f：D →D是一个Scott连续函数，且f：D→ D是一个最小元为f的dcpo。 那么f有一个D. Wang等人/理论计算机科学电子笔记347（2019）303313⊥--∈IXD（X）Σ∈^→Di=1⊕∈0i=1Dd=efλx。0。再来一点，最小不动点是f的递增Kleene链的上确界（即，的ω-链± f（）± f（f（））±···± fn（）±···），记为lfp±f。第3.2章（一）[33，Hofmann-Mislove theorem]）设X是sober空间，即，一个T0-空间，其中每个非空闭集要么是一个点的闭包，要么是两个真闭子集的并集。一个过滤族A ii∈I（即，任何两个子集的交都在族中）的紧饱和子集是紧的且非空的。 如果这样一个过滤交包含在一个开集U中，则对于某个i，Ai U。具体地说，配备斯科特拓扑的连续dcpos和配备劳森拓扑的相干dcpos是清醒的。3.2可能的PowerdomainsJones等人在概率幂域[36，35]上的开创性工作扩展了计算机科学中广泛使用的完全偏序集，以模拟概率计算。设X是一个非空可数集。上的所有分布的集合表示为，即，一个概率功率域。回想一下，X上的分布是一个函数Δ：X→[0，1]，使得x XΔ（x）≤1，并且对于某个x ∈ X，点分布δ（x）定义为λxJ。[x = xJ]。分布def是逐点排序的，即，Δ1±DΔ2=Δx∈X：Δ1（x）≤Δ2（x）。我们定义了概率选择分布Δ1，Δ2相对于权重p∈[0，1]，写作Δ1p<$Δ2，表示为p·Δ1+（1−p）·Δ2。下面的定理提供了概率幂域的特征命题3.3（[36，35，47，62]）偏序集<$D（X），±D <$构成一个凝聚dcpo具有可数基{nri·δ（x i）|n∈N <$r i∈Q +<$$>n r i≤1<$x i∈X}。它命题3.4（[35，62]）每个函数f：X（X）都可以提升为唯一的Scott连续线性映射f：D（X）→D（X）。3.3非确定性Powerdomains当非确定性进入画面时，正如我们在第1节中讨论的那样，现有的研究通常在非确定性之前解决程序输入[37，18，50，47，51，48，62]。在§1，我们称这样的模型为nondeterminism-last，它解释了非确定性作为从输入到输出集合的映射。设X是一个非空可数集。D（X）的子集A称为凸的，如果对所有Δ1，Δ2∈A和所有p∈[0，1]，我们有Δ1pΔ2A.任意子集A的凸包是包含A作为子集的最小凸集，记为conv（A）。凸性条件确保了从编程的角度来看，不确定性选择总是可以用概率性选择来定义。概率幂域D（X）上的凸幂域PD（X）然后被定义为D（X）中的凸透镜，其中允许最小元素p∈ [0，1]是Scott连续的。314D. Wang等人/理论计算机科学电子笔记347（2019）303P··↑{··|{\fn黑体\fs22\bord1\shad0\3aHBE\4aH00\fscx67\fscy110 }^^您的位→ PD→DDDdefEgli-Milner序A±PB=A<$<$B <$$>↑A<$B。下面的定理提供了凸幂域的特征命题3.5（[47，62]）偏序集<$P D（X），± P<$构成一个凝聚的dcpo。它-mitsaleastelement最后一个元素 {\fnSimHei\bord1\shad1\pos（200，288）}对于r1，r2∈[0，1]，满足r1+r2≤1，we定义r1A+r2Bd=efCC，其中reC为r1Δ1+r2Δ2Δ1AΔ2B。然后，概率选择操作被提升为Scott连续操作，defAp<$P B = p·A+（1 − p）·B。此外，它带有一个Scott-连续半格def运算，称为形式并集，定义为A−PB=C↑C，其中C是conv（AB）。直观地说，形式上的联合运算代表了不确定的选择。命题3.6（[62]）每个函数g：X（X）可以提升到唯一的Scott-连续线性映射g：PD（X）→ PD（X）保持形式并。例3.7考虑下面的程序P，其中*可以用任何涉及程序变量t的确定性条件来定义：if*then t：= t+1else t：= t−1fi我们想从X→PD（X）中给它分配一个语义对象，其中状态空间X=Q表示t的值。固定输入t∈Q。数据操作t：=t+1和t：=t−1然后分别将输入到幂域PD（Q）中的单例{δ（t+ 1）}和{δ（t−1）}。 因此，非决定性选择被解释为{δ（t+1）}−P−P{δ（t−1）}，其中h为{r·δ（t+1） +（1−r）·δ（t−1）|r∈[0，1]}，对于a给定t∈Q。4不确定性-第一在本节中，我们开发了一种新的非确定性模型--非确定性第一方法，它以域理论的方式在程序输入之前解决了非确定性选择。这个模型的灵感来自于对程序在不同输入上的行为的推理的元素）而不是集值映射（即，X→X（X）的元素）。如本节所示，对于非确定性-first，t：=t+1和t：=t−1分别被赋予语义对象{λt.δ（t+1）}和{λt.δ（t−1）}本文首先引入核函数，然后提出一个新的广义凸性概念（简称g-凸性），并最终为非决定论开发一个幂域4.1次概率核设X是一个非空可数集。函数κ：X（X）称为（子概率）核。直观地说，内核将输入状态映射到输出状态。 所有子核的集合表示为yK（X）d=efX→D（X）。内核def是逐点排序的，即， κ1±Kκ2= κx ∈ X：κ1（x）±κ2（x）。D. Wang等人/理论计算机科学电子笔记347（2019）303315K±φKi=1且若φ∞可 测，则φ∞包含在.i=1n∈Ni=112x′∈X12D定理4.1偏序集（X），最少的元素。K形成相干的dcpo，d=efλx。拉瓜斯设W（X）d=fX→[0，1]是从X到i_n[0，1]的函数集.我们把y≤tec表示为逐点比较，把yrtec表示为常数函数任意r∈[0，1]。如果κ是一个核且φ∈ W（X），我们将核λx写成φ · κ.φ（x）·κ（x）。 如果κ1，κ2是k核，且φ1，φ2∈W（X）满足φ1+φ2≤stec1s t e c，则对核λx记为φ1·κ1+ φ2·κ2，φ1（x）·κ1（x）+ φ2（x）·κ2（x）. 更一般地说，如果{κi}i∈N+是核序列，{φi}i∈N+是W（X）suchthesouth φi≤stec1s t e c，我们写为φ∞ φi·κi表示内核。↑nφi·κi。然后我们定作为κ1函数φ∈W（X）上核函数κ1，κ2的条件选择Qκ2d=efφ·κ1+（1stec−φ）·κ2。我们将k核κ1、κ2的位置定义为：定义κκ = λx.λxJJ。κ（x）（xJ）·κ（xJ）（xJJ）。引理4.2（i）条件选择运算φQ对所有的φ∈ W（X）.(ii) 复合运算是Scott连续的。4.2广义凸性如第3.3节所示，非确定性-last被分布的凸集捕获。然而，需要一个更复杂的凸性概念来开发内核上的非确定性第一语义。设X是一个非空可数集。对于每个函数φ∈W（X），每个语义对象都应该在条件选择φQ下是封闭的。回想一下，定义κ1Qκ2d=efφ·κ1+（1stec−φ）·κ2类似于一个常数vex组合，不同之处在于系数不仅可以是常数，而且还可以取决于状态。我们通过定义g-凸性的概念来形式化这个想法。定义4.3K（X）的子集A称为g-凸的，如果对所有序列{κi}i∈N+εA{φi}i∈N+<$W（X）i=1φi=1i=1φi·κiA现在我们证明了某些Domain理论运算保持g-凸性。引理4.4设A是K（X）的g-凸子集。 然后(i) 饱和度↑ A和下闭包↓ A是g-凸的。(ii) 闭包A是g-凸的。（X）的子集A的g-凸包是包含A作为子集的最小g-凸集，记为gconv（A）。直观地说，gconv（A）丰富了A，使之成为一个在任意条件选择下封闭的合理语义对象。下面是gconv（·）运算符的一些属性引理4.5假设A和B是K（X）的g-凸子集。 则{κ φQ ρ|对于所有函数φ ∈ W（X），κ∈A<$ρ∈B}是g-凸的.推论4.6如果A和B是g-凸的，则gconv（A <$B）由{κ 1φQ κ 2|φ316D. Wang等人/理论计算机科学电子笔记347（2019）303κ1∈ A <$κ2∈ B <$φ∈ W（X）}.D. Wang等人/理论计算机科学电子笔记347（2019）303317{\fn黑体\fs19\bord1\shad1\1cHD8AFAF\4cHC08000\b0}我们知道，∞. ΣKK{|∈}K≤∪≤∪我我我i∈N+我i∈N+我i=1i=1证据可以直接证明gconv（A<$B）是{κ1φQκ2} 的 超集|κ1一κ2BφW（X）。 然后证明了这个集合确实是g-凸的。我们总结了Lem的证明。四点五Q对于K（X）的有限子集F，作为Cor的直接推论4.6、简单的gconv（F）={κFφ κ·κ| {φ κ}κ∈F<$W（X）<$κFφ κ=1s t e c}。引理4.7对于任意的A K（X），我们有gconv（A）=. Σ∞φ·κ|{κ}A{φ}W（X）φ=1秒。引理4.8（i）对于任意的A∈ K（X），我们有gconv（A）=gconv A。（ii）若{Ai}i∈I是K（X）的Scott闭d个子集按集合包含序的有向集合，则gconv（Ai）=gconv（Ai）.引理4.9设A和B是K （ X ） 的 Scott紧g-凸子集。然后gconv（A B）也是Scott-紧凑的。现在我们来讨论g-凸性的一些分离性质引理4.10（i）如果A （X）是g-凸的，则对所有x， κ（x）κA是凸的。(ii) 如果A κ K（X）是Scott-紧的，则对所有x，{κ（x）|κ ∈ A}是Scott-紧的。(iii) 如果A κ K（X）是Scott闭的，则对所有x，{κ（x）|k ∈ A}是Scott闭的。引理4.11让我们考虑（X）的子集。设K是Scott紧g-凸集，A是与K不相交的非空Scott闭g-凸集.然后它们可以被g-凸Scott-开集分离，即，存在一个g-凸Scott-开集V，V包含K且与A不相交。引理4.12如果K（X）非空且是Scott紧的，则gconv（K）是Scott紧的。4.3不确定性优先的g-凸幂域从文献中，Plotkin定理[1]由一个二元运算−−定义，称为形式unio n，并且如下：（i）A−B=B−A，（ii）（A−B）−C=A−−（B−C），和（iii）A−A=A，对于po w erdomain中的所有o bA，B，C。因此，形式上的联合−n−表示非确定性选择。更进一步，形式并导出一个半格序：A B如果A−−B=B。从Domain理论的角度来看，半格序通常是不有趣的，然而，它是有趣的。描述条件选择和非确定性选择之间的关系的工具-A φQ B A−−B对于所有语义对象A，B-非确定性选择应该抽象一个任意的（可能是概率性的）条件选择。设X是一个非空可数集。由于非确定性-first将程序解释为输入-输出转换器的集合，我们希望在318D. Wang等人/理论计算机科学电子笔记347（2019）303⊗defG GK−K（X），即，X上的核为了实现这个目标，我们需要（i）识别一个在K（K（X））中的格式良好的语义对象的集合，它允许上面描述的形式并运算，（ii）将条件选择φQ和核上的组合正确地提升到幂域，以及（iii）证明幂域是dcpo并且运算是Scott连续的。受凸幂域研究的启发[1，47，62]，我们从以下集合开始G K（X）={S<$K（X）|非空g-凸透镜是K（X）中按Egli-Miler阶A±G排序的所有g-凸透镜的集合Bd=efA↓B↑AB. 我们称GK（X）为X上核上的g-凸幂域。下面的定理建立了g-凸幂域的特征定理4.13<$GK（X），±<$G构成一个dcpo，其中最后一个元素为<$Gd=ef{0}。现在我们将条件选择φQ（其中φ∈W（X））和核的复合矩阵提升到幂域GK（X），如下所示。defAφQG B ={a φQ b |a ∈ A <$b ∈ B}<$↑{a φQ b |a ∈ A<$b ∈ B}defAGB = gconv（{a b |a ∈ A <$b ∈ B}）<$↑ gconv（{a <$b |a ∈ A <$b ∈ B}）这些操作通过引理4.4和4.12构造非空g-凸透镜。由于条件选择和组合操作在内核上是斯科特连续的，因此提升操作在幂域中也是斯科特连续的。引理4.14对于所有φ ∈ W（X），运算φQG和φG是Scott连续的。最后，我们定义了一个正式的工会操作−G在Prop。3.5至Interpretdef非确定性-c选择为A−G−GB=C <$↑C，其中C是gconv（A<$B）。引理4.15形式并− G −G是上的Scott-C连续半线性算子G K（X）.例4.16回想一下例4.16中的概率程序P。3.7：if*then t：= t+1else t：= t−1fi状态空间X是Q，并且我们想要表明对于P的任何概率精化Pr（即，*由yprob（ r ）定义），对于t的 输入值st1 ，t2， 我们有Et′1<$Δ1 ， t′2<$Δ2[tJ1-tJ2]=t1t2，其中程序Pr以分布Δ1结束，t=t1和Δ2，其中t=t2。对于非确定性g-凸幂域G K（X）-first，t：= t +1和t：= t − 1分别被赋予语义对象{λt.δ（t +1）}和{λt.δ（t − 1）}。因此，非确定性选择被解释为{λt}的子集。δ（t+1）}−ε−G{λt. δ（t−1）}，即{κ r|r∈[0，1]}，其中κ r=λt.r·δ（t+1）+（1