概率互模拟和非确定性选择的完整操作语义及应用

理论计算机科学电子札记96（2004）7-28www.elsevier.com/locate/entcs概率公理与非决定论公理MichaelMislovea，1和Jo？elOuaknineb，2和JamesWorrella，1a杜兰大学数学系，6823 St Charles Avenue，NewOrleans LA 70118，USAb卡内基梅隆大学计算机科学系，5000 Forbes Avenue，PittsburghPA 15213，USA摘要本文研究了一个简单的微积分有限状态过程具有不确定性和概率选择。 我们提出了一个域模型和我们的演算的操作语义。 指称模型使用琼斯和普洛特金的概率幂域，结合了普洛特金幂域的几何凸变体。操作模型定义了转换规则，在该规则下，过程转换为状态上的概率分布。 我们证明了一个完整的抽象结果，表明两个进程具有相同的表示，当且仅当它们是概率bisilimited。我们还表明，预期的法律概率和非确定性是健全的和完整的指称模型。关键词：概率互模拟，非确定性选择，Segala-Lynch概率自动机，CCS1介绍到目前为止，有一个完善的子集的并发文学处理的进程代数的功能概率选择，无论是代替，或除了，不确定性的选择。在给这种语言提供操作语义时，不仅必须指定哪些转换是可能的，而且还必须指定它们被采用的概率（参见，例如，[19]）。存在下1感谢美国国家科学基金会和美国海军研究办公室的支持。2感谢ONR合同N 00014 -95-1-0520、国防高级项目研究局和陆军研究办公室根据合同DAAD 19 -01-1-0485提供的支持。1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.04.0198M. Mislove et al. / Electronic Notes in Theoretical Computer Science 96（2004）7-无保护递归的结果簿记变得相当复杂，并且可以说破坏了操作方法的通常优点。另一方面，在领域模型中，许多技术细节可以通过引入一般领域理论的标准构造和结果来隐藏。本文给出了概率进程代数的论域语义。我们使用概率幂域[12]来模拟概率选择，并且我们使用Plotkin幂域的几何凸变体，独立于Mislove [16]和Tix[20]，来模拟非确定性选择。我们还给出了一个操作语义的进程代数，我们表明，我们的域模型是完全抽象的概率双相似性。的依赖于主要的结果的文件，它提出了一套法律的概率和不确定性的选择，是健全的和完整的关于我们的域模型。完备性结果适用于有限状态过程;因此，我们将自己限制在一个具有前缀、概率选择、非确定性选择和递归的过程代数中。然而，对于完整性证明来说，使用域模型比使用操作模型更方便项E和F的不确定性和记为E+F，而对于<0p1，记为p乘以E和1−p乘以F E.我们所描述的模型是非交替的，即只有一种类型的过程，并且可以不受限制地应用运算符+和+p为了适应这两种类型的选择，遵循Segala和Lynch [18]的概率自动机模型，我们将过程的初始能力建模为一组概率分布。不确定性选择的模型为并通过逐点提升概率分布上的自然概率和算子到这些分布的集合来进行概率选择。这最后一种方法需要我们的语义满足以下概率选择优于非确定性选择（E + F）pG =（EpF）+（FpG）。（一）我们对概率选择的解释的另一个结果是，为了确保定律EpE=E成立，我们将过程的初始能力建模为概率分布的几何凸1反过来，这需要以下的凸性法律的不确定性选择E+（EpF）+F = E + F。（二）1一个概率分布集S是几何凸的，如果pσ+（1−p）v∈S，只要σ，v∈S且0≤p≤ 1。稍后，我们也将引入这样的集合的序凸性M. Mislove et al. / Electronic Notes in Theoretical Computer Science 96（2004）7-9因此，E和F的非确定性选择也包括E和F的任何凸组合。在操作上，这对应于Segala和Lynch [18]的想法，即通过随机调度器可以将不确定性选择分解为分配律（1）促进了一种语义，在这种语义中，非确定性选择和概率性选择满足期望律。另一方面，非确定性选择分布在概率性选择之上的双重要求例如，另一个分配律的例子是（E 1F）+（E 1F）= E 1（（E + F）<$2 F）。2 2 4 3在存在这样一个恒等式的情况下，保留+的恒等式似乎是不可取的。特别是，这意味着简单的五五选择E1F等于E、F和E+F的各种加权组合。2二元分配律往往出现在那些模型中，哲学是概率选择应该在非决定性选择之前解决这些模型的例子可以在[13，17]中找到。类似地，分配律（1）意味着，在我们的模型中，非确定性选择被分解为概率性选择。1.1相关工作Stark和Smolka [19]和Baeten等人[4]给出了具有概率选择但没有非确定性选择的演算的概率双相似性的完整公理化。[19]中的发展密切遵循Milner [15]对有限状态CCS中双相似性方程的处理。我们的完备性证明遵循相同的模式，除了基于操作语义的参数被域理论所取代。在米尔纳[15]和斯塔克和斯莫尔卡[19]之后，我们包括一个唯一的固定点规则（参见。表1中的F4）作为我们的公理化的一部分。这实际上是一个条件方程的图式。 相比之下，概率双相似性的纯等式公理化最近beenobtainedbyyAceto，E′sikanddIngo′lf sd′ottir[2]. 这是一个非常好的解决方案，在迭代理论的基本方程式中加入概率选择公理Bandini和Segala [6]给出了一个代数的强和弱概率双相似性的完备公理化，该代数包括不确定性和概率选择，但不包括递归。他们的表述与我们的表述之间的一个显著区别是，他们对概率选择和非确定性选择的应用引入了句法限制。你比如说10M. Mislove et al. / Electronic Notes in Theoretical Computer Science 96（2004）7-分配律（1）在它们的设定中是病态的Baier和Kwiatkowska [5]从域理论的角度考虑了概率和非确定性的结合。像我们一样，他们通过求解涉及概率幂域的域方程来生成进程代数然而，他们使用Hoare幂域，而不是几何凸Plotkin幂域。此外，他们引入概率通过一个运营商的行动保护概率选择，而不是无限制的概率选择运营商，我们的模型。最后，他们不公理化他们的语义。Varacca [21]研究了一种完全不同的方法来模拟域理论中的概率和非确定性。他使用一个指数估值单子来模拟概率选择。这种结构比通常的概率幂域（这是一个商）更严格，它支持Hoare幂域上的分类分配律。利用这一分布定律，他定义了一个概率性和非确定性选择的组合单子。然而，相应的等式理论不包括定律EpE=E.Andova [3]考虑将概率选择添加到代数ACP中，de Bakker和他的学生广泛研究了这一点。 Andova工作中的关键问题最后，论文den Hartog [11]提出了一个广泛的考虑之间的相互作用的不确定性和概率的选择，称为本地和全球，并对应于内部和外部的选择操作。2概率微积分我们首先介绍概率表达式的微积分PE。这是[19]的语言，增加了一个不确定的和运算符。体育术语的语法如下。E：：= X|0|AE|E + E|EpE|µXE其中a∈Act且0

p}其中0≤p≤ 1，U∈D是Scott开的。每个元素x∈D产生一个赋值δx，定义为δx（U）= 1，如果x∈U，且δx（U）=0。一个简单的赋值有公式a∈Araδa关于简单赋值的一个中心结果是分裂引理;这将用于证明我们的方程公理化的完备引理3.1（Jones [12]）设σ = a∈Araδa和ν = b∈Bsbδb是D上的单赋值.则σ±ν当且仅当存在一族迁移数{ta，b|a ∈ A，b ∈ B}<$[0，1]满足• 对于acha∈A，b∈Bta，b=ra，• 对于每个b∈B，a∈Ata，b=sb，• ta，b= 0表示a± b。3.2Powerdomain中的几何凸图设D是一个相干域。如果L是非空的，在Lawson拓扑中是紧的，并且是序凸的，我们说LD是透镜，即，L=↑L↓L。我们让PD表示所有这样的透镜连同空集的集合，并且我们用X或Y表示Pow（D）的典型元素。集合PD变成了14M. Mislove et al. / Electronic Notes in Theoretical Computer Science 96（2004）7-相干域时，配备了Egli-Milner顺序。 它的定义是：L±LJi <$L<$<$LJ和↑LJ<$↑L对于透镜L和LJ，以及{λ}± λ。PD上的Scott拓扑可以直接用D上的Scott拓扑来描述，使用“may”和“must”模态。 次基本开放是集oU ={X ∈ P D |X U}U ={X∈P D|X U}其中UD是Scott Open。我们的概率和非确定性选择模型是PVD的一个收缩。 为了定义这个，我们首先需要回忆序凸闭包和几何凸闭包的概念。 给定一个Lawson紧集S<$VD，S的序凸闭包定义为↑S<$<$S。S的几何凸闭包定义为{pσ +（1−p）v：σ，v∈S，0≤p≤1}。一个重要的事实是，这两个闭包算子都保持劳森紧性。我们现在定义复合闭包运算符−设λXλ是X的几何凸闭包的序凸闭包。（注意几何凸集的序凸闭包仍然是几何凸的则Pw − Pw是一个Scott连续幂等映射，它的像，我们记为Pow（D），恰好是PVD的几何凸元素的集合。因此，Pow（D）是PVD的收缩，因此是继承顺序中的相干域我们可以为Pow（D）配备概率和非确定性和的运算如下。给定Pow（D）中的S和SJ，不确定性和X+Y定义为：X + Y=XY概率和XpY定义为：X<$pY =<${pσ +（1 − p）ν：σ∈ S，ν ∈ SJ}<$。给定一个有限集合F ={ν1，...，我们定义{|v1，...，νn|}是由L生成的Pow（D）的元素，即，{|v1，... ，νn|}= ↑ F ↓ F。M. Mislove et al. / Electronic Notes in Theoretical Computer Science 96（2004）7-15a∈ActD而不是A是对A，D，根据标准论证，+和p作为从Pow（D）×Pow（D）到Pow（D）的映射都是Scott连续的。我们还注意到，对于透镜L和LJ，当p趋于1时，LpLJ收敛于L，当p趋于0时，L p L j收敛于LJ 最后，我们注意到分配律（1）在Pow（D）中成立，主要是因为Pow（D）上的概率选择运算是逐点定义的。我们指读者可以参考Mislove [16]和Tix [20]，以进一步解释这些观点。3.3分离和我们使用的关于域的其余构造是分离和。让行动成为一组有限的行动，我们一劳永逸地固定下来。给定一个整环D，对于D与其自身的积，记a∈ A tD，并有一个新的底其中a∈Act，d∈D，且a=aj，d∈ ±d ∈J，d∈a，d∈J，d∈I.4域模型为了找到PE的域模型，我们求解Abramsky域方程的概率版本更确切地说，我们构造了一个域D，01-02a∈Act D）的情况。（五）一般域理论[10]告诉我们，我们不仅可以找到这样一个域，而且存在一个规范的这样的选择-所谓的最小不变量。 我们认为这个域是一个通用的Segala-Lynch概率自动机[18]。根据这种直觉，如果ν∈ι（d），那么我们写d→ν-读d有能力ν。下面我们展示如何在域D中解释进程代数PE的项。项E相对于环境ρ（将变量映射到D的元素）的语义表示为[[[E]]ρ。递归是用最小固定点的标准方法处理的在语义映射的以下定义中，我们省略了符号的同构i：D→Pow（a∈ActD）。透明度[[0]]ρ=0[[aE]] ρ={|δα，[[E]]ρα|}[[E+F]]ρ=[[E]]ρ+[[F]]ρ[[EpF]]ρ=[[E]]ρp[[F]]ρ[[µXE]] ρ = µθ [[E]]（ρ [X <$→ θ]）。元素邻接。因此，16M. Mislove et al. / Electronic Notes in Theoretical Computer Science 96（2004）7-这些方程定义了从PE到我们的域模型的组成图D，从而给出了我们的过程演算的指称模型4.1域逻辑接下来，我们引入D的域逻辑L。我们使用这个逻辑作为工具来证明D的一个元素在另一个元素之下。 特别是，它被用于证明下面的一些等式规则的合理性（参见。表1）。该逻辑是基于拓扑描述的各种函子的建设D。为了通过逻辑完全捕获域，还应该给出一个证明系统，用于判断何时两个公式表示相同的开集，参见。Abramsky [1].然而，就我们的目的而言，这是不必要的。在L的文法中，有两种短语类型：状态公式和概率公式。这对应于域方程中的非确定性和概率性选择的交替状态公式表示为用罗马字母和概率公式用希腊字母：（状态公式）f：：= f<$f |f f |♦ϕ|奥里（概率公式）：：= T |⊥ |ϕ ∧ ϕ |ϕ ∨ ϕ |a其中a∈Act，p∈[0， 1]。公式的模态深度定义为：md（o）= md（）= md（）+1md（apf）= md（f）.通常，合取词（析取）的模态深度是合取词（析取）的模态深度我们定义了D的元素与状态公式之间以及V（a∈ActD）的元素与概率公式之间的满足关系di（ν）（d→νν） doi（ν）（d→νν）ν► ⟨a⟩pf iff ν{⟨a, d⟩: d ► f}>p.设d∈D，DJ∈D，如果d ∈ f蕴涵d ∈ f，则d ∈ d，类似地，给定ν，σ∈ V（a∈Act D），我们说ν“n σ，如果ν ∈ σ对e a c h蕴涵s σ ∈ σ，其中m u la ∈ h md（ω）≤ n。利用幂域上拓扑的模态描述和域D的归纳构造，可以证明以下结果。定理m4.1Givend，DJ∈D，d±DJi <$d“ndj，对a l l n ∈ N.换句话说，域逻辑表征域D上的顺序。M. Mislove et al. / Electronic Notes in Theoretical Computer Science 96（2004）7-17˜是Pow的一个元素（a∈ActPE）。 （一）以“为”为核心，以“为”为核心。5操作语义在本节中，我们定义了PE的操作语义。稍后，在第6节中，我们将证明第4节中的域理论语义对于我们下面定义的概率双相似性形式是完全抽象的令PE表示所有PE项的集合，PA表示概率代理的集合，即，封闭的条件。设a∈ActPE表示元素A，E的偏序集，其中a∈Act，E∈ PE是离散序的，且有一个bottom.汤姆元素相邻。PE的操作语义可以看作是表示一个转换关系E→μ，其中E是一个项，μ∈V（a∈ActPE）是一个（必然简单的）赋值。实际上，我们定义了一个函数inits（E），它给出了一个项E的初始行为，即，Inits（E）={µ|E→ μ}。集合inits（E）根据定义是几何凸的由于每个转换E→μ可以看作是由解决E中的不确定性的调度程序引起的，最后一个要求对应于具有概率性调度程序的可能性。正如我们前面所解释的，这个特征对于我们的语义满足概率选择优于非确定性选择的分配律（1）至关重要。它也将是这样的情况，即inits（E）是序凸的;给定定义6.2中提出的互模拟概念，在这种情况下识别具有其序凸闭包的集合正如我们前面提到的，定义PE操作语义的一个复杂因素是无保护递归的存在举个简单的例子对于这种现象，考虑术语P<$µX（（aX<$1X）+bX）。 显然2一个可能的跃迁是P→δδb，Pδ b。 稍微不那么明显的是，另一个可能的转变是P→δα，Pβ。这种转换对应于总是选择递归主体中的左被加数的调度器;在这样的调度器下，保证动作a最终会发生。在纯粹的概率设置中，Stark和Smolka [19]通过分别计算一个项的可能转移和它们发生的概率来处理无保护递归。这些概率被计算为最小固定点。我们的方法在精神上是相似的，但必然更复杂在非决定论面前为了处理无保护递归，我们在操作语义中引入了环境。给定一组变量X={X1，. ，Xn}，环境是一个函数σ：{X1，...，Xn} →Pow（a∈ActPE）给出每个变量Xi的初始跃迁。我们把一个t ∈ E的首字母写为（E，σ），在自由变量X∈E中，它与e∈σ有关;它是归纳：首先通过归纳子项在E18M. Mislove et al. / Electronic Notes in Theoretical Computer Science 96（2004）7-，Pow（PA）PAPow（a∈ActD）、的形式µXF，这是不属于一个prefixing运算符的范围内，然后通过结构归纳E。定义中的条款如下：• Inits（0，σ）=0• inits（X，σ）=σ（X）• inits（aE，σ）={δ<$a，E<$}• inits（E+F，σ）= inits（E，σ）+inits（F，σ）• inits（E<$pF，σ）= inits（E，σ）<$pinits（F，σ）• inits（µXE，σ）=µθ inits（EJ，σ[X<$→θ]），其中EJ通过代入µXE用于E中X的所有受保护出现。最后一个子句说inits（µXE，σ）是方程的最小解θ= inits（EJ，σ[X<$→θ]）在域Pow（a∈ActPE）中。 注意，如果X在E中被保护，则EJ只是E{µXE/X}，所以X在EJ中不会自由出现，给定的固定点一步到位。事实上，这个子句中的固定点只针对变量X的无保护出现。例5.1考虑施事P<$µX（（aX<$1X）+bX）。 初始化（P）2是方程θ = inits（（aP<1 X）+bP，[X <$→θ]）。2这可以构造为以下链的Pow（a∈ActPA{|{\fn黑体\fs22\bord1\shad0\3aHBE\4aH00\fscx67\fscy66\2cHFFFFFF\3cH808080}|，|δb，P，1δa，P+1δ}|，|δb，P，3δa，P+1δ，1δa，P+1δb，P}|，2 2 4 4 2 2whic h isequaltoo{|δa，P，δb，P}|.6全抽象定理6.1表达了用指称模型D_n=P _w定义的操作语义的兼容性（a∈A ctD），来自第4节。 从理论上说，指称映射[[[−]]：PA →D是一个余代数homo-态射，参见[1]的文件。定理6.1下图初始化za∈Act ‘[[−]]、P ow（z，a∈Act[[−]]）DιM. Mislove et al. / Electronic Notes in Theoretical Computer Science 96（2004）7-19证 据 （ 略 ） 证 明 遵 循 初 始 化 （ P ） 定 义 的 归 纳 结 构 。 对 于 prefixing ，nondeterministic choice和prob-probability choice的归纳案例是直接的，并利用了相应在初始化和[[[−]]]的定义中的子句。递归的归纳法依赖于递归的操作和指称语义中相应定点构造之间的兼容性。Q6.1互模拟与模态逻辑我们的概率代理域理论语义对应于一个版本的概率互模拟。具有概率性选择和非确定性选择的代理互模拟的定义出现在[18，13]中。下面的定义略有不同，因为我们考虑了操作语义中的分歧。设R是PA上的关系。我们将R扩展到a∈ActPA上的关系，定义Ea，ER b，Fia =b和ERFRR接下来，我们定义关系对于所有Oa∈ActPA，其中R（O）是O在R下的像.定义6.2我们说PA上的关系R是部分概率互模拟[1]，如果P R Q意味着• P→μ蕴涵（μν）（Q→ν和μ• Q→ν意味着（μμ）（P→μ和μ如果代理P和Q通过部分概率互模拟相关，则我们写P±Q。我们可以使用PE的操作语义来定义概率主体和所引入的逻辑L的公式之间的满足关系 在第4节。事实上，这个定义在句法上几乎与第4节中的相应定义相同。这三个条款是Pi （ v ） （ P→νν ） Poi （ v ）（P→νν）νapf i v{a，P：P f}>p.作为PE的操作语义和指称语义的相容性的推论，如定理6.1中所表示的，我们得到了逻辑L的两种语义之间的关系的以下结果。20M. Mislove et al. / Electronic Notes in Theoretical Computer Science 96（2004）7-推论6.3对于每个概率主体P和L上的公式f，P<$fi <$[[P]] a.证据通过对模态深度f的归纳，采用定理6.1进行归纳步骤。Q下面的结果说，逻辑L表征概率代理到双相似性。它是[13，定理8]的一个微小的变体。定理6.4给定概率主体P和Q，P±Q i <$P<$f意味着对所有公式f ∈ L，Q ∈ f。下面的定理是本节的主要结果。它说，概率代理的域语义是完全抽象的部分概率双相似性。定理6.5给定概率主体P和Q，P ± Q ∈ [[P]] ± [[Q]]。证据P±Qi <$（<$f∈L）（P<$f <$Q<$f） （根据第6.4节）i <$（<$f∈L）（[[P]]<$f<$[[Q]]<$f）（b）在第6卷内。第三章i ∈[[[P]] ± [[Q]]（定理4.1）。Q7方程下表列出了PE项之间的（不）等式。这些将被证明是健全的和完整的关于域模型D。半格方程N_1-方程P1-不确定性选择和概率性选择通过分配律D1和D2相互作用剩下的方程涉及递归。规则F4意味着保护递归有唯一的不动点。（一个变量X在项E中被保护，如果X在E中的每个自由出现都出现在aEJ形式的子项中。）规则F1和F2展示了如何从递归定义中消除无保护变量。我们可以把分配律D1和D2看作是说，在表达式EpF中，E和F的非确定性选择首先被解决，然后概率地组合。特别地，如果F代表空选择，如在D2中，则EpF是惰性的。另一方面，如果我们被引导根据对偶分配律，如[13]，则Ep0表示一个行为像E的主体，其概率为p，行为像0的概率为1−p。我们还注意到M. Mislove et al. / Electronic Notes in Theoretical Computer Science 96（2004）7-21Ω±EN1E+F=F+EN2E+（F+G）=（E+F）+GN3E=E+EN4E+0=EP1E=EEpF=F1−pEEp（FqG）=（EpF）p+q−pqGp+q−pqP2P3D1（E+F）pG=（EpG）+（FpG）D2E=0F1µX（E+X）=µX（E+X）F2µX（（EpX）+F）=µX（E+F）F3µXE=E{µXE/X}F4由E=F{E/X}和F{EJ/X} ±EJ，X在F中被保护，推断E±EJ。Fig. 1. PE项在[5，6]中研究的过程代数中，由于某些语法限制，零过程0不能作为概率选择中的被加数我们写<$E±F以表明存在E±F的推导。可证性关系的逐点扩展到项向量。公理D1和P1的一个直接但重要的推论是：► E + F = E+（EpF）+F。（六）这个凸性方程的一个特殊情况在Bandini和Segala [6]的陈述中作为公理出现按照[15，19]的模式，这个系统的完整性取决于几个重要的变换，这些变换可以通过方程的组合来实现。其中第一个是相互递归定义的解的标准deBakker-Bekic-Scott构造。这体现在下面的命题中，即[15，定理5.7]。22M. Mislove et al. / Electronic Notes in Theoretical Computer Science 96（2004）7-˜ ˜ ˜ ˜ ˜˜˜˜˜˜˜7.我的朋友1（SolutionLemma）LetX1=（X1， . . . ，Xm）和Ym=（Y1， . . . ，Yn）是不同变量的向量，并且Gn=（G1， . . ，G_m）是（X_i，Y_i）中具有自由变量的项的向量，其中每个X_i都是确定的. 然后他就存在表达式E_n=（E1， . . ，Em），其中Y中有h个变量，► E= G{E/X}。此外，如果F=（F1，.，Fm）是Y中具有自由变量的项的向量，使得<$G{F/X} ± F，则<$E ± F。定义7.2一个简单的项是一个变量，或者是一个前缀aE。 一标准形式是形式mn（i）Eiji=1 j=1其中每个Eij是一个简单项。因此，标准形式是一个不确定的和，每个被加数是一个简单项的概率和。如果一个项aE作为Eij之一出现，那么我们说E是标准形式的导数下一个命题说每个PE项E可证明等于项向量E的第一个坐标，项向量E是递归定义的解。命题7.3（标准形式）对于任何在Y中有自由变量的项E，有项E1，.，Ek也具有Y中的自由变量使得EkE=E1并且每个Ei可证明等于标准形式，其中每个导数取自集合{E1，.，Ek}。例如，中文（简体）MnJ（i）► E1=Ⓢri jaijEf(i,j)⊕p(i)ΣⓈsijYg(i,j)⊕q(i)Ω.类似的方程对于每个Ei都成立。证 据 （ 略 ） 证 明 是 通 过 E. 分 配 律 D1 和 D2 用 于 处 理 归 纳 情 形E<$F<$pG。固定点方程F1Q8可靠性和完备性下面的定理是本文的主要结果，它断言上述方程对模型D是可靠的和完备的。i=1j=1j=1M. Mislove et al. / Electronic Notes in Theoretical Computer Science 96（2004）7-23定理8.1 <$E ± F i <$[[E]] ± [[F]]。公理N1-N4、P1-P3、D1和D2的可靠性我们现在可以自举证明定点定律F1-F4的可靠性。我们将详细解释两个案例，以展示领域理论的基础如何发挥作用。8.1F2的可靠性为了简单起见，为了避免提及环境，我们假设在E和F中出现的唯一自由变量是X。我们还省略了语义括号，将术语E和F直接视为语义域D上的函数。设d∈D是E+F的一个不动点，即d=E（d）+F（d）. 然后（E（d）<$pd）+F（d）=（E（d）<$p（E（d）+F（d）+F（d）=E（d）+（E（d）pF（d））+F（d）（分布性）=E（d）+F（d）（凸性）=d。因此d也是（E<$pX）+F的不动点。因为递归是由最少的固定点，它遵循[[[μX（（EpX）+F）]]±[[μX（E+F）]]。另一方面，假设d=（E（d）<$pd）+F（d）。我们证明d也是E+F的一个预定点，并得出[[[μX（E+F）]]±[[μX（（E<$pX）+F）]]的结论。为此，考虑以下推导。d=（E（d）pd）+F（d）=（E（d）p（（E（d）pd）+F（d）+F（d）=（E（d）p（E（d）pd））+（E（d）pF（d））+F（d）=（E（d）<$2p−p2 d）+（E（d）<$pF（d））+F（d）。我们可以通过将子项d重写为（E（d）pd）+F（d），然后使用分配性和凸性进行简化来进一步转换上面的最后一个表达式（2）。通过重复执行这些变换，可以获得以下形式的表达式序列：（E（d）rnd）+（E（d）snF（d））+F（d）它们都等于d并且使得rn和sn趋于1。根据算子+和算子φ p的连续性，这个序列在Scott拓扑中收敛到E（d）+F（d）。因此E（d）+F（d）±d.故d是E+F的一个预定点。24M. Mislove et al. / Electronic Notes in Theoretical Computer Science 96（2004）7-MMM8.2F4的可靠性假设F是变量X被保护的项。进一步证明了E和 EJ满足[[[E]]=[[F{E/X}]]和[[F{EJ/X}]]±[[EJ]]，即E是F的一个不动点，EJ是F的一个预动点.我们要证明F4的可靠性，必须证明[[[E]]±[[EJ]]。这是由下面的引理（取GX）得出的。给我8分。2LetGbetmw ithf v（G）f v（F）;n[[G{E/X}]]±[[G{EJ/X}]].我的律师。我们通过引入[[[G{E/X}]]N.根据定理4.1，这就得到了所希望的结果。为了简单起见，为了避免提及环境，我们假设X是F中唯一自由出现的变量。变量X在G{F/X}中被保护。 因此G{F/X}具有标准形式中文（简体）r ij a ij G iji=1j=1从除F4以外的所有定律的可靠性可以得出，每一项都具有与其标准形式相同的外延因此[[G{E/X}]]=[[G{F{E/X}/X}]]=[[G{F/X}{E/X}]]中文（简体）=[[同样，Ⓢ rijaijGij{E/X}<$p（i）<$]]。（七）i=1j=1中文（简体）[[G{EJ/X}]]±[[Ⓢ rijaijGij{EJ/X}<$p（i）<$]]。（八）i=1j=1归纳定理证明对于每一对i，j，[[[Gi j{E/X}]]n [ [ G i j { E j / X } ] ]。归纳步骤依赖于标准形式（7）和（8）之间的结构相似性。特 别 地，对于[[G{E/X}]]]的每个能力ν，存在[[[G{EJ/X}]]的具有ν“n σ的能力σ。 对于[[[G{EJ/X} ]的e个能力σ，，，存在[[[G{E/X}]的具有ν“n σ的能力ν。 该直径满足[[[G{E/X}]n +1 [ [ G { E j / X } ] ]。Q8.3完整性下面我们给出公理完备性的基本证明。M. Mislove et al. / Electronic Notes in Theoretical Computer Science 96（2004）7-25˜˜˜˜˜˜˜˜˜˜˜˜˜ ˜˜MG和H。从G和H中分离出完整的proo一IJIJi=1j=1假设E和F是项，为了简单起见，假设它们是封闭的，使得[[[E]] ± [[F]]]。根据命题7.3 ，有 一个闭项向量E=（E1 ， . . ， Ek ） ， 以及向量Gk=（G1， . . ，Gk）的函数Xk=（X1， . . ，Xk），证明了eachGi是标准形式，且EachGi=E1，且► E= G{E/X}。类似地，存在封闭项F =（F1，.，F1），以及项H =（H1，.，H1）中