Maude1中的Typed Mobile Ambients — Cardelli和Gordon环境演算的操作语义和类型系统

理论计算机科学电子笔记147（2006）135-161www.elsevier.com/locate/entcsMaude1中的Typed Mobile AmbientsFernando Rosa-Velardo、Clara Segura和Alberto VerdejoDepartamentodeSistemasInform'ticosyProgramacio'nUniversidadComplutense de Madrid，Madrid，Spain{fernandorosa，cs eg ura，a lbe rto o}@si p. uc m.es摘要Maude揭示了自己是一个强大的工具，用于实现不同类型的语义，以便快速原型可用于尝试示例和证明属性。在本文中，我们将展示如何在Maude中定义Cardelli和Gordon的环境演算的两个语义。 第一个是操作（归约）语义，它需要定义Maude策略以避免无限循环。第二个是Cardelli和Gordon为了避免通信错误而定义的类型系统。该系统的正确性没有得到正式证明。 我们丰富的操作语义与错误规则，并证明良好类型的进程不会产生这样的错误。类型系统是高度不确定的。我们在这里展示了一种在规则中实现这种非确定性的可能方法。保留字：环境演算，操作语义，类型系统，莫德。1介绍Maude是一种支持等式和重写逻辑计算的高级语言和高性能系统[8，7]，它已经成为表示不同类型语义的强大工具[11，20，21]。由于Maude规范是可执行的，因此我们得到的是语言的实现，以便快速原型可用于尝试示例和证明属性。我们使用Maude作为一种元语言，在其中可以正式定义特定语言我们的目标之一是保持尽可能短的表示距离。有几个不同的1由MCyT西班牙项目MIDAS部分支持的工作，TIC 2003-01000。1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.06.041136F. Rosa-Velardo等人/理论计算机科学电子笔记147（2006）135将推理系统映射到重写逻辑的方法。在结构操作语义学的情况下，判断通常具有状态之间的某种转换P→Q的形式，因此考虑将状态之间的这种转换关系直接映射到表示状态的项之间的重写关系的可能性是有意义的。当以这种方式思考时，P1→ Q1.P n→QnP0→Q0成为一个条件重写规则的形式P0−→ Q0如果P1−→ Q1.Pn−→ Qn，其中条件包括重写。通过这种方式，语义规则成为（条件）重写规则，其中结论中的转换成为规则的主要重写，前提中的转换成为重写条件。在本文中，我们将展示如何在同一个框架中集成两个不同的语义，即操作和静态的环境演算（AC）。 这将使我们能够研究涉及它们的性质。首先，我们将Cardelli和Gordon给出的操作语义定义为结构同余和归约规则。我们展示了如何利用重写机制来减少规则的数量，以及我们为了避免无限减少而做出的决定。重写规则不必是连续的或终止的。这种理论上的通用性在规范成为可执行时需要一些控制，因为用户需要确保重写过程不会朝着不希望的方向发展。我们最近为Maude定义了一种策略语言，以控制重写过程[12]。策略表达式可以被定义为减少给定项的重写树。例如，AC中的复制需要定义策略以避免无限循环。Cardelli和其他人为AC定义了几种类型系统[5，3，4]，以避免不同类型的错误：基本上是通信错误，以及违反移动性和开放性约束。我们在这里研究如何实现Cardelli和Gordon [5]定义的第一个类型系统来检测通信错误和语法错误的术语。在那里，他们证明了一个主语归约定理，以证明类型系统的正确性，但没有给出类型意义的正式定义。因此，类型系统和操作语义之间没有形式上的正确性关系。这是一个有趣的练习，形式化的关系，以完成正确性证明。我们丰富的操作语义与错误减少recrucecting我们要避免的错误然后，我们证明（手），F. Rosa-Velardo等人/理论计算机科学电子笔记147（2006）135137一个类型良好的进程永远不会导致这样的错误。我们在Maude和类型系统中实现了类型规则是高度不确定的。我们已经开发了两种（等价的）管理非确定性的方法来实现规则，但我们在这里只展示其中一种（参见[17]的替代实现）。这两种实现都将进程类型推断为重写的结果此外，作为类型规则研究的结果，我们发现，通过添加一个新规则，更多不产生通信错误的进程可以被类型化，因此我们稍微增加了类型系统的能力。在Maude中表示的AC操作语义和类型系统，在某种程度上非常接近原来的数学公式，为我们提供了解释器，这些推理系统可以执行。我们的最终目标是在使用Maude的开发中更进一步，并利用为这种语言设计的正式工具。例如，Maude中关于规范的自动推理得到了实验ITP工具[6]的支持，这是一个基于重写的定理证明器（也在Maude中实现），可用于证明方程规范的归纳性质。本文的其余部分组织如下。第2节简要介绍了Maude和我们使用的策略语言（在[8，12]中，您可以找到更多细节和示例）。第3节回顾了环境演算。第4节描述了AC的操作语义的实现，并使用它来执行一个重要的示例。第5节用错误规则丰富了语义，并实现了避免通信错误的类型系统。最后，第6节给出了结论和未来的工作。图A.1到A.4显示了环境演算和Cardelli和Gordon类型系统的语法和操作语义2英文片名Maude in a Nutshell在重写逻辑和Maude中，数据和系统的状态都是通过等式规范形式上指定为代数数据类型的。Maude使用了一个非常有表现力的等式逻辑版本，即成员等式逻辑[1]。在这种规范中，我们可以定义新的类型（通过关键字排序）;类型（子排序）之间的类型关系（理解为包含关系）;用于构建这些类型的值的运算符（op），给出其参数和结果，并且可能具有关联138F. Rosa-Velardo等人/理论计算机科学电子笔记147（2006）135例如，（ask）或交换（ask）;标识用这些运算符构建的项的方程（eq）;以及成员资格（mb）t：s，其声明项t具有排序s。方程和成员资格都可以是有条件的，分别使用关键字ceq和cmb。条件由方程和成员的结合（写作/\）假设方程是连续的和终止的，也就是说，我们可以从左到右使用方程将项t约化为唯一的，规范的形式tJ（模运算符属性为结合性、交换性和恒等性），其等价于t（它们表示相同的值）。系统的动态行为由重写规则指定，重写规则的形式如下：t−→tJ如果（ui=vi）<$（wj：sj）<$（pk−→qk）ijk描述系统的本地并发转换。也就是说，当系统的一部分匹配模式t并且满足条件时，它可以被转换为模式tJ的相应实例。2.1战略因为系统模块是重写理论，不需要是连续的或终止的，我们需要有好的方法来控制重写推理过程，原则上不能终止或可能会在许多不希望的方向，通过适当的策略。我们已经为Maude定义了一种策略语言，可以用来控制规则如何应用于重写术语[12]。最简单的策略是常量idle，总是成功，什么都不做，失败，这总是失败。 基本策略由规则的应用组成（由相应的规则标签）到给定术语。在这种情况下，规则被应用于术语中任何它匹配满足其条件的地方。当所应用的规则是在条件中具有重写的条件规则时，策略语言允许通过搜索表达式来控制如何解决重写还提供了一个操作top，用于将规则的应用限制在术语的顶部。然后组合基本策略，以便将策略应用于执行路径。 一些策略组合子是结构的简单表达式：c oncatena tion（;），union（|），以及iteration（* 表示0次或多次迭代，+表示1次或多次迭代，并且！对于一个直到结束”迭代）。另一个策略组合子是典型的if-then-else，但一般化了，所以第一个论点也是一个策略。该语言还提供了一个orelse组合子，只有当第一个策略不成功时才应用第二个策略F. Rosa-Velardo等人/理论计算机科学电子笔记147（2006）135139一个项被拆分为子项，并指定如何重写这些子项。3Ambient演算在本节中，我们将介绍有关环境计算的基本概念[2]，这是一个进程代数，重点关注位置，移动性（代理及其环境）和授权（移动或交互）的概念。环境将是这个模型的主要实体。环境是由计算发生的边界限制的地方。它们是分层结构的，因此我们不会抽象出到达每个目的地所需的路径。智能体被限定在环境中，环境在智能体的控制下移动，允许嵌套环境的移动，其中还包括数据和实时计算。在图A.1中，给出了带有通信原语的AC语法。我们将考虑两个不相交的集合，N ={m，n，. . }，并且Var ={x，y，.. . }表示变量，还有一个特殊的符号。对于标识符，我们将Id = NVar表示为，Cap ={in N，out N，open N|N∈Id} for capa-babilities.我们将在元素上形成的路径（序列）的集合写为A曲霉环境记为n[P]，其中n是它的名称，P是它的内容，它本质上是顺序过程和子环境的平行组合。这些顺序过程可以是预固定过程M.P，这意味着它必须在表现为P之前消耗M;多元输入（x1：W1，. ...，M n.我们将假设出现在输入结构中的变量是两两不同的.此外，可以创建新的名称（限制）（νn：W）P，并且可以复制进程！P.有一个特殊进程0处于非活动状态。请注意，为了简单起见，在语法定义中，环境名称和功能属于相同的语法类别。因此，语法允许构造无意义的过程，例如n.P或in n[P]。稍后，这些项将被我们将在第5节讨论的类型系统排除。该语言的操作语义是通过一个结构同余关系和一个归约关系定义的。前者基本上识别了那些等价于一些微不足道的句法重组的过程。它是满足图中规则的最小等价关系A.2.例如，当与其他进程并行时，可以消除（或添加）不活动进程0。此外，过程可以通过α-转换来识别，直到重命名为140F. Rosa-Velardo等人/理论计算机科学电子笔记147（2006）135绑定名称和变量：（νn：W）P=（νm：W）P{n：=m}如果m/∈fn（P）（x1， .. . ，xn）P=（yi，. . ，yn）P{xi：=yi}如果yi∈/fv（P）受限制的名称不能在其作用域之外使用。然而，α-转换可以用来避免名称冲突，并且通过这种方式，原则上不能从受限制的术语中知道受限制的名称。通过挤出规则，我们可以将限制的范围从一个并行组件扩大到整个并行组合，前提是受限制的名称不出现在其他组件中：P|（νn）Q∈（νn）（P|Q） 如果n/∈fn（P）如前所述，如果上面的进程P确实有n作为自由名，并且我们希望P和Q相互作用，我们总是可以应用α转换。这也可以应用于环境，如规则（结构Res Amb）所示。约简规则主要给出了移动性和通信性公理。环境可以移动到它们的兄弟环境中，也可以移动到它们周围的环境中，分别如规则（Red In）和（Red Out）中所述。它们也可以溶解它们的子环境的边界，因此包含在开放环境中的过程现在属于开放环境，如规则（红色开放）中所定义的。最后，通信可能发生在他们内部（红色通信）。规则的其余部分指出 ， 归 约 可 以 发 生 在 某 些 构 造 函 数 中 ， 即 restriction 、 ambients 和parallel，但不能发生在input、prefixes或replications中。最后，规则（RedRing）明确了我们正在处理模结构等价的事实。作为语义的说明性示例，让我们考虑以下示例：n.出口n.in出口。M|打开，打开。（x）Q]F. Rosa-Velardo等人/理论计算机科学电子笔记147（2006）135141这一进程可按以下方式发展：n.不，n.in，不。M|打开，打开。（x）Q]）n.不，n.in，不。[M] |0个字符]|打开，打开。（x）Q]）→a [m] [M] |n [0]|打开，打开。（x）Q]（1）n [0] |a [m] ⟨M⟩| 0个字符]|打开，打开。（X）Q]→（2）n [0] |m [a] M [a] |0个字符]|打开一个. （x）Q]n [0]|打开，打开。（十）Q |a [M]]→n [0] |m [（x）Q |Mn [0] |m [Q{x：= M}]其中，例如，可以使用规则（Struct Par）、（Struct Par Comm ）、（Struct Zero Par）和（Struct Amb）来证明等价性（1）成立，并且可以使用规则（Red Par）和（Red In）来进行步骤（2）4移动环境在Maude中的实现在本节中，我们将在Maude中实现AC的操作语义。我们尽可能忠实于微积分最初的描述方式。首先，我们定义语法，然后通过等式和重写规则实现操作语义。最后，我们定义了控制重写规则应用的策略。所有的代码都可以在Maude的网站上找到4.1定义我们在这里定义AC语法。为了可读性，我们省略了大多数源代码中的变量声明和运算符优先级定义必须考虑如何处理绑定名称和变量。在AC中有两个绑定操作符：创建新名称（νn）绑定名称，输入操作（x）绑定变量。我们需要de Bruijn在索引名称ni中，i表示自由出现和其绑定出现之间的中间n绑定的数量因此，我们必须在AC语法中使用索引名称和变量。我们可以使用Maude为了清楚起见，名称是Qids142F. Rosa-Velardo等人/理论计算机科学电子笔记147（2006）135以字母“a”到“t”开头的变量，以及以字母“u”到“z”开头的变量，这些变量可以很容易地使用成员公理来定义。索引名称和变量，我们称之为Acid，定义为：排序Qidn Qidx。子分类Qidn Qidx=“u”.名称Var Acid。subsortsName Var Var. op_{_}：Qidn Nat-> Name.此外，我们需要函数来管理索引名称和变量[18]。本质上，它们在必要时增加索引以避免名称冲突。请注意，在一个由想要执行示例的用户定义的系统中，每个名称和变量都有一个0索引，因为与0不同的索引只会通过通信或α转换产生。因此，我们定义了一个装饰函数dec，它用适当的0填充用户定义的系统钻石时标 我们在这里没有给出它的定义（完整的代码见[16有了定义好的名字和变量，我们就可以直接定义消息和进程。消息可以是（索引的）名称和变量、基本值（如整数）、功能和路径：排序消息能力路径。子分类Int Acid能力路径<消息。[_]中的操作：消息->能力。op out[_] ： 消 息 -> 能 力 。opopen[_]：消息->能力。op eps：-> Path.op_._ ：消息消息->路径[asview]。为了定义过程，我们首先需要定义输入和输出序列，以便进行多种通信。输入序列应排除同一变量的多次出现（这是通过将输入序列的连接运算符_，_定义为partial~>，并给出一个条件成员资格，说明连接何时有效）。输入序列包括每个输入变量的类型注释（排序AType）;这是因为稍后我们将定义AC的类型系统（目前可以忽略它们）。sort InputSeq.F. Rosa-Velardo等人/理论计算机科学电子笔记147（2006）135143op_：_：Qidx AType -> InputSeq.op_，_：InputSeq InputSeq ~> InputSeq [asq].操作符：Qidx InputSeq ->Bool。等式bel（x，y：T）=x == y。等式bel（x，（I1，I2））= bel（x，I1）或bel（x，I2）。cmb（（x：T），IS）：如果不是bel（x，IS），则为InputSeq。sort输出序列子排序消息<输出序列。op _，_：OutputSeq OutputSeq -> OutputSeq [asplane].过程定义如下对NSProcess Process进行排序。子排序NSProcess Process.* 0进程操作_._ ：消息处理-> NSProcess。操作_|_：Process Process -> Process [aslogid：stop].操作_|_：NSProcess NSProcess -> NSProcess [aslogid：stop]。OP！_ ：过程->过程。OP！_ ：NSProcess -> NSProcess。op_'[_']：消息处理-> NS处理。op<_>：OutputSeq -> NSProcess。op'（_'）_：InputSeq Process -> NSProcess。op new '[_：_']_：Qidn类型进程->进程。op new'[_：_']_：QidnATypeNSProcess->NSProcess。其中我们使用两种不同的排序：NSProcess用于与stop不同的进程，Process用于每个进程。我们将在下一节中看到这种方法的优点。从现在开始，我们将使用P，Q，R作为排序Process的变量，使用NSP，NSQ，NSR作为排序NSProcess的变量。使用这个语法定义，我们可以编写下面的防火墙示例，如[2]所示：op firewall：Process -> Process。eq firewall（P，Q）= newk：Amb[Shh]]（“n [open k”k]. P]的范围| new[’m: Amb[Shh]](’m [’k [out[’m]. in 1997]. 以['m]为单位。停止]|Q]）。类型注释现在可以忽略了。Ambient上述机制可以用于保证认证，以通过以下方式确保消息的新鲜度：随机数的手段或模拟共享密钥加密。4.2操作语义AC的操作语义由一组结构同余规则和一组约简规则组成。令人高兴的是，Maude免费给了我们一些一致性规则。特别是144F. Rosa-Velardo等人/理论计算机科学电子笔记147（2006）135• 规则（Struct Res）到（Struct Action）和（Struct Input）定义了每个过程构造器的一致性，由于Maude中的等式一致性，因此不需要定义。• 规则（Struct Par Asynchronous）、（Struct Par Comm）和（StructZero Par）通过在并行运算符的声明中指明关联性、交换性和恒等属性来获得。规则（结构路径），（结构零Res）和（结构零Repl）是通过Maude方程定义的，因此只能从左到右应用。我们写它们是为了寻找一个标准形式，以便保持一致性：eq eps. P = P。eq（M.N）。 P= M。 （N.P）。eq！停止=停止。eqnew[n：T] stop =停止。拉伸规则（Struct Res Res）、（Struct Res Par）和（Struct ResAmb）被写成三个等式，用于绑定名称的α转换和（字母）重新排序如果string（l）string（k），则ceq new[k：T1]new[l：T2] P = new[l：T2] new[k：T1] P<。eq（（new[n：T] NSP）|NSQ）= new[n：T]（NSP|（[shiftln]NSQ））。等式M [new[n：T] P]= new[n：T]（（[shiftln] M）[P]）。其中移位寄存器适当地增加索引注意，为了使第一条规则真正一致，我们应该在（不常见的）情况下定义类型之间的（仅仅是语法）顺序，使用不同类型的在这种情况下，重新排序应该重新排列所涉及的名称的索引。注意，我们在第二个（α-转换）规则中使用了NSProcess排序的变量NSP和NSQ，这样它只适用于进程与stop不同的情况。如果我们使用sort Process的变量，|可以通过一次又一次地生成|停下来，以符合方程。我们将在类似的情况下面这种方法使我们能够避免会增加执行时间的条件方程。我们不会因为把前面的同余规则写成方程而失去任何力量，因为它们只是重新排序项，以便可以应用后续的归约规则要做到这一点，并行运算符属性和等式同余是基本的。方程的应用产生一个标准形式，其中：• stop仅出现在前缀（capability或input action）之后或F. Rosa-Velardo等人/理论计算机科学电子笔记147（2006）135145环境温度;• eps没有出现在任何地方，• 与右侧相关联的能力序列• 新的操作符被尽可能地挤出（以便可以发生交互）并且按顺序排序。规则（结构复制Par）将在后面讨论。最后，我们有约简规则作为Maude中的重写规则，其中一些是条件重写规则：rl[RedIn]：n[in[m]. P| Q]| m[R] => m[n[P| Q]| R]。rl[RedOut] ：m[n[out[m].P|Q]|R]=> n[P|Q]|m [R].rl[RedOpen]：打开[n]。P| n[Q] => P|Q.rl [RedComm]：（（I）P）| =>束缚（I，O）P。crl [RedRes]：new[k：T] P => new[k：T]QifP =>Q.crl [RedAmb]：如果P => Q，则n[P]=>n[Q]。crl[RedPar]：NSP |NSR => Q |NSR，如果NSP => Q。函数bound（I，O）生成一个替换作为通信的结果，然后将其应用于进程。请注意，我们免费使用了同余和归约规则的交错，因为Maude本身将方程的应用与重写规则交错。然而，演算的归约关系并不是所有算子的同余关系，而只是限制算子（Red Res）、环境构造（Red Amb）和并行算子（Red Par）的归约关系。 这意味着我们不能自由地使用我们写的重写规则，因为Maude会在一个术语中的任何地方应用它们;我们不希望它们在前缀，输入和复制之后应用。这就是为什么有必要定义一种控制这些规则应用的策略我们现在来研究复制过程中发生了什么。复制行为在AC中通过一致性规则（Struct Repl Par）进行描述。我们不能把它写成和其他方程一样的方程，因为没有一个方向是方便的。如果我们从左到右应用它，我们会得到一个无限循环，因为我们可以无限地展开复制。如果我们从右到左应用它，我们就看不到当复制过程的新副本与系统的其他部分甚至与它自己的其他副本交互时，系统是如何演化作为一个例子，146F. Rosa-Velardo等人/理论计算机科学电子笔记147（2006）135为了过程！在...中，在...中0]要进化，需要展开复制两次：！在...中，在...中0]在...中，在...中0个字符]|！在...中，在...中0]在...中，在...中0个字符]|在...中，在...中0个字符]|！在...中，在...中0]→在...中，在...中0 |n [0]]|！在...中，在...中0]→...这导致我们将这个一致性规则写成两个重写规则：rl[Rep]：！ P => P|！ P.rl [UnRep]：P|！P =>！P.我们仍然有同样的问题，所以我们必须定义策略来控制这些规则的应用我们希望仅在后续交互需要时应用ruleRep，并使用ruleUnRep删除复制流程的孤立的不必要副本。4.3评价战略我们需要策略来控制前面定义的重写规则的应用。运动和交流的规则可以在任何地方应用，但在预设和复制之下。因此，我们首先定义一种策略来控制这些规则的应用，称为norep（无复制）。正如我们所写的规则，减少内部环境，在平行的过程中，名称限制，我们只需要在顶层应用所有重写规则。这意味着该策略将递归应用，但当遇到前缀或复制时，规则RedRes、RedAmb和RedPar是条件重写规则，因此策略需要知道在重写条件中应用哪个策略以及如何在生成的重写树中搜索在这种情况下，我们想要相同的策略被（递归地）应用，深度优先搜索就足够了（策略在seq声明中定义seq norep = top（RedIn）|顶部（RedOut）|顶部（RedOpen）|顶部（RedComm）|top（RedAmb{dfs（norep）}）|top（RedPar{dfs（norep）}）|top（RedRes{dfs（norep）}）。现在我们将这个策略与一个新的策略结合起来来控制复制。我们只想在必要时展开复制，也就是说，当作为展开的结果，一个运动或通信发生时。不过，我们必须小心，因为两个展开可能是必要的移动-F. Rosa-Velardo等人/理论计算机科学电子笔记147（2006）135147事件或通信发生，因为发生在过程中！在...中，在...中0]。此外，即使一次展开足以进行一次缩减步骤，如果我们立即强制进行这种缩减，我们也可能会丢失重写。例如，如果我们的策略在每次展开到进程n [0]之后应用norep，|！在...中，在...中0]，我们将得到以下重写：n [0]|！在...中，在...中0]n [0]|在...中，在...中0个字符]|！在...中，在...中0]→n [n [0]|！在...中，在...中0]n [n [0]|在...中，在...中0个字符]|！在...中，在...中0]→n [n][0] |n [0]]|！在...中，在...中0] .所以只有像n [n [0]这样的进程|......这是什么？|！|! 在...中，在...中[0]可以获得，失去（除其他外）以下可能的重写：n [0]|！在...中，在...中0]n [0]|在...中，在...中0个字符]|！在...中，在...中0]n [0]|在...中，在...中0个字符]|在...中，在...中0个字符]|！在...中，在...中0]→n [0]|在...中，在...中0 |n [0]]|！在...中，在...中0]→n [n [n [0]]|！在...中，在...中0]→...我们声称，两个unrollings是足够的，以获得所有的解决方案，这意味着- ing的解决方案，这些过程中，没有减少规则可以应用。这可以通过检查S的重写树来容易地证明|P|P|！P和S|P|P|P|！P.唯一的区别是我们找到解决方案的水平。考虑到前面的两个观察，我们定义了一个新规则，允许我们展开两次任何出现在进程中的复制，但是在prefixes之后和复制下（与norep的原因相同）。rl [Rep2]：P =>rep（P）。被定义为oprep：Process ->Process。eqrep（！P）=P |P|！P. 等式rep（M[P]）= M[rep（P）]。当量代表（NSP |NSQ）= rep（NSP）|代表（NSQ）。148F. Rosa-Velardo等人/理论计算机科学电子笔记147（2006）135eq rep（new[n：T] P）= new[n：T] rep（P）。等式rep（P）= P [owise]。由于我们希望展开以检查整个过程，因此此规则也应该应用于顶层seq unroll-rep = top（Rep2）。当然，也有可能展开对进程的演化没有帮助，而只是生成空闲副本。在这种情况下，我们应用规则UnRep来吸收这些垃圾副本。例如，通过展开两次，然后进行通信，|！（x）x [0]将重写为n [0]|（x）x [0]|！（x）x [0]，然后通过应用规则UnRep，我们将获得n [0]|！（x）x[0]。此外，为了避免在进程没有终止时的无限计算，用户应该告诉策略他想要执行多少语义缩减步骤。因此，该策略应用复制展开（如果有的话），并立即应用一个移动和/或通信步骤（如果可能的话，我们还没有完成）。当我们完成时，我们消除了所有闲置的副本。seq cg（0）= UnRep！ .seq cg（s（n：Nat））=（unroll-rep; norep; cg（n：Nat））orelse（UnRep！）.例如，当重写！（“n {0} [在”n {0}中]。停止]|“n{0} [在”n {0}中]。停止]）通过使用策略CG（1），我们得到以下解：！（“n {0}[在”n {0}中]。停止]|“n{0}[在”n{0}中]。停止]）|“n{0}[在”n {0}中]。停止|'n{0}[停止]]其中复制过程的一个副本已经进化。通过应用cg（2），我们得到以下三个解：方案一：！（“n {0}[在”n {0}中]。停止]|“n{0}[在”n {0}中]。停止]）|“n{0}[在”n {0}中]。停止]|“n{0}[在”n {0}中]。停止|'n{0}[停止]|' n{0}[stop]]解决方案2：！（“n {0}[在”n {0}中]。停止]|“n{0}[在”n {0}中]。停止]）|“n{0}[在”n {0}中]。停止]|“n{0}[在”n {0}中]。停止|'n{0}' n {0}[stop]解决方案3：！（“n {0}[在”n {0}中]。停止]|“n{0}[在”n{0}中]。停止]）|“n{0}[在”n {0}中]。 停止|'n{0}[停止]]|“n{0}[在”n {0}中]。 停止|'n{0}[停止]]仅通过两次运动和一次最终应用UnRep获得。 这三种可能性可以很容易地通过在n中写过程n [得到。0个字符]|在...中，在...中0个字符]|在...中，在...中0个字符]|在...中，在...中[0]和所有可能的方式，使只有两个运动。作为最后一个例子，当使用cg（4）重写防火墙（P，Q）时，我们得到：new'k：Amb[Shh]]new['m：Amb[Shh]]（'m {0}[Q|'n{0}[[shifting'm]P]]）F. Rosa-Velardo等人/理论计算机科学电子笔记147（2006）135149我我我我我果然通过使用过程变量P和Q，我们能够普遍量化防火墙示例的执行，并给出任何两个过程的一般结果。然而，有一些操作不能应用，如移位，并保持原样。4.4一个例子：选举制度文献[13]研究了π-演算中的纯环境演算的编码问题。特别是，它表明，对称的选举系统的任意大小存在的纯环境演算（AC没有通信），这意味着AC是不可编码的π演算与单独的选择。[13]的作者声称以下过程是对称的选举系统：净k= P0|......这是什么？| P k−1P i= n i [in n j. 0|m i [in（s）. out（s−）. 出岛0]]j∈Sks∈Tk哪里表示平行组合，Sk是所有自然数小于k，不包括i，Tk是所有长度为k−1的字符串的集合，使用S k的每个成员恰好一次，s−是字符串s的逆序，in（s）是对于每个连续的j ∈ s的in n j的序列（类似地，out（s））。对于一个像上面那样的对称网来说，它是一个选举系统，它的所有最大计算必须产生一个唯一的可观察量，因为它们都是不同的。在这种情况下，可观测量是具有{m1，.，m k−1}在最高层。我们已经在AC的表示中实现了上面的示例：op Net：Nat->Process。eq Net（k）=elect（0，k）。操作选择：Nat Nat-> Process。ceq elect（i，k）=Pr（i，k）|elect（i+1，k）if i

下载后可阅读完整内容，剩余1页未读，立即下载