高阶过程演算的上下文标记语义及其互模拟特性

理论计算机科学电子笔记138（2005）61-77www.elsevier.com/locate/entcs高阶过程演算的上下文标记语义Yongjian Li李永健1，2中国科学院软件研究所，北京摘要在本文中，我们研究了高阶过程演算的上下文标记转换语义。带标号的转换语义相对干净和简单，此外，我们还发展了一种新的方法来推理高阶替代过程P{Q/X}的行为，并在此基础上直接证明了一个非常重要的结果为了显示我们的语义和既定的，我们的互模拟的特点是在一个版本的倒钩等价。1引言本文有三个主要目的。首先研究了高阶演算中LTS语义的设计原则，不仅给出了计算步骤，而且给出了高阶过程的同余关系。第二个目标是产生一种方法来明确制定高阶替代。我们认为高阶替换是高阶微积分区别于一阶微积分的一个本质特征高阶替代过程P { R/X }的行为应该有一个好的公式。第三个目标是发展新的技术来解决高阶微积分中的困难问题，如同余问题，因式分解定理，并以更直观的方式组织理论结构。1本工作得到了国家自然科学基金项目（60173020）的资助2 电子邮件地址：lyj238@ios.ac.cn1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.05.00562Y. Li/Electronic Notes in Theoretical Computer Science 138（2005）61−→−→标记语义在早期的过程计算研究中取得了很大的成功基于标记语义，互模拟的思想由Milner和Park [1][2][3]提出并阐述，并已成为进程演算中最重要的概念之一当转向具有移动性和高阶特征的更强大的过程演算时，传统的标记语义变得难以处理，并且相应的互模拟公式通常更加详细，从而导致不太令人满意的理论。似乎有两个问题使得传统的标记语义难以实现更丰富的进程演算。第一个是将本地名称传递到定义它们的作用域之外为了解决这个问题，引入了作用域挤压规则[4]，但它也给标签引入了一些微妙的结构，并使标签转移关系的定义第二个问题是传统LTS中高阶输出动作标号的意义它只考虑进程发出的对象，而不考虑应该在其中使用发出的对象例如，让我们考虑∼−在HOπJs LTS [8]的输出动作Pν caKPJ∼−νcaK代表输出对象和挤出名称，并且PJ表示P.A1的剩余部分-尽管标签包含复杂信息，但整个转换规则不包含关于其中应该使用发射对象的上下文的任何信息。这种传统的高阶输出转移定义会导致互模拟定义中的非自然性问题。更详细地说，当定义两个示例过程P，Q的某种互模拟R时，我们不能使用下面的传统子句来定义两个过程的高阶输出动作的匹配，μ• 当P−→PJ，则QJ存在s.t. QμQJ和PJRQJ，其中μ是a高阶输出动作。（一）与一阶输出动作不同，高阶输出动作（例如过程）的标签比较不能基于互模拟公式中的句法同一性，这对于任何合理的语义等价来说都太强了。在比较标签[5]中，Rebecsen使用了双相似性而不是同一性，遵循Astesiano和Boudol [ 6 ][ 7 ]的早期思想，但由此产生的等价性仍然太强。Sangiorgi在[8]，[9]中有一些非常说明问题的例子他指出，物体部分之间的分离（即，所发出的过程）和高阶输出的上下文阻止了对这两者专用的信道的满意处理，并且然后导致了上述高阶互模拟的问题为了避免输出动作的对象部分和上下文之间的这种分离，他提出了一种上下文bisimu-Y. Li/Electronic Notes in Theoretical Computer Science 138（2005）6163−→−→如下所示，它明确考虑了应该使用发射对象的上下文。∼−∼ −• 当P（ν b）a∈K1∈ PJ，则QJ存在s.t. Q（ν c）aK2 对于所有G∼∼∼∼其中f n（G）<$（b <$c）=<$，（νb）（P J|G{K1/U}）R（νc）（QJ|G{K2/U}）。（二）在[11]中，Sewell引入了标记语义学的语境观点，并通过明确标记转换捕捉术语和周围语境之间可能的相互作用这一直觉，指出了标记语义学和归约语义学之间的联系大致上，他的想法是，来自过程P的转换的标签将是上下文，当与P放在一起时，创建约简规则的出现作为对这个想法的一个检验，他证明了标记跃迁的新定义为CCS的一个片段引入了相同的互模拟。请注意，Sewell的语境变迁标签与传统变迁标签的关键区别在本文中，我们想表明，同样的想法可以成功地应用于高阶过程演算。在我们的标记转换语义中，有五种标签：τ，a（U）.Q，m.Q，−一个1000磅的，−m.0.像往常一样，P −τ→ PJ代表传统LTS的内部通信。然而a（U）.QPm.QJ−一个小女孩。0J−M. 0J−→P，P−→P，P−→P和P−→P表示P可以响应- -对试验a（U）.Q，m.Q，a_（？）K_（？）0，这是程序的片段，上下文，然后变成PJ。例如，高阶测试标签a（U）.Q意味着环境可以在端口a接受P发出的对象，并在交互后提供延续Q，发出的对象将用于实例化Q中的高阶变量U。第二个目标是产生一种方法来明确地制定高阶替代。我们认为高阶替换是高阶微积分区别于一阶微积分的一个本质特征 高阶替代过程P {R/X}的行为应该有一个好的公式。事实上，我们可以对过程P{R/X}的行为进行非常直观的分类，这些行为要么仅仅是由于P的一部分，要么仅仅是由于R的一个副本，要么是由于P的一个组件与R的一个副本之间的相互作用，要么是由于R的两个副本之间的相互作用。尽管这种分类具有清晰的直观性，但人们从未在高等微积分中明确地将其困难在于P是一个自由变量的开放过程为了克服这一缺点，我们扩展了LTS语义，将符号转换规则与开放公关。例如，我们将有一个这样的过渡，如P−α→PJ，对于openJ64Y. Li/Electronic Notes in Theoretical Computer Science 138（2005）61过程，并且这些转换描述了在P中独立于操作变量的行为。我们将注意到，P{R/X}−α→PJ{R/X}，如果P−α→PJ在我们的LTS。此外，我们还开发了一种新的技术来探索开变量所在的上下文，该技术将分析P{R/X}仅由于R的副本而导致的行为。注意，如果P=C[X]，并且C是静态的，context，ndR−α→RJ，nC[X]{R/X}−α→C[RJ]{R/X}在我们的框架work中.第三个目标是发展新的技术来解决高阶微积分中的困难问题，如同余问题，因式分解定理，并以更直观的方式组织理论结构首先，我们把因子分解定理作为一个比其他作者在高阶微积分中不同语义下更基本的结果直观地说，这个结果告诉我们，可以通过使用触发器替换和私有资源来模拟高阶替换我们直接证明了P{R/X}和νk（P{↑k/X}|k我们采用的技术与高阶替换的细粒度公式密切相关它不再需要使用同余性质，这表明因子化定理是高阶微积分中一个相当独立的结果。进一步证明了高阶代换的同余性质，因式分解定理的简单推论本文的其余部分组织如下：第2节陈述了本文将考虑的演算的语法第三节详细阐述了我们语言的归约语义，以及我们研究上下文标记语义第4节详细说明了上下文标记的转换语义，并介绍了演算中相应的互模拟。第五节证明了互模拟的因子分解定理和同余性质。第6节将展示我们的标记转换语义和归约语义之间的对应关系第七部分是结论及相关工作。2语法我们探索的语言类似于Sangiorgi在[8]中提出的高阶π-演算的第二个片段，它满足以下限制：（1）所有对象都是一元的，（2）每个过程都是有限可描述的，（3）只允许有保护的选择，（4）只允许过程传输（或者过程是唯一的通信值）。 在这个演算中，可以避免复制，因为递归和复制可以在我们的演算中使用限制和并行组合来模拟，如Alfresen [5]所示。 但为了方便起见，我们引入了所谓的资源程序k P，它是一个被k永远引用的服务器进程，并在被引用后生成P的副本-Y. Li/Electronic Notes in Theoretical Computer Science 138（2005）6165ΣΣ一次就死了。设FN（HN）是一阶（高阶）名称的有限集合中的可数项则FN = df{m|m∈ FN}，HN = df{a|a∈ HN }，N = FN <$HN，N = FN <$HN.在N中不出现的特殊符号τ表示无声符号。我们用K，L，P，Q，R来排列进程a，b，.，在更高阶的名字m，n，.在一阶名称x，y，. 用于在名称上进行范围，U、V、X、Y用于在变量上进行范围，l、k用于在FN <$FN<${τ}上进行范围，α、μ用于在N <$N <${τ}上进行范围。 按照惯例，如果l τ，则l = l。定义2.1我们的语言的语法如下：P：：= {αi.Pi|i∈I}|P1|P2|νaP|X| ⟨k⇐P ⟩−α：：= a P|a（十）|L像往常一样，用0表示我们写P{Q/X}来表示Q对X在P中的自由出现的避免捕获的高阶替换，fn（P）（fv（P对于出现在P中的自由名（变量）的集合，n（P）（V ars（P））对于出现在P中的名（变量）的集合。我们把所有过程的集合写成Pr，把所有闭过程的集合写成Prc为了方便起见，我们将α-等价的过程视为语法相同的过程，P=Q意味着P和Q是语法相同的。定义2.2当hole []替换定义2.1中语法给出的过程项中出现的0时，就得到了上下文。静态上下文C由BNF语法定义：C：= [] |C|P|P|C| νbC。对于上下文C，我们通过归纳法定义bn（C）（1）bn（[]）=（2）bn（X）=(3) bn（C|P）= bn（C）(4) bn（P |C）= bn（C）(5) bn（νbC）=bn（C）<${b}我们使用C来在上下文上进行范围，并使用C[P]来表示通过在C中用P替换[]而获得的过程。3归约语义在本节中，我们首先介绍我们的演算的归约语义本文选择归约语义作为研究的出发点，主要有三点：（1）归约语义的解释是由一组重写语义统一给出的66Y. Li/Electronic Notes in Theoretical Computer Science 138（2005）61一规则、可以应用它们的一组归约上下文以及结构一致性。因此，它可以很容易地用类似于上下文演算的风格来表达。(2)如前所述，我们采用语境观点来制定一个新的标记语义，而所谓的语境观点的本质只是明确了标记转换捕捉一个术语和周围语境之间可能的相互作用这有助于解释我们提出新的标记语义学的动机（3）如果归约系统是可用的，则通过证明两个语义之间的正确性，可以证明新的标号语义的正确性结构一致性如下：(i) （P |Q）|R P|（Q|R）; P |Q Q|P; P |0元（ii）vx00;vxvyPvyvxP;（vxP）|Q_x（P|Q），如果x∈/fn（Q）.约简关系是如下规则的集合H-COM：100（U）. P，... }|{−}−→P{K/U}|QF-C O M：{m. P，... }|{−}−→P|Q智商，...R-C O M：mP|{m.Q，.. . }−→P|⟨m⇐P⟩|QP−→PJP−→PJPAR：P |Q −→ P J|Q RES：νx P −→ νx P JQ<$P，P−→PJ，PJ <$QJ联系人：Q−→QJE xample3.1LetR1=νxa . P，R2=νya（U）.Q，R=R1|R2，andx=/y，x <$f n（Q）=<$，显然，存在一个约化R −→ νx（（νyQ）{S/U}|P）如上所示，进程R1可以输出一个对象S，它可能包含本地名称x。如果R1被一个平行的上下文包围，即， 我们将R1与某个环境过程X并行，则R1项有一个约简|X涉及R1和X之间的交互当且仅当X可以执行输入动作，即，a（U）.Y在X中无保护地发生，对于某个Y，a是无限制的。 在约简发生之后，对象S到X的输出将通过用S实例化X的延续部分中的某个变量U来表示。在上面的例子中，R2肯定可以提供一个名为a的输入动作，并且在动作发生后它的延续是νyQ因此，我们可以将X的输入操作视为X提供的测试，通过该测试，X可以输入R1发出的名称为a的对象，并将延续Xj传递给R1。更正式地说，我们可以将测试写为a（U）.XJ。对于上面的例子，我们可以写R2可以提供一个测试a（U）.νyQ。R1的一个输出动作就是它对这样一个测试的反应.因此，我们很自然地通过对环境提供的输入测试的反应来表示R1注意，测试a（U）.XJ的语法是Y. Li/Electronic Notes in Theoretical Computer Science 138（2005）6167−→从代表环境的上下文中提取出来，这就是上下文观点的本质。另一方面，我们可以采用语境的观点来确定一个过程的输入动作但这个过程要简单得多假设上面例子中的进程R2，如果R2与某个环境进程X并行，则R2项有一个减少|X涉及R2和X之间的相互作用，当且仅当X可以执行输出动作，即，一个无保护的K.Y出现在X中，对于某个Y。交互作用对R2的影响可以通过实例化R2与对象K的延续来表示。我们可以将X的输出操作看作是X提供的一个测试，通过这个测试，X可以输出名称为a的对象K。的输入动作R2只是它对这样一个测试的反应。因此，我们可以通过由R1的环境提供的输入测试来表示R1的输入动作 为了统一地将测试表示为上下文的片段，我们将这样的输入测试编写为一个RISK测试。0，而不是一个K。在上面的例子中，我们可以写R1可以提供一个测试a. 0的情况。类似地，我们可以采用上下文观点来确定第一输入和第一输出动作的含义。在介绍了关于过程动作意义的语境观点背后的动机在我们的LTS中的转换标签是上下文的，在这个意义上，每个标记的transtion代表一个小程序，诱导适当的减少。[11]有五种。−a（U）.Q，aR. 0，m.Q，m. 0. 如预期P−τ→ PJ表示−a（U）.Q内部沟通。但是P−→PJ，Pm.QPJ，P一个小女孩。0−→PJ，P−m→. 0PJ表示P能够响应测试a（U）.Q，m.Q，−一个小女孩。0、和m. 0，然后变为PJ。在下面的部分中，我们将正式介绍我们的上下文标记语义。4上下文标记语义为了符号简单，我们还在以下转换语义的定义中扩展了对标签a（U）.Q和m.Q的限制和并行操作Ifα=a（U）.Q，若U∈/fv（P），α|P表示sa（U）。（Q|P），P|α表示a（U）. （P|Q）;若x∈/fn（α），则νxα表示sa（U）. vxQ. Letα=m.Q，α|P表示M. （Q|P），P|α表示sm。（P|Q）;若x∈/fn（α），则νxα表示sl. νxQ. 我们定义α{R/X}=dfτ，如果α=τ，α{R/X}=dfP{R/X}，如果α=P，对于某个P。标记的转移关系由表1中的规则给出。与辅助关系的规则一起用于com的边条件中68Y. Li/Electronic Notes in Theoretical Computer Science 138（2005）61{Σ一H-输入：{a（U）.P，... }−一个小女孩。0−→P {K/U}H-输出：− K. P，...−a（U）.QP|Q{K/U}F-输入：{m. P，... }−m→. 0PF-输出：{m. P，... .M. QP|Qa（U）.Q}−→P−→RH-Coml：（PJ↓a（U）.Q）P|PJ−τ→Rm.QP−→RF-Coml：（PJ↓m.Q）Parl：Res：P|PJ−τ→P−α→PJP|Q−α→PJ|QP−α→PJαR（c∈fn（α））νc.P−→νc.PJ−Resource：mP−m→. 0P|⟨m⇐P⟩τ-Pe fix：τ{τ. P，... }−τ→PF-输入-P红色：{m. P，... }↓m.PH-Input-Pred：{a（U）.P，. } ↓a（U）.PP↓αRes-Pred：νc P↓νc αP↓α（c∈fn（α））左预测： P|Q ↓ α|Q （bv（α）∈/fv（Q））资源：m P ↓ m。（P |m表1标签转换通信规则辅助谓词P↓a（U）.PJ表示P可以提供测试a（U）.PJ. 在这种情况下，它与[15]中的承诺谓词相同的a（U）.QP通信规则−→R（PJ↓a（U）.Q）表示，如果P可以对P|PJ−τ→R测试a（U）.Q并变成R，而PJ可以提供测试，然后把它们并行地，系统可以进行内部通信并变成R。换句话说，R的内部通信是由于R1对R2提供的测试的反应，其中R1，R2是R的一些子过程。我们可以很容易地证明以下三个引理。} −→Y. Li/Electronic Notes in Theoretical Computer Science 138（2005）6169˜ ˜ ˜ ˜ ˜通常情况下，t=f−τ→的transitive和rexexiveclosureeμ，=beμμbμ=−→=，如果μ=τ，则==，否则=。 Pα表示P = Δ ↓ α。有了这个标记的转移关系，互模拟的概念可以用通常的方式给出。定义4.1二元关系R <$Prc×Prc是强/弱模拟μ如果PRQ意味着当P−→PJ，则存在QJ使得QμJμbJ J J−→Q/Q = Q和P R Q，其中fv（μ）=。一个关系R是强/弱互模拟，如果R和R−1都是强/弱模拟。 我们说P，Q是双相似的，记为P<$/<$Q，如果PRQ对于某个强/弱互模拟R.定义4.2[开放过程的互模拟]对于过程P1，P2，自由可变的fv（P1）fv（P2）X，如果全部闭合，则P1/P2处理Q时，P1{Q/X}≠ P2{Q/X}。引理4.3假设P<$Q，且P↓a（X）.S，则对任意K，存在SJS. T. Q∈a（X）.SJ和S{K/X} ∈SJ{K/X}.下一个引理说，在非对象上下文中保留了对象引理4.4设P，Q，R，S是闭过程表达式，若P<$Q，则(1) vxPvxQ(2) α.P+R<$α.Q+R(3) P|罗克|r33和|PR|Q(4)⟨k⇐P⟩≈⟨k⇐Q⟩注4.5在引理4.4中，（3）的证明需要特别注意。而不是证明{|P<$Q，P，Q，R∈Prc}是一个互模拟，这里我们应该证明{（C [P]，C[Q]）|P<$Q，P，Q∈Prc}是互模拟，其中C是静态上下文.现在我们已经证明了弱互模拟在所有算子除了对象构造器（即， PQ意味着−aP.S+R−aQ.S+R），这是最困难的，由于高阶设置，我们的语言属于。 为了得到这一点，我们必须证明高阶替换上的P_Q的同余性质（即P_Q蕴涵P{R/X}_Q{R/X}）。我们可以遵循Sangiorgi[8][9]。但本文首先独立证明了分解定理，然后证明了高阶代换上的同余性质只是前者的一个推论70Y. Li/Electronic Notes in Theoretical Computer Science 138（2005）61Σ一一−→一5互模拟的因式分解定理和同余性质。高阶代换为了方便起见，我们用↑k来表示触发程序，它是一个k形式的进程。0的情况。直观地说，在过程νk（P{↑k/X}|<$k<$Q<$k），进程Q表示P的“本地资源”，k是指向该资源的“指针”，触发器↑k的唯一功能是激活Q的一个副本，Q的每个副本在需要时由触发器↑ k激活。 很自然地，我们要探索是否νk（P{↑k/X}|在弱互模拟的意义下，P { Q/X}和P{Q/X}是等价的。我们将要证明的因式分解定理告诉我们是这样的。 为了证明νk（P {↑k/X}|当过程νk（P {↑ k/X }）与P {Q/X}双相似时，我们需要四个引理，引理5.2和引理5.3分析过程νk（P {↑ k/X}）中发生的转移|引理5.4、5.5分析P { Q/X }中发生的非通信导出的和通信导出的转换。我们使用的中央技术是基于制定的非通信衍生的过渡或通信衍生的过渡执行这些条款。通过对这些跃迁的细粒度表述的分析高阶替代过程的公式化的细节可以在[17]中找到在我们的语义中，转换分为两组：非通信派生（或前缀）转换;通信派生转换。比如说，−v b（a 0.0个）a（X）.X−→νb（0 |0）是非通信派生的，因为它是由于prefixtransition−100Ω。0）a（X）.X0|0;但transition νb（− <$0<$. 0|a（X）。X）−τ→v b（0 |0）是通信派生的，因为它是由于通信trans.com如果你是我的话，0|a（X）.X−τ→0 |0的情况。定义5.1设P−α→PJ是一个转移，如果它的导出树不在-在H-Coml，H-Comr，F-Coml，F-Comr规则中，则我们称其为非通信衍生的转变;否则，我们称其为通信衍生的转变。下面的引理分析了结果进程的形式，它是由一个已被触发的资源副本派生的引理5.2设P∈Pr，fv（P）<${X}，Q∈Prc，且k不出现在P，Q，如果P{↑k/X}|-τ→PJ，并且导出这个转移的最后一个规则是F-Comm，则存在上下文C使得P = C [X]，PJ<$C [Q]{↑k/X}|.Y. Li/Electronic Notes in Theoretical Computer Science 138（2005）61710000000⎩⎭下面的引理说，如果P{↑k/X}执行与k无关的动作α，则P可以执行α。给我5分。3如果P{↑k/X}-α→PJ，fv（P）<${X}， fv（α）=<$，且k个d不出现在P，Q，α中，则存在一个程序P0使得PJ=P0{↑k/X}，并且P−α→P，更进一步，对于任意的d，it保持P{R/X}−α→P{R/X}普塞斯河下面的引理分析了非通信导出的转移P{R/X}−α→Acn如何由yνk（P{↑k/X}|k给我5分。4LetP∈Pr，fv（P）<${X}，如果P{R/X}−α→PJ，且该变换是非通信导出的，则(1) 或者对于某个P，P{R/X}= PJ，且νk（P{↑k/X}|）−α→νk（P0{↑k/X}|）;(2) 或P=C[X]，其中R−α→RJ，C[RJ]{R/X}=PJ，对于某些C，RJ，且νk（P{↑k/X}|k< <$R>）−τ→−α→νk（C[0|RJ|< kR>]{↑k/X}）。下面的引理分析了如何通信派生的转换，P{R/X}可由νk（P{↑k/X}）模拟|k给我5分。5LetP∈Pr，fv（P）<${X}，若P{R/X}-τ→PJ，且该变换是通信导出的，则存在过程P0使得PJ=P{R/X}和νk（P{↑k/X}|< kR>）。−τ→∪−τ→−τ→∪−τ→−τ→−τ→Σ≡νk（P0{↑k/X}|）。在我们继续证明因式分解定理之前，我们首先定义一个关系TrigForm，定义5.6二元关系TrigFormPrc×Prc定义如下：TrigForm=你好，Q。 P=P0{R/X}，Q∈νk（P0{↑k/X}|kDF. 对于k，P，R，其中fv（P）<${X}且R∈Pr引理5.7设P，Q∈Pr，TrigForm（P，Q）蕴涵TrigForm（C[P]，C[Q]）对于任何静态上下文C.结合引理5.2、5.3、5.5和5.4，我们可以分析P{R/X}且νk（P{↑k/X}|k定理5.8设P∈Pr，R∈Prc，fv（P）<${X}，且k在P和R中不自由出现，则有νk（P{↑k/X}|）P{R/X}。此外，它还认为：C72Y. Li/Electronic Notes in Theoretical Computer Science 138（2005）61⇒000）=(1) 当νk（P{↑k/X}|）−α→PJ，存在tsQJs。t.P{R/X} =αbQJ和TrigForm（QJ，PJ）;(2) 反之亦然，当P{R/X}−α→PJ时，存在sQJS. t. νk（P{↑k/X}|联系<我们αbQJ和TrigF orm（PJ，QJ）;证据 让={|k|如果k在P，R中不自由出现}。我们证明了λ是一个直到λ的互模拟。请注意，TrigForm（PJ，QJ）意味着对于某个Q j j，PJ<$QJ <$QJ。I. 证明了P {R/X}可以模拟νk（P {↑ k/X}）的任何行为|kSupposeνk（P{↑k/X}|<$k<$R<$）−α→νkPJ，则nP{↑k/X}|当k∈R<$−α→PJ时，分析的结果是P{↑k/X}的线性方程组|<$k<$R<$−α→PJ。情形1最后一个规则是F-Coml，α = τ，则根据引理5.2，存在上下文C使得P= C [X]，PJ<$C [R]{↑k/X}|如果P = C [X]，则P{R/X}= C [R]{R/X}。 所以P{R/X}= P{R/X}=C[R]{R/X}，和TrigForm（C [R]{R/X}，νkP J）。情形2最后一个规则是Parl，则存在一个程序PJ使得P{↑k/X}−α→PJ，kdoe在P，Q，α，so e中不成立，由引理a5.3可知，x是a程序PsuchthatP−α→P，PJ=P{↑k/X}，P{R/X}−α→P{R/X}，0 0 0 0和TrigForm（P0{R/X}，νk（PJ|kII. 我们证明了νk（P{↑k/X}|kP {R/X}。SupposeP{R/X}−α→PJ，则情形1这个转移是通信导出的，根据引理5.5，存在τP0满足PJ=P{R/X}，且νk（P{↑k/X}|k<$−τ→−τ→ <$−τ→） =QJ <$νk（P{↑k/X}|对于QJ，0TrigForm（PJ，QJ）;情形2这个转移是非通信导出的，根据引理5.4，则有两种情形：（2-1）对于某个P，P{R/X}= PJ，且νk（P{↑ k/X}| k<$R<$）−α→νk（P0{↑ k/X}|和TrigForm（P0{R/X}，νk（P0{↑ k/X}|k（2-2）或P=C[X]，其中R−α→RJ，C[RJ]{R/X}=PJ，对于某些C，RJ，且νk（P{↑k/X}|k<$R）−τ→k/X}|k−α→νk（C[0]{↑k/X}|克·卢尔|RJ）νk（C[RJ]{↑显然，TrigForm（C [RJ]{R/X}，νk（C [0]{↑k/X}|克·卢尔|RJ））。QY. Li/Electronic Notes in Theoretical Computer Science 138（2005）617322引理5.9（abs-同余）设P1，P2，P∈Pr，fv{P}<${X}，P1<$P2蕴涵P{P1/X}<$P {P2/X}。证据结合引理4.4和5.8，我们有P{P1/X}π（引理5.8）νk（P{↑k/X}|kνk（P{↑k/X}|kP{P2/X}Q定理5.10（目标算子下的同余）设P，Q，R，- -S是处理表达式，如果P<$Q，则a<$P<$.S+R<$a<$Q<$.S+R证据 引理5.9。Q6倒钩等价在这里，我们将以[13]的风格提出一个倒钩等价的概念，这是[8]中提出的倒钩互模拟的变体，也被Sangiorgi在[ 10 ]中称为感兴趣的读者可以参阅[14]，[10]关于这两种方法的讨论。作为−通常，P↓a表示a（U）.Q，aK.Q在P中无保护地发生，不受限制，即， 出现不是c（U J）.R，c <$KJ<$.R的子表达式，也不在νa的范围内。类似地，我们可以定义↓m，其中m是一阶名。此外，我们定义P_a（U）.S来表示P（−→）_a（U）. S。定义6.1二元关系R <$Pr× Pr是倒钩互模拟，如果P1RP2意味着(1) 对任意过程Q∈ Pr，P1|QR P2|Q.(2) 对于每个名字a，P1<$x当且仅当P2<$x;(3) 当P1-→Pj时，则存在PJ使得P2（-→）<$PJ且PJ1 2 2 1RP J.(4) 当P2-→Pj时，则存在PJ使得P1（-→）<$PJ，PJ2 1 1 1RP J.两个过程P和Q是倒钩等价的，记为PbQ，如果PRQ对于一些互模拟R.现在我们证明，对于高阶微积分来说，Bb和Bb是一致的我们需要下面的引理，这些引理很容易证明。下面的引理将n−→和−τ→之间的对应关系联系起来。74Y. Li/Electronic Notes in Theoretical Computer Science 138（2005）61J=00000J−→引理6.2P−→PJ当且仅当存在P0，PJ使得P<$P0，0τJ J JP0−→P0，P0<$P.引理6.3对于任何进程P和名字x，它成立：(1) 如果x是一个高阶名，则P↓x成立当且仅当P−α→PJ- -其中α = x（U）.Q，x<$K<$. 0表示U、K、Q、P。(2) 如果x是一阶名，则P↓x当且仅当P−α→PJ，其中reα=- -x.Q，x. 0对于一些Q，P。引理6.4设z是在P中非自由出现的名字，a（U）.Q，m。0然后−一个小女孩。0，m.Q，a（U）.Q(1) 如果Pm.QJ J=P/P= Pm.z= 0.Q= 0.PJ;则P |z（X）。0 |a（U）. z 0.Q =P/P |z（X）。0|−一个小女孩。0J−M. 0J-τJ−(2) 如果P=P/P.z（U）。0=P则P |z（X）。0|a K. z 0. 0 =0.000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 M|=τPJ;（3）如果P |z（X）。0 |a（U）.z <$0 <$.Q（−→）<$P JJ/P |z（X）。0 |m.z<$0 <$.Q（−→）<$P JJ，以及PJJ/p则存在PJ使得Pj<$PJ，且Pa（U）·QPJ/Pm·QPJ;z-你好==吉吉（4）如果P|z（X）。0|aK.z0. 0（−→）P/P |z（X）。0 |m.z = 100 μm。0（−→）P和PJJ/zz则存在PJ使得P j<$PJ，且P−一个小女孩。0=P/P−M.0PJ;定理6.5对于两个过程P和Q，P<$bQ当且仅当P<$Q。证据如果：我们表明，是一个倒钩互模拟。假设P=Q。通过引理4.4，在并行运算中保持了k。如果P−→PJ，则由引理6. 2，t∈PJsucthatP<$P，P −τ→PJ，PJ<$PJ. Since，然后00 00 0P0<$P<$Q，所以Q =<$QJ，对于某个QJ，其中QJ<$PJ<$PJ。以引理为例6.2 同样，我们可以找到QJ，使得Q（−→）<$QJ和PJ<$QJj.于外稃6.3 而P<$Q，我们有P<$x当且仅当Q<$x。只有当：我们证明了，Bmb是一个互模拟到。 考虑P bQ。Sup-posettPa（ U ） .RPJ.Chooosesomez∈fn （ P ， a （ U ） . R ） ， 通 过 定 义 weh eP |z（X）。0 |a（U）.z 0. RbQ|z（X）。0 |a（U）.z <$0 <$.R，并且通过引Y. Li/Electronic Notes in Theoretical Computer Science 138（2005）6175理6.4（1），P |z（X）。0 |a（U）.z <$0 <$.R =<$P1<$Pj，对于某个P1，其中P1/<$z，则由引理6.2，P |z（X）。0 |a（U）.z <$0 <$.R（−→）<$PJ，因此Q|z（X）。0 |a（U）.z <$0 <$.R（−→）<$Q1对于某个Q1，其中Q1/<$z且Q1<$bP1。 根据引理6.4（3），存在QJ，−Qa（U）.RQJ<$Q，则JbJ一个很好的朋友0JM.RJ=1你好。 关于P−→P，P−→P，P−m→. 0PJCANAP−τ→PJ更简单。Q76Y. Li/Electronic Notes in Theoretical Computer Science 138（2005）617结论及相关工作实际上，本文的工作是[16]工作的继续和扩展在[16]中，我们分别研究了一阶π-演算和高阶π-演算的一个简单片段中的上下文标记语义。事实上，高阶π-演算的那个片段的语法是非常有限的，并且比本文中的简单得多本文将语义框架推广到全二阶微积分时，并行算子的常规证明方法失效，必须如注4.5所述进行修正此外，本文还导出了文献[16]中未涉及的因式分解定理这是一个很大的进步，因为因式分解定理揭示了高阶微积分的本质。Sangiorgi在类似的主题上对更高的过程结石做了最开创性的研究[8][9]。在[9]中，他提出了一个传统的后期标记语义和上下文互模拟更高的进程演算。为了证明上下文互模拟的同余性质，他首先证明了它在并行和复制算子下是保持的，然后他利用P的结构归纳法证明了关于高阶替换的同余性质利用同余性质和一些巧妙的技巧，证明了所谓的蕴涵替换的分配性，从而得到了因式分解定理的结果。我们实现核心结果的方法与他的方法有很大的不同。主要区别在于高阶代换和因式分解定理的同余性在他的证明中，第一个问题是主要的，并且是独立证明的，第二个问题的证明大量使用了第一个问题的结果。我们强调，因式分解定理的证明是不容易的，即使有同余的结果[9]。但是我们把因式分解定理看作是更基本的结果，它可以独立证明，的congruence性质的高阶替代是一个简单的推论的因式分解定理。 我们证明因式分解定理的主要技术是基于直觉，即P{R/X}和νk（P{↑k/X}|kFactorisation定理是高阶演算中的一个关键结果，它揭示了高阶替换可以通过触发器和私有资源来模拟。在此基础上，可以很容易地导出同余性质此外，它在我们推导正常互模拟时起着关键作用Je Escherey和Rathke采用了同样的思想，给出了一个带有局部名的CML片段的标号语义[12]，并证明了这样得到的双模拟等价与倒刺等价的一个版本相同我们论文中第一个特征定理的证明类似于他们的证明。Y. Li/Electronic Notes in Theoretical Computer Science 138（2005）6177工作但由于CML的函数性质，他们在工作中采用了触发语义来证明互模拟等价的同余性质，粗略地说，他们首先直接证明触发语义的同余性质，然后证明原语义与触发语义的对应关系，从而得到原语义的在[18]中，他们直接引入了触发器语义作为各种高阶π-演算的规范语义，并证明了触发器语义中的互模拟等价与约简语义中的倒钩等价最重要的结果是，他们证明了这种语义的互模拟等价的同余性质的递归类型的语言。他的证明技术仍然是一个结果，就像因式分解的-orem，而不是归纳技术的类型，这通常是失败的高阶语言与递归类型。理解我们的高阶演算的语义和公式是否可以应用于这些演算将是非常有趣的引用[1]R.米尔纳通信系统的微积分。LNCS 92，Springer Verlag，1980年。[2]D. 公园无限序列上的并发性和自动机。LNCS 104，1981年。[3] R. 米尔纳 通信和并发。普伦蒂斯·霍尔1989年[4] R. Milner，J. Parrow，and D.沃克移动过程的演算（第一部分和第二部分）。信息与计算，100，1992。[5] B.我是杰森高阶通信系统的微积分。博士论文，帝国理工学院计算机系，1990年。[6] E. Astesiano和A.乔维尼关系规范中的广义互模拟。LNCS 294，第207-266页。[7] G.布多面向并发和通信系统的lambda演算。LNCS 351，第149-161页。[8] D.桑吉奥吉表达进程代数中的迁移性：一阶和高阶范式。 博士论文，爱丁堡大学，梅菲尔德路，爱丁堡，苏格兰，1992年。[9] D.桑吉奥吉高阶过程演算的互模拟。信息与计算，131（2）：141- 178，1996.[1