名传递演算中名称传递的同余格式

理论计算机科学电子笔记156（2006）169-189www.elsevier.com/locate/entcs名传递演算的一种同余格式Axelle Ziegler、Dale Miller和Catuscia Palamidessi1INRIA-FutursanddLIX，E′colePolytechnique，Palaiseau，France摘要我们定义并使用基于SOS的框架来指定具有名称传递属性的演算的转换系统。这种设置使用证明理论工具来处理名称绑定的一些特殊困难，并使它们在证明中更容易处理。本文的贡献是提出了一种格式，确保开放双相似性是该框架内指定的演算的一致性，将众所周知的tyft/tyxt格式扩展到名称绑定和名称传递的情况。我们将这个结果应用到π演算的晚期和早期语义中关键词：结构操作语义，规则格式，名称绑定，名称移动性，开放互模拟。1介绍结构化操作语义（SOS）[22]非常适合进程演算的规范，并允许清晰方便地表示转换系统。由于人们希望以组合的方式来推理行为等价性，因此许多研究人员对操作语义的规范进行了限制，以保证派生的双相似性概念是一致的。第一个这样的限制，如GSOS [4]，tyft/tyxt [9]和Panth[31]，并不适合处理涉及抽象的过程。这种进程演算的例子是高阶进程演算，如CHOCS [26]，以及名称传递和1电子邮件：ziegler [at] clipper.ens.fr，戴尔[在] lix.polytechnique.fr，和catuscia [at] lix.polytechnique.fr1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.09.032170A. 齐格勒等人/理论计算机科学电子笔记156（2006）169名称绑定过程演算，如π演算[16]。最近，有人提议将规则格式扩展到高阶语言[10]，特别是高阶进程演算[3，11]。然而，[11]既没有考虑名称传递也没有考虑名称绑定的特性，而[3]确实处理了一些名称传递语言，但代价是完全重写了规范，最终以间接和低级的方式表示名称的特性。据我们所知，与名称相关的机制的规则格式还没有被研究过，至少没有以直接的方式。本文的目的是填补上述空白：我们提出了一个规则格式的名称传递和名称绑定进程演算，保证开放的双相似性是一个同余，并处理名称绑定和传递直接的方式。为了得到全等的结果，我们需要明确名传递和名绑定过程演算的全等概念。我们提出了一个概念，它将标准的一阶全等概念提升到我们的高阶设置。我们的定义受到了λ演算中类似定义的强烈启发（例如，逻辑关系[24]）。在进程演算的框架中，我们所知道的唯一的另一种提议是这样的概念：抽象和具体的π-演算的主体同余[12]。然而，我们方法的精神与[12]的精神不同：我们的目标是 在保持一致性的一阶概念的意义，因此，我们的定义要严格得多。例如，强双相似性在[12]中是一个主体全等，但根据我们的定义不是全等本文的结果是基于第一作者详细内容请参阅本文全文[33]1.1论文计划在第2节中，我们描述了用于编码转换系统规范的证明理论工具，并简要说明了它们与π演算的使用。第3节和第4节展示了如何将互模拟和同余的通常概念提升到我们的证明理论框架中以适应名称绑定。在第5节中，我们使用这个框架来定义一个规则格式，以确保开放双相似性是一个同余。我们在第6节中总结了一些未来的方向。A. 齐格勒等人/理论计算机科学电子笔记156（2006）1691712过渡系统规范和名称传递2.1激发绑定SOS的标准处理在用于指定名称传递和名称绑定演算（例如π演算）时的主要缺点是变量和名称的状态通常需要添加许多副条件。例如，有些可能要求名称在某些子表达式中是自由的，或者名称在某些上下文中是“新鲜的”，等等。此外，这些副条件的存在通常被认为会给特定过程演算的理论带来许多复杂性。用抽象来指定流程语义的一种更具声明性的方法涉及到找到一种完全内在化绑定复杂性的逻辑。如果有这样的逻辑，那么希望边条件被逻辑中自然发生的现象所取代。当然，这种逻辑的规范者必须处理绑定和替换的复杂性。1940年，Church [5]设计了简单类型理论（STT）作为一种高阶逻辑，它只包含一个绑定器，即λ-绑定器，可以用来捕获公式和术语中的所有绑定器。STT的证明规则确实很复杂，以便完全公理化λ-binders如何与逻辑推理规则相互作用。几十年后，编程语言的经验，如λProlog [14]（基于STT的一个子集，没有扩展性）表明，操作语义规范中的绑定可以在该逻辑中以声明方式处理。在高阶逻辑的某些弱子集中使用λ-项被称为编码语法的λ-树语法方法[15]。 λ树语法方法是高阶抽象语法（HOAS）的一种特殊方法[21]。在后者中，绑定的编码的其他方法是可能的。例如，[6]中π演算的HOAS编码使用了一个扩展逻辑，因此语法中的绑定被映射到高阶逻辑中的函数。本文的大部分开发都要求逻辑将λ-绑定解释为抽象语法而不是函数。虽然丘奇 Miller和Tiu [18，17]最近的论文提供了这样一种方法，提供逻辑FOλΔ（fold-nabla），其中包括用于定义类属判断的新量化器。在FOλΔΣ中，完全可以为π演算[29，28]172A. 齐格勒等人/理论计算机科学电子笔记156（2006）169声明性的，没有附加条件的。2.2系统技术说明为标记的转换系统呈现SOS的常规方法使用以下形式的推理规则：.ΣA我Pi−−→ Qi|i ∈ I.一P−−→Q这是一个微不足道的观察，这样的推理规则可以被视为号角条款- 是的ΣΣAiAXPi−−→Qi<$P−−→Qi∈I一个T阶逻辑。在这里，他的价值在他的李stX'变量是否自由在规则的结论或前提中。 它们有一阶类型n、a或p，分别代表名称、动作和进程这些变量被称为推理规则的元变量或模式变量。为了使用这种传统的方法来处理进程及其转换中的名称绑定构造，经常使用推理规则上的副条件。这些附加条件通常说明名称是“新鲜的”或在给定术语中不是自由的。有两种选择来形式化这样的副条件：一种是在一阶逻辑中将它们公理化，或者，按照2.1节的动机，转移到直接支持绑定的逻辑。我们在这里采用第二种方法。特别是，我们使用FOλΔ一种逻辑，允许在术语中进行λ-绑定，并使用两个箭头类型n→a和n→p是由这个λ-结合构造的。由STT导出的包含λ-绑定的句法表达式满足α、β和η转换。正如我们将看到的，为了能够充分地推理λ-抽象的结构，我们将需要λ-量化器，以及对n的类型的区分。为了编码一个转换系统，我们将引入一个新的类型系统：如前所述，在我们的语言中，对于过程的句法范畴，我们有一个类型p，但是对于名称的句法范畴，我们实际上需要两个类型n和v。在这里，n表示通常的名称概念，包含无穷多个常数，v表示新名称。没有常量被假设为v类型，v被认为是n的子类型，这意味着我们可以在需要n类型值的任何地方使用v¯A. 齐格勒等人/理论计算机科学电子笔记156（2006）169173我（新名字就是新名字）。我们也有n→p和v→p抽象。此外，我们还有一个用于操作的类型a，它随三个构造函数一起↓：n→n→a，↑：n→n→a和τ：a，表示输入、输出和内部动作。例如，↓xy表示在名称为x的频道上输入名称y的动作。如果需要，系统可以扩展以处理更多类型的动作。·Transitionshemselvesareencoodedueusingeymbol·−−→·· 这个符号denotesthreedi erent谓词：·−−→·p·取类型p，a和p，·−−·→n→p·讨论pep，n→a和n→p，nd的参数。 −−−·→ ·v→p参数类型为p，v→a和v→p。 第一个谓词允许我们编码自由过渡，而其他两个允许我们编码绑定过渡，抽象的名称或新鲜的名称。这种区别背后的直觉有了这个符号，我们就可以用通常的方法来指定跃迁系统。与通常做法的主要区别是，我们将允许更高类型的模式变量的量化，例如n→a和n→p，以及在规则的前提下对名称进行量化。具体而言，规则将采用以下形式：..Σ一QiPi−−→QiγiΣ| i∈ IP−−→A Qγ其中I是N的有限子集，并且γ和γi可以是{p，n→p，v→p}。此外，模式变量P和Pi是类型p，变量Q、Qi分别是类型γ和γi，并且变量A、Ai是类型a、n→a或v→a，这取决于γ。最后，Qi表示一个可能为空的v型量化变量序列。图1给出了这些推理规则的例子。2.3操作语义学的逻辑我们在这里概述了量子化器的证明理论，以帮助明确它在名称绑定规范中的作用。更多的细节可以在[18，17]中找到。逻辑FOλΔ的证明理论是从直觉主义逻辑的标准微积分中通过添加量化器导出的。这quantifier用于声明一个新对象的作用域在计算的某个部分内，而不在其他地方。考虑到我们在这里关注的是进程演算中的名称绑定，量化的变量将始终是名称，并且它们将174A. 齐格勒等人/理论计算机科学电子笔记156（2006）169在V型中。现在我们概述一下在证明中如何容纳量化。我们的序列扩展了传统的（单结论）微积分的添加和灰的全球和当地的签名。特别是，σ1d B1，.，σnd Bn<$σ0d B0，被称为全局签名的集合Σ i将整个σ i的自由（本征）变量收集在一起，而列表σi是局部签名，并且这些包含仅在Bi上作用的变量。我们认为这两种签名序列内的绑定结构为了说明新的功能FOλΔ，我们提出的推理规则，一个接一个这两个量化器之间的互动是我们工作的核心，σσd<$γx.B，Γ<$C <$Ln;（σ，y）d B[y/x]， Γ<$C;σdB[（h σ）/x]; Γ <$σd<$x.B<$RΣ; Γσ（σ，y）d B[y/x]n;r<$σd<$xB <$R请注意，对于R2，右和左的引入规则基本上是相同的。因此，是自对偶的：也就是说，等价x。B将保持。在比较针对Ranking和Ranking的正确引入规则时，我们注意到Ranking绑定的变量移动到局部签名（自下而上读取校对规则），Ranking绑定的变量移动到全局签名。由BRR规则引入的新特征变量h进行提升：也就是说，它不是用新变量来实例化量化器，而是用“提升”变量表达式（h σ）来实例化量化器，它表示项（hx 1. xn）如果σ是列表（x1. xn）。因此，当一个绑定的变量出现在局部变量的作用域中时，这个绑定的变量将通过对局部变量的抽象来实例化。在这里，我们可以简单地比较一下Gabbay和Pitts提出的“新的“新的”量化器然后能够从这个现有的名称集合中选择一个新的变量名称（特别是，一个在量化公式中不存在的名称），并且基本的集合论提供了量化器是用证明理论来描述的，可以用来量化任何类型（不一定是名称类型），它的元理论并不假设该类型是有人居住的。这个量化器基本上是假设的。它本质上提出了这样一个问题：A. 齐格勒等人/理论计算机科学电子笔记156（2006）169175这两个量化器之间的具体区别在于，“新”量化器既不被“新”量化器所蕴涵，也不需要“新”量化器，而FOλΔ的另一个方面是它允许处理固定点：也就是说，谓词可以被定义为归纳和共归纳。比如说，操作语义由归纳定义来具体化，而双相似性由共归纳定义来具体化。在微积分中如何处理这一点的细节并不是我们介绍规则格式定义的核心，也不是我们陈述主要结果的核心。然而，主要结果的正式证明是基于这种固定的尖结构的细节。有兴趣的读者可以在[19，27]中找到更多细节2.4示例：pi演算为了编码π演算语法，我们使用构造函数0：p，！，τ：p→p，out：n→n→p→p，in：n→（n→p）→p，+，|：p→p → p， 匹配：n→n →p → p，ν：（v→p）→ p。简单地说：特别地，我们将x（y）.P编码为x（λy.P），x<$y。P等于xyP，νy。P为ν（λy.P），[x=y].P为matchxyP.注意π演算绑定在项内映射到λ绑定。我们通常以原始形式编写π演算表达式，并且仅在需要时引用此特定编码。π演算的规则如图1所示。从表面上看，这些推论类似于π演算的通常推论。然而，有几个微妙的差异。一个区别是规则不显式包含名称，而是包含类型v和n的元变量（这些变量是隐式通用绑定的，用大写字母表示）或类型v或n的绑定变量（这些变量是显式λ-或λ-绑定的，用大写字母表示）。变量的类型总是可以从上下文中推断出来。在本文中，可量化的变量将始终被认为是类型v。第二个区别是，这些推理规则使用n→a，n→p，v→a，v→p和（在第二（RES）规则中）n→n→p类型p. 注意，表达式X（y）。（My）匹配π演算表达式n（w）。嗯。当第n个可变元X和M与第n和λ w相关联时，嗯。0，相对独立。 在α-转化之前，这种结构是唯一的. 进一步注意，表达式X（y）.M无法匹配这个相同的π演算表达式，因为没有对M的捕获避免替换将产生该表达式。176A. 齐格勒等人/理论计算机科学电子笔记156（2006）169一τ（τ）（IN）↓X↑XY（OUT）τ。P−−→PpX（y）。（My）−→Mn→pXY。P−→PpP−−→A Rγ（加）P−−→A Qγ（MATCH）P+Q−−→A RγP−−→PJp一个 J（面值）[X=X].P−−→A Qγ一P−−→Mδ一（面值）P|Q−−→P|QpP|Q−−→λ x（M x|Q）δx（Px−−→Ap Qx）（RES）x（Px−−→Aδ PJx）（RES）vx. Px−−→Ap Vx.Qxvx. Px−−→Aδ λy.νx.PJxy1998年，↑Xy↓X↑XP y−→Qy）P−→MQ−→Np（开放）↑Xn→pτv→p（关闭）是的。P y−−→Qv→pP|Q−−→νy。（My|Ny）p↓X↑XYJ↑XYJ↓XP−→MQ−→QP−→PQ−→Mn→pτp（COM）Jpn→pτJ（COM）P|Q−−→MY|QpP|Q−−→Pp| MYP−−→A P Jp（！（法案）P−−→A PJδ（！（法案）！P−−→ApPJ|！P！P−−→Aδλx（P Jx|！P）↑XYJ↓X↑X↓XP−→PP−→MP−→MP−→Np！τJn→p（！COM）v→pτn→p（！关闭）P−−→！P|（Pp| MY)！P−−→νy。（啊！P|（Ny|My））pFig. 1. π演算后期语义的转换系统。还假设了（CLOSE）以及（PLUS）和（PAR）规则我们使用规则的模式变量用大写字母书写的约定类型变量γ在集合上变化{p，n → p，v → p}，而δ的范围为{n → p，v → p}。第三个区别是使用了量化：在图1中没有明确的规则来引入量化。A. 齐格勒等人/理论计算机科学电子笔记156（2006）169177相反，2.3节中概述的逻辑推理规则负责处理这个量化器。高阶变量和量子化之间的相互作用意味着关于名称及其出现的共同附带条件是不必要的。例如，（RES）规则的通常限制，即x在A中不是自由的，隐含在该规则的量化器作用域规则中：x的量化器在A的量化器作用域中，因此没有178A. 齐格勒等人/理论计算机科学电子笔记156（2006）169ττ此推理规则的替换实例将在A的替换中出现x。当然，逻辑保证了替换的应用避免了变量捕获。修改这些规则来编码π演算的早期语义是很简单的：特别是，我们需要添加规则↓徐X（y）（My）−−→（MU）p（IN-E）并将两个（COM）规则替换为↑XYJ↓XYJ↓XYJ↑XYJP−→PpQ−→QpP−→PpQ−→QpP|Q−−→PJp|QJ（COM-E）P|Q−−→PJp|QJ（COM-E）并更改（！COM）和（开放）规则↑XYP−→Pp↓XYP−→Qp1998年，AyP y−−→Qy）p（开放）！P−−→τp（！COM-E ）！P|PJ|QJ是的。P y−−→A Qδ3开放互模拟图2中定义的共归纳谓词定义了我们的开放互模拟概念，在这个意义上，两个过程P和Q被称为是开放互相似的，当有一个证明（可能涉及共归纳推理规则），其中x<$i表示P和Q中所有自由变量s的选择。在π演算的情况下，这个定义与开放互模拟的通常定义完全一致[25，29]。然而，在其他微积分中，这个关系可以另外命名。 在本文的其余部分中，我们将称之为开放互模拟的是互模拟，直到类型为 n和v型变量的区别[25]。请注意，如果我们考虑为mulaxbisimPQ提供，我们将把P和Q的自由名视为不同的。因此，在开放互模拟的情况下，量子化可以帮助编码区别如[29]所示，假定关于名字相等的排除中间假设，即，w让我们能够捕捉到强互模拟。JJA. 齐格勒等人/理论计算机科学电子笔记156（2006）169179P−→JJbisimPQ=νA<$PJ[P−−→ApA<$QJ[Q−−→ApPJQJ.Q−−→ApQJPJ.P−−→ApQjbisimPJQJ]PjbisimQJPJ]A一P Q.Q−−→n→p QJw. bisim（PJw）（QJw）]Pj. P −−A→Pjw. bisim（QJw）（PJw）]n→p n →pQj. Q−A→Qjw. bisim（PJw）（QJw）]v→p v →pPj. P −−A→Pjw. bisim（QJw）（PJw）]v→p v →p图 二、 这是一个很好的解决方案。e=ν可以与共归纳推理规则一起使用。符号用于声明此定义我们现在定义三个二元关系Obisimp，Obisimn→p和Obisimv→p，它们涉及图2中的定义和任何给定的SOS描述的可证明性。让P和Q成为一对对称的函数，并让P或Q中的变量自由。如果P和Q具有类型p，则集合ObisimpcontansP，Qp如果且op如果p是p，则集合Obisim p c o n t a n s p。bisimPQ. 如果P和Q具有p∈n→p第n个元素Obisimn→pcontainsP，Qifandoifxy. bisim（P y）（Qy）. 最后，如果P和Q有类型v→p，则集合Obisimv→p包含P，Q，如果和o，如 果 ， 。bisim（P y）（Qy）.4同余我们现在提出一个概念的一致性在我们的框架。要成为一个同余，一个关系显然应该是构造函数保持的（将相等作为名称上的关系），并且是每个集合上的等价关系此外，在我们的框架中添加抽象类型需要添加基本类型和抽象类型之间的交互条件定义4.1三元组Rp，Rn→p，Rv→p称为同余，如果对于每个γ∈ {p，n→p，v→p}，Rγ是γ型开项的二元关系，并且如果下列性质成立。• （Equ）：这三个二元关系是等价关系。• （λ）：若<$P，Q<$∈Rp，则<$λx.P，λx.Q<$∈Rn→p且<$λx.P，λx.Q<$∈RV→p，180A. 齐格勒等人/理论计算机科学电子笔记156（2006）169i i−→我取决于x的类型。• （App）：若<$M，N <$∈Rn→p且t是n型项，则<$Mx，Nx<$∈Rp.若M，N <$∈ Rv→p且M和N是闭的且t是n型构造函数，它既不出现在N中也不出现在M中，则<$Mt，Nt<$∈ Rp.• （缺点）：如果c是类型为t1→t2→ ··· →tn→p的构造函数，并且如果P1，Q1 . ，nPn，Qnn n均在Rt1， . . . ，Rtn，R tc（P1， . . ，Pn），c（Q1， . . . ，Qn）n在Rp中。定义4.1中的属性是在我们的设置中组合关系的最低要求：除了标准条件之外，还需要（λ）属性来确保在其类型中具有抽象的构造函数将根据标准的同余概念表现出预期的行为。事实上，考虑例如π-演算的in 如果没有（λ）性质，则可以有<$P，Q<$∈Rp而不是<$（λx.P），（λx.Q）<$∈Rn→p，（Cons）性质不能保证在y x P中，在y x Q中，这就是为什么强双相似性不是标准意义上的同余（对于π演算）。注意，在[12]中，同余是使用比（λ）弱得多的要求来表述的：只有当P和Q的所有实例都相关时，才强制<$（λx.P）和（λx.Q）<$相关。[12]故，强双相似性是一个同余。请注意，定义同余的前三个性质适用于Obisimp，Obisimn→p，Obisimv→p，无论使用什么SOS规则，由于其定义的证据理论起源。这些性质是关系的定义所固有的，而不是系统所固有的：它是5规则格式在[9]中，引入了对规则格式的两个限制，以确保双相似性是一个同余。我们提供了这两个限制的推广，以便我们可以在扩展设置中声称相同的定理定义5.1SOS的tyft/tyxt格式将所有推理规则限制为以下形式之一：.Q（P-Ai Y）|i∈IγiΣ， 其中所有模式变量Xj和Yi是不同的，除了名称变量（fX1）...Xn）一−−→Qγ（即n类型的变量）或A. 齐格勒等人/理论计算机科学电子笔记156（2006）169181.ΣA我{Q（Q）|i∈ IiPi−−→YiγX−−→A Qγ， 其中X和所有模式变量Y是是不同的。这里，如前所述，Qi表示可量化变量的可能空序列。 符号Yi表示f（Yiu1. . uk）其中Qi是一号... 阿努乌湾 类型变量γ在集合{p，n→p，v→p}上变化在tyft/tyxt格式的标准定义中，规则的前提是A我形式Pi−−→Yi，其中Yi是变量（类型p）。 这一要求一个变量作为过渡的延续出现意味着不能通过首先探测结果的结构来选择推理规则。A我一个过渡例如，一个形式为Pi −−→0的前提是明确规定的，出去当存在围绕这样的带标签的转移判断的绑定时，有必要用应用于所有这些的变量来替换该变量。bindings：也就是说，前提格式变为.拉乌... 拉乌一 （YuΣ... u）的1kPi−−→i1kγi注意这个前提的实例将导致可能包含也可能不包含变量u1，.，uk.然而，如果在这个应用程序中有更少的连续约束变量，则可以使用该规则来探测延续的一些结构。例如，（开放）规则图1是一个简单的（↑Xy）. 如果这个前提是不确定的（↑XyJ）P y−−→QypP y−−→Qp则前提将仅匹配其中所述第一-第二-第三-第四-第四-第五绑定变量y没有绑定（回想一下，替换在逻辑中是避免捕获的）。这种探测连续结构的能力可能导致双相似性的全等性丢失。定义5.2带有前提集的规则的依赖图A我{Q（Q）|i∈ I}iPi−−→Yiγ如果Y i在P j中是自由的，则有I作为它的节点和从i到j的箭头。如果这个图是非循环的，则规则没有循环依赖当然，我们还要求所有的推理规则都是正确类型的。这种类型限制增加了约束规则的另一种方式。例如，考虑一个推理规则，它包含一个v→p类型的元变量M，并包含一个前提或结论，其中包含公式我182A. 齐格勒等人/理论计算机科学电子笔记156（2006）169一P−→n→pλx，Qx。正确的类型意味着变量M不能被应用于表达式Qx中的x：本质上，表达式M，它需要一个新的名字，不能应用到变量x。我们现在陈述我们的主要结果。定理5.3如果tyft/tyxt格式的标记转移的指定和所有规则都没有循环依赖，那么根据定义4.1，由bisim导出的这个系统的关系是一个同余。这个证明的结构部分遵循[9]中的结构有新奇的有关处理的名称，这主要是由我们的证明理论设置处理。我们在这里只说明证明的结构。主要引理的完整证明出现在[33]的附录首先，考虑函数C（t，s，γ），其中t和s是γ型项且γ∈ {n，p，v→p，n→p}。然后，它按如下方式取值C（t，s，n）=（t = s） C（t，s，v → p）= πy. r（ty）（sy）C（t，s，p）= rt sC（t，s，n →p）=y. r（ty）（sy）第二，我们给出了包含子句的BRRμBisimP Q=BisimP Q以及条款μnr（fT1. Tn）（fS1. Sn）=i=1C（Ti，Si，γi），一个用于过程表达式的每个构造函数f：γ1→ ··· →γn→p。 因此，如果类型p有j个构造函数，则有j+1个子句定义μ好吧尽管它的外观，符号=并不是字面上的等价物。相反，它被用来指示，BMR由相互的归纳定义，μ递归使用所有由=符号标记的为了说明第二个上述定义条款的种类，以下是相应的条款，+ ：p→p和in：n→（n→p）→p。μT1+T2（S1+S2）r（X R）（Y S）= rT1S1rT2S2μ= X = Y（Rw）（Sw）接下来，我们希望证明谓词bisim等于bisim。显然，后者是前者的一个子集。为了证明相反的情况，我们只需要证明Bisim是bisim定义的一个后固定点。自从BisimA. 齐格勒等人/理论计算机科学电子笔记156（2006）169183B = λrλPλQ。AJAJ JJP−−→Pp⊃∃Q.Q−−→Qp[P]QAJAJ JJQ−−→Qp⊃∃P.P−−→Pp[2019 -04 -21]AJAJ J JP−→PA⊃∃Q.Q−−−→Q∧∀w. r（Pw）（Qw）]w）]AAw）]（w）]图三. 用于证明共归纳性质的高阶λ被定义为共归纳的，这意味着BISIM中包含了对BISIM的解释。为了继续下去，我们证明以下引理。引理5.4设B为图3中定义的公式。式我的天啊rPQ是可以证明的这部分证明在结构上与标准案例相似。感兴趣的读者可以参考[33]的附录了解更多细节，并参考[9]将我们的证明与标准情况进行比较。从这个引理，我们可以推导出由两个谓词obisim和obisir所诱导的关系是一致的。我们现在可以证明，根据我们的定义，是一个正如我们在第4节末尾所评论的，同余定义中的前三个条件自动成立，用来描述这三重关系的逻辑。第四个条件对Congr立即成立，并且由于该关系与Obisimp一致，因此它也对Obisimp我们现在已经证明，我们的格式足以确保开放双相似性是一个同余。对名称的量化及其与粘合剂的相互作用的使用使我们的证明几乎与一阶情况一样简单。很容易看出，前面给出的π演算满足我们的扩展tyft/tyxt格式，对于晚期和早期跃迁系统都是如此。因此，我们提供了另一个证明，在这些情况下，开放双相似性是一个同余n→p n →p−−AQJPJ.P −−APJw. r（QJw）（PJ−→ −→n→p n →p−−AP JQJ.Q−−AQJw. r（PJw）（QJ−→ −→v→p v →p−−AQJPJ.P −−APJw. r（QJw）（PJ−→ −→v→pv→p184A. 齐格勒等人/理论计算机科学电子笔记156（2006）1696结论和今后的工作我们已经提出了一种格式，以确保开放的双相似性是一个一致的名称传递演算。为了获得这个结果，我们使用了一种新的转换系统规范，更适合于推理名称传递和名称绑定，基于SOS的扩展，利用基于逻辑的绑定方法。事实上，通过使用能够在内部处理绑定的丰富逻辑，我们能够自然地重用标准的一阶技术来获得我们的结果。这项工作开辟了几个有趣的扩展领域。首先，我们所有的工作都是在证明理论中完成的，这一事实允许使用标准的高阶逻辑编程技术来提供SOS规则的可执行规范以及（有限）过程表达式的符号互模拟[29，28]。最近的Level 0/1系统[30]已经被用来为π演算提供这样的实现。此外，在我们的框架中表达其他的名字传递演算也是很有用的.不同类型的绑定转换之间的区别应该允许我们对融合演算的超等价性进行建模处理π-演算的扩展，如Abadi和Fournet在这里，我们希望我们的完全证明理论框架将为我们提供方便的工具来处理术语的统一。最后，将我们的工作扩展到进程传递演算将是非常有趣的，就像在[11]中所做的那样，因为它将为我们提供一个统一的框架来处理名称绑定和高阶。将这项工作与基于模型理论语义的操作语义的其他工作（如[7]）联系起来，肯定是一个值得追求的有趣方向。致谢。 我们感谢ACI GEOCAL和Rossignol基金的支持，以及Alwen Tiu对本文早期草稿的评论。第一作者的工作得到了巴黎ENS的部分支持。引用[1] 我的意思是，我的意思是， 移动电话、新电话和安全通信。在POPLACM Press，2001.[2] M. Boreale，M. Buscemi和U.蒙塔纳里 D-fusion：一种独特的融合演算。 在proc的APLAS04，LNCS的卷3302。Springer，2004.A. 齐格勒等人/理论计算机科学电子笔记156（2006）169185[3] Karen L.伯恩斯坦高阶语言结构化操作语义的一个同余定理。见John Mitchell，编辑，LICS 98会议记录，第153-163页。IEEE，1998年6月。[4] Bard Bloom，Sorin Istrail，and Albert R.迈耶互模拟是无法追踪的。Journal of the ACM，42（1）：232-268，January 1995.初步版本出现在POPL 1988：229-239。[5] 阿朗佐·丘奇简单类型论的一个公式。Journal of Symbolic Logic，5：56[6] JoéelleDespeyroux.π-c alculus的高性能。在中国。2000年8月17-19日在日本仙台举行的I FIP理论计算机科学国际会议上发表。，2000年8月。[7] M. P. Fiore，G. D. Plotkin和D.图里抽象语法和变量绑定。在第14届计算机科学逻辑上，第193IEEE Computer Society Press，1999.[8] M. J. Gabbay和A.M. 皮茨使用变量绑定的抽象语法的新方法Formal Aspects of Computing，13：341[9] 扬·弗里索·格鲁特和弗里茨·凡德拉格。 结构化操作语义与互模拟一致性。信息与计算，100：202[10] 道格拉斯·豪 函数式程序设计语言中互模拟的全等性证明。信息与计算，124（2）：103-112，1996。[11] Mohammad Reza Mousavi ， Murdoch J. Gabbay ， and Michel A. 雷 尼 尔 高 阶 进 动 的 SOS 。CONCUR'05：Concurrency Theory，2005年地出现。[12] 罗宾·米尔纳通信和移动系统：π演算。剑桥大学出版社，1999年。[13] 雷蒙德·麦克道尔，戴尔·米勒，卡图西娅·帕拉米德西.在微积分中编码转换系统。TheoreticalComputer Science，294（3）：411[14] 戴尔·米勒和戈帕兰·纳达图尔操作公式和程序的一种逻辑编程方法。Seif Haridi，编辑，IEEESymposium on Logic Programming，第379-388页，旧金山，1987年9月[15] 戴尔 米勒 和 卡图夏 Palamidessi。基础 方面 的 语法. 在 P. 德加诺，R. Gorrieri ， A. Marchetti-Spaccamela 和 P. Wegner ， 编 辑 ， ACM Computing SurveysSymposium on Theoretical Computer Science：A Perspective，第31卷。ACM，1999年9月[16] 罗宾·米尔纳，约阿希姆·帕罗，大卫·沃克。移动过程的演算，第一部分。信息与计算，100（1）：1-40，1992年9月。[17] 戴尔·米勒和阿尔文·蒂乌一般判断的证明理论。ACM Trans. on Computational Logic，ed.福基翁·科莱提斯出现，2003年11[18] 戴尔·米勒和阿尔文·蒂乌 A Proof Theory for Generic Judgments：An Extended Abstract. 在Proc.18th IEEE Symposium on Logic in Computer Science（LICS 2003）中，第118-127页。IEEE，2003年6月。[19] Alberto Momigliano和Alwen Tiu。微积分中的归纳与共归纳。 Mario Coppo Stefano Berardi和Ferruccio Damiani，编辑，《2003年类型报告》，LNCS第3085期，第293[20] 约阿希姆·帕罗 介绍了π演算。 在Bergstra，Ponse和Smolka，编辑，过程代数手册，第479-543页。 Elsevier，2001年。[21] 弗兰克·普芬宁和科纳尔·埃利奥特高阶抽象语法。在Proc. of the Conference on ProgrammingLanguage Design and Implementation，第199ACM Press，June 1988.[22] G. 普洛特金操作语义学的结构化方法DAIMI FN-19，奥胡斯大学，奥胡斯，丹麦，1981年9月。186A. 齐格勒等人/理论计算机科学电子笔记156（2006）169[23] 约阿希姆·帕罗和比约恩·维克多融合演算：移动过程中的表达性和对称性。计算机科学中的逻辑，176-185页[24] 理查德·斯塔曼逻辑关系和类型化λ-演算。信息与控制，65：85[25] 大卫·桑吉奥吉和大卫·沃克。π演算：移动过程理论。剑桥大学出版社，2001年。[26] 本特·罗森。Plain Chocs：高阶过程的第二代演算。 Acta Inf. ，30（1）：1[27] 阿尔文·蒂乌一个关于逻辑规范推理的逻辑框架。博士论文，宾夕法尼亚州立大学，2004年5月。[28] 阿尔文·蒂乌使用证明搜索进行π演算的模型检查。CONCUR'05：Concurrency Theory，2005年地出现。[29] 阿尔文·蒂乌和戴尔·米勒π-演算的一个证明搜索规范。 2004年9月，第三届全球普适计算基础研讨会[30] Alwen Tiu Gopalan Nadathur和Dale Miller在自动化的证明器中混合有限的成功和有限的失败。2005年5月提交[31] 克里斯·维尔霍夫。带有谓词和否定前提的结构化操作语义的一个同余定理。Nordic J. ofComputing，2（2）：274[32] 阿克塞尔·齐格勒Un format pour que la bisimulation soit une congruence dans les langagesdeprocessusavecmobilit'e. Techn icalreport，ENS，2004. 我的天啊。[33] Axelle Ziegler，Dale Miller，and Catuscia Palamidessi.一种用于名称传递演算的全等格式技术报告，LIX，Ecole Polytechnique，2005年。可在www.example.com上获得http://www.lix.polytechnique.fr/parsifal/ziegler05report.pdf。一全等结果现在我们我们假设读者熟悉微积分背后的基本思想，以及在这种证明中使用定义来提供固定点的主要思想：例如，参见[13，17]。为了证明P：p，Q：p;r PQ Br P Q我们可以假设这是对谓词使用定义左引入规则的结果，然后产生以下两个序列来证明：P：p，Q：p;bisim PQB r P QT：γ，S：γ，...，T：γ，S：γ;C（T，S，γ）∈Bcongrf（T<$）f（S<$）.1 1 11无无无无无无无我我我在第二种情况下，P和Q与f（T1，.，Tn）和f（S1，.，Sn），其中f是类型为γ1→ ··· →γn→p的构造函数.A. 齐格勒等人/理论计算机科学电子笔记156（2006）169187在第一种情况下，对bisim的定义进行一次展开（通过定义的左引入规则），P：p，Q：p; BbisimPQB r P Q.给出了一个简单的证明。在第二种情况下，事情稍微复杂一些一个人可以写B r PQ如下公式：ΣγA.P−−→Aγ PjQJ[Q−−→AγΣΣQJ <$C（PJ，QJ，γ）]Σγ A.Q−−→Aγ QjPJ[P−−→AγΣΣPJ <$C（PJ，QJ，γ）]，其中γ的范围为{p，n→p，v→p}。应用合取权引入规则得到六个序列，由两组三个对称序列组成。由于问题是对称的，我们证明